library test

spec partial_order =

sort elem

pred __<=__ : elem*elem

forall x,y,z:elem

. x <= x %(reflexive)%

. x <= y /\ y <=x => x=y %(antisymmetric)%

. x <= y /\ y <= z => x <=z %(transitive)%

end

spec strict_partial_order =

sort elem

pred __<__ : elem*elem

forall x,y,z:elem

. not x < x %(irreflexive)%

. x < y /\ y < z => x <z %(transitive)%

. x < y => not y < x %(asymmetric)% %implied

end

view v : partial_order to

{strict_partial_order then

pred __<=__(x,y:elem) <=> x<y \/ x=y }

end