Floors: trait
  Floor enumeration of K, S, B, 1, 2, 3, 4, 5, 6
  introduces __<__: Floor, Floor -> Bool
             pred : Floor -> Floor
  asserts with x, y, z : Floor
    ~ ( x < x);
    x < y /\ y < z => x < z;
    x < succ(x);
    y = succ(x) => x = pred(y)