E.2.5 Nat_List_with_Reverse_Orders

spec

Ordered_Nat =

 

Nat then

preds

__ < __ , __ > __ : Nat × Nat

vars

m,n : Nat

·

zero < n

·

¬ (succ m < zero)

·

succ m < succ n <=> m < n

·

m > n <=> n < m

end

spec

Nat_List_with_Reverse_Orders =

 

List_with_Order [ Ordered_Nat fit Elem ^_|-> Nat, __ < __ ^_|-> __ < __ ]

and

 

List_with_Order [ Ordered_Nat fit Elem ^_|-> Nat, __ < __ ^_|-> __ > __ ]

then

 

axiom

forall l : List[Nat] · order[__ > __](l) = reverse(order[__ < __](l))

end