import "field_logic";
import "listdatatype_logic";

rewrite cons_list_not_empty:
  builtin_eq(cons(?a,?b),empty()) = numeric_const("0")

rewrite reflexivity:
  builtin_eq(?x,?x) = numeric_const("1")

rewrite subtraction_inverse_of_addition:
  builtin_minus(builtin_plus(?y,?z),?y) = ?z

rewrite element_of:
  elem(?e,app(?a1,cons(?e,?a2))) = numeric_const("1")

rewrite length_app_cons:
  len(app(?a1,cons(?e,?a2))) = builtin_plus(builtin_plus(len(?a1),len(?a2)),numeric_const("1"))

rewrite length_of_appended_list:
  len(app(?a1,?a2)) = builtin_plus(len(?a1),len(?a2))

rewrite length_of_cons_list:
  len(cons(?e,?a)) = builtin_plus(numeric_const("1"),len(?a))

rewrite length_non_negative:
  builtin_ge(len(?a),numeric_const("0")) = numeric_const("1")

rewrite only_empty_has_length_zero:
  builtin_eq(len(?a),numeric_const("0")) = builtin_eq(?a,empty())

rule same_list:
 | OL(?x,?y) |- OL(?x,?z)
if
OL(?x,?y) | |- ?y=?z

rule same_root:
 | OL(?x,?y) |- OL(?z,?y)
without
 ?x!=?z
if
OL(?x,?y) | |- ?x=?z

rule appends_equal:
 | |- app(?w,?x)=app(?y,?z)
without
  ?w=?y * ?x=?z
if
 | |- ?w=?y * ?x=?z