use(ex1).
use(ex).
%use(elements).

complete(S) == (ex(S,empty)=empty).

correct(S) ==
 (all(S1,all(E,all(S2,prefix(S1,S) and (S1=cons(S2,dmin(E)) or S1=cons(S2,del(E))) => lower_bound(E,ex1(S2,nil))=<E)))).

preconditions(S) ==
 (correct(S) and all(E,contains(ex(S,empty),E) => lower_bound(E,ex1(S,nil))=<E)).

property(S) ==
 (all(S1,all(E,all(S2,prefix(S1,S) and S1=cons(S2,dmin(E)) => elem(del_min(ex(S2,empty)))=E)))).

main_property(S) == (preconditions(S) and property(S)).

precedence([ex1,ex,del_min,contains,lower_bound,elem,empty,prefix,dmin,del,nil,=<,<]).
top_predicates_precedence([main_property,property,preconditions,correct,complete]).