use(string_predicates).



induction_step_create ==
  (main_property(nil) and all(S,main_property(S) => main_property(cons(S,create)))).

induction_step_insert ==
  (main_property(nil) and all(S,all(E,main_property(S) => main_property(cons(S,ins(E)))))).

induction_step_delete ==
  (main_property(nil) and all(S,all(E,main_property(S) => main_property(cons(S,del(E)))))).

induction_step_delete_min ==
  (main_property(nil) and all(S,all(E,main_property(S) => main_property(cons(S,dmin(E)))))).




top_predicates_precedence([induction_step_delete,induction_step_insert,induction_step_create]).