342N/Alibrary test

579N/A

342N/Aspec partial_order =

342N/A sort elem

342N/A pred __<=__ : elem*elem

342N/A forall x,y,z:elem

342N/A . x <= x %(reflexive)%

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

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

342N/Aend

342N/A

342N/Aspec strict_partial_order =

342N/A sort elem

342N/A pred __<__ : elem*elem

342N/A forall x,y,z:elem

342N/A . not x < x %(irreflexive)%

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

342N/A . x < y => not y < x %(asymmetric)% %implied

342N/Aend

342N/A

342N/Aview v : partial_order to

342N/A {strict_partial_order then

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

342N/Aend

342N/A