E.2.4 List_with_Order

spec

List_with_Order [Partial_Order] =
List [sort Elem]

then

 

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