E.2.3 LIST_WITH_ORDER

spec

List_With_Order [
sort Elem; pred __<__ : Elem × Elem
%%  axioms  as usual %% ] =

free type

List[Elem] ::= nil | cons(hd:?Elem; tl:?List[Elem])

ops

insert : Elem × List[Elem]  ->   List[Elem];
order[__<__] : List[Elem]  ->   List[Elem]

vars

x,y : Elem; l : List[Elem]

axioms

order[__<__](nil)=nil;
order[__<__](cons(x,l))=insert(x,order[__<__](l));
insert(x,nil)=cons(x,nil);
x<y   =>   insert(x,cons(y,l))=cons(x,insert(y,l));
¬  (x<y)   =>   insert(x,cons(y,l))=cons(y,insert(x,l))

hide

insert

end