use(string_predicates).

%lm1 == all(S,(all(S2,prefix(S2,S) => prefix(S2,cons(S,create))))).

%lm2 == all(S,correct(S) => correct(cons(S,create))).

%lm3 == all(S,all(S1,all(E,all(S2, prefix(S1,cons(S,E)) and (S1=cons(S2,dmin(E)) or S1=cons(S2,del(E)))=> prefix(S1,S) and (S1=cons(S2,dmin(E)) or S1=cons(S2,del(E))))))).

%lm4 == all(S,correct(cons(S,create)) => correct(S)).

%lm5 == all(S,preconditions(S) => preconditions(cons(S,create))).

lm2 == all(S,preconditions(S) and property(S) => property(cons(S,create))).


top_predicates_precedence([lm3,lm2,lm1]).