2.4 COMPOUND_SYMBOLS_ARE_NICE

spec

COMPOUND_SYMBOLS_ARE_NICE =

 

LIST_WITH_ORDER[ NATURAL fit Elem |-> Nat, __<__ |-> __leq__ ]

and

 

LIST_WITH_ORDER[ NATURAL fit Elem |-> Nat, __<__ |-> __geq__ ]

then

var

l : List[Nat]

axiom

order[__geq__](l) = reverse(order[__leq__](l))

end