library Blocks

spec Props =
  preds A,B,C : ()
  . A
  . not (A /\ B)
  . C => B
  . not C %implied
end

spec Tarski1 =
  sort Blocks
  preds Cube, Dodec, Tet, Small, Medium, Large : Blocks
  ops a,b,c : Blocks
  . not a=b
  . not a=c
  . not b=c
  . Small(a) => Cube(a)    %(small_cube_a)%
  . Small(a) <=> Small(b)  %(small_a_b)%
  . Small(b) \/ Medium(b)  %(small_medium_b)%
  . Medium(b) => Medium(c) %(medium_b_c)%
  . Medium(c) => Tet(c)    %(medium_tet_c)%
  . not Tet(c)             %(not_tet_c)%
  . Cube(a)                %(cube_a)% %implied
  . Cube(b)                %(cube_b)% %implied
end