axiom associative_andb: associative ? andb.
axiom distributive_andb_orb: distributive ? andb orb.
+lemma andb_true: ∀x.(true ∧ x) = x. intro; reflexivity. qed.
+
lemma and_of_list_permut:
∀i,f,l1,l2. eval i (and_of_list (l1 @ (f::l2))) = eval i (and_of_list (f :: l1 @ l2)).
intros;
lapply (H4 i); clear H4;
rewrite > symm_orb in ⊢ (? ? (? ? %) ?);
rewrite > distributive_orb_andb;
+ demodulate.
+ reflexivity.
+ (*
autobatch paramodulation
+ by distributive_orb_andb,symm_orb,symm_orb,
+ Hletin, Hletin1,andb_true.
+ *)
| simplify in H2 ⊢ %;
intros;
lapply (H2 i); clear H2;
- autobatch
+ pump 100. pump 100.
+ demodulate.
+ reflexivity.
+ (* autobatch paramodulation by andb_assoc, Hletin. *)
| simplify in H2 H4 ⊢ %;
intros;
lapply (H2 i); clear H2;
rewrite > demorgan2;
rewrite > symm_orb;
rewrite > distributive_orb_andb;
- autobatch paramodulation
+ demodulate.
+ reflexivity.
+ (* autobatch paramodulation by symm_andb,symm_orb,andb_true,Hletin,Hletin1. *)
| simplify in H2 ⊢ %;
intros;
lapply (H2 i); clear H2;
- autobatch
+ autobatch paramodulation;
| simplify in H2 ⊢ %;
intros;
lapply (H2 i); clear H2;