(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demo/propositional_sequent_calculus/".
-
include "nat/plus.ma".
include "nat/compare.ma".
include "list/sort.ma".
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;
[1,2:
simplify in H;
destruct H
- | generalize in match H; clear H;
- elim f2;
+ | elim f2 in H ⊢ %;
[1,2:
simplify in H;
destruct H
simplify;
apply (ex_intro ? ? a3);
apply (ex_intro ? ? a4);
- autobatch
+ autobatch depth=4
| right;
intro;
apply (bool_elim ? (same_atom a (FAtom n1)));
intros;
lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1;
simplify in Hletin;
- generalize in match Hletin; clear Hletin;
- generalize in match H2; clear H2;
- generalize in match H; clear H;
- elim l1 0;
+ elim l1 in Hletin H2 H ⊢ % 0;
[ intros;
simplify in H2;
- generalize in match H2; clear H2;
- generalize in match H1; clear H1;
- generalize in match H; clear H;
- elim l2 0;
+ elim l2 in H2 H1 H ⊢ % 0;
[ intros;
simplify in H2;
destruct H2
| assumption
| lapply (H2 n1); clear H2;
simplify in Hletin;
- generalize in match Hletin; clear Hletin;
- elim (eqb n1 n);
+ elim (eqb n1 n) in Hletin ⊢ %;
[ simplify in H2;
rewrite > H2;
autobatch
rewrite > eqb_n_n in H3;
simplify in H3;
(*
- generalize in match H3;
- generalize in match H1; clear H1;
- generalize in match H; clear H;
- elim l 0;
+ elim l in H3 H1 H ⊢ % 0;
[ elim l2 0;
[ intros;
simplify in H2;
]
[ autobatch
- | generalize in match H4; clear H4;
- generalize in match H2; clear H2;
- elim t1;
+ | elim t1 in H4 H2 ⊢ %;
[
|
|