Recently introduced bug in CicRefine.eat_prods fixed: a whd was now missing.

Added a test to verify the performances of refinement.

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index e99ce5cd70285fe94680b80fdab6a20442b860c7..90643164d576bf14b5f309fc4011104bfa1d8b1b 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1197,7 +1197,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       function
         | [] -> [],metasenv,subst,hetype,ugraph
         | (hete, hety)::tl ->
-            (match hetype with
+           (match (CicReduction.whd ~subst context hetype) with 
                  Cic.Prod (n,s,t) ->
                    let arg,subst,metasenv,ugraph1 =
                      try

diff --git a/matita/tests/hard_refine.ma b/matita/tests/hard_refine.ma
new file mode 100644 (file)
index 0000000..b528414
--- /dev/null
+++ b/matita/tests/hard_refine.ma
@@ -0,0 +1,67 @@
+set "baseuri" "cic:/matita/TPTP/BOO024-1".
+include "legacy/coq.ma".
+alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
+(* Inclusion of: BOO024-1.p *)
+(* -------------------------------------------------------------------------- *)
+(*  File     : BOO024-1 : TPTP v3.1.1. Released v2.2.0. *)
+(*  Domain   : Boolean Algebra *)
+(*  Problem  : Half of Padmanabhan's 6-basis with Pixley, part 2. *)
+(*  Version  : [MP96] (equality) axioms : Especial. *)
+(*  English  : Part 2 (of 3) of the proof that half of Padmanaban's self-dual *)
+(*             independent 6-basis for Boolean Algebra, together with a Pixley *)
+(*             polynomial, is a basis for Boolean algebra. *)
+(*  Refs     : [McC98] McCune (1998), Email to G. Sutcliffe *)
+(*           : [MP96]  McCune & Padmanabhan (1996), Automated Deduction in Eq *)
+(*  Source   : [McC98] *)
+(*  Names    : DUAL-BA-2-b [MP96] *)
+(*  Status   : Unsatisfiable *)
+(*  Rating   : 0.00 v2.2.1 *)
+(*  Syntax   : Number of clauses     :    8 (   0 non-Horn;   8 unit;   1 RR) *)
+(*             Number of atoms       :    8 (   8 equality) *)
+(*             Maximal clause size   :    1 (   1 average) *)
+(*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
+(*             Number of functors    :    7 (   3 constant; 0-3 arity) *)
+(*             Number of variables   :   15 (   2 singleton) *)
+(*             Maximal term depth    :    5 (   2 average) *)
+(*  Comments : *)
+(* -------------------------------------------------------------------------- *)
+(* ----Half of Padmanabhan's self-dual independent 6-basis for Boolean Algebra: *)
+(* ----pixley(X,Y,Z) is a Pixley polynomial: *)
+(* ----Denial of conclusion: *)
+
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
+alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
+alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
+alias id "sym_eq" = "cic:/Coq/Init/Logic/sym_eq.con".
+alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
+
+theorem prove_add_multiply: \forall (A: (Set)).(\forall (a: (A)).(\forall (add: ((A) \to ((A) \to (A)))).(\forall (b: (A)).(\forall (inverse: ((A) \to (A))).(\forall (multiply: ((A) \to ((A) \to (A)))).(\forall (n1: (A)).(\forall (pixley: ((A) \to ((A) \to ((A) \to (A))))).(\forall (H0: (\forall (X: (A)).(\forall (Y: (A)).((eq) (A) ((pixley) (X) (Y) (X)) (X))))).(\forall (H1: (\forall (X: (A)).(\forall (Y: (A)).((eq) (A) ((pixley) (X) (Y) (Y)) (X))))).(\forall (H2: (\forall (X: (A)).(\forall (Y: (A)).((eq) (A) ((pixley) (X) (X) (Y)) (Y))))).(\forall (H3: (\forall (X: (A)).(\forall (Y: (A)).(\forall (Z: (A)).((eq) (A) ((pixley) (X) (Y) (Z)) ((add) ((multiply) (X) ((inverse) (Y))) ((add) ((multiply) (X) (Z)) ((multiply) ((inverse) (Y)) (Z))))))))).(\forall (H4: (\forall (X: (A)).((eq) (A) ((add) (X) ((inverse) (X))) (n1)))).(\forall (H5: (\forall (X: (A)).(\forall (Y: (A)).(\forall (Z: (A)).((eq) (A) ((multiply) (X) ((add) (Y) (Z))) ((add) ((multiply) (Y) (X)) ((multiply) (Z) (X)))))))).(\forall (H6: (\forall (X: (A)).(\forall (Y: (A)).((eq) (A) ((multiply) ((add) (X) (Y)) (Y)) (Y))))).
+ \forall HH:(\forall x:A.eq A (multiply (add x x) n1) (add (add x x) (add x x))).
+ \forall HH1:(\forall x:A.eq A (multiply (add x x) n1) (add x x)).
+((eq) (A) ((add) ((multiply) (a) (b)) (b)) (b)))))))))))))))) .
+intros.
+(* sotto termine piu' piccolo, comunque lentissimo *)
+letin k \def (eq_ind_r A (add (multiply ? (inverse ?)) (multiply b n1)) (\lambda x:A.(eq A (multiply b n1) x)) (eq_ind A (multiply (multiply b n1) n1) (\lambda x:A.(eq A (multiply b n1) (add (multiply ? (inverse ?)) x))) (eq_ind A (pixley ? ? (multiply b n1)) (\lambda x:A.(eq A x (add (multiply ? (inverse ?)) (multiply (multiply b n1) n1)))) (eq_ind A (add ? (inverse ?)) (\lambda x:A.(eq A (pixley ? ? (multiply b n1)) (add (multiply ? (inverse ?)) (multiply (multiply b n1) x)))) (eq_ind_r A (add (multiply ? (multiply b n1)) (multiply (inverse ?) (multiply b n1))) (\lambda x:A.(eq A (pixley ? ? (multiply b n1)) (add (multiply ? (inverse ?)) x))) (H3 ? ? (multiply b n1)) (multiply (multiply b n1) (add ? (inverse ?))) (H5 (multiply b n1) ? (inverse ?))) n1 (H4 ?)) (multiply b n1) (H2 ? (multiply b n1))) (multiply b n1) (eq_ind_r A (multiply n1 (add b b)) (\lambda x:A.(eq A (multiply (multiply b n1) n1) x)) (eq_ind_r A (multiply n1 (add b b)) (\lambda x:A.(eq A (multiply x n1) (multiply n1 (add b b)))) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (multiply (multiply n1 (add b b)) n1) x)) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (multiply x n1) (add (multiply b n1) (multiply b n1)))) (H8 (multiply b n1)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply b n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1)))) (multiply b n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))))) b (eq_ind A (pixley ? ? b) (\lambda x:A.(eq A x (add (multiply ? (inverse ?)) (multiply b n1)))) (eq_ind A (add ? (inverse ?)) (\lambda x:A.(eq A (pixley ? ? b) (add (multiply ? (inverse ?)) (multiply b x)))) (eq_ind_r A (add (multiply ? b) (multiply (inverse ?) b)) (\lambda x:A.(eq A (pixley ? ? b) (add (multiply ? (inverse ?)) x))) (H3 ? ? b) (multiply b (add ? (inverse ?))) (H5 b ? (inverse ?))) n1 (H4 ?)) b (H2 ? b))).
+focus 162. clearbody k.
+letin k1 \def (eq_ind_r A (add (multiply ? (inverse ?)) (multiply b n1)) (\lambda x:A.(eq A (multiply b n1) x)) (eq_ind A (multiply (multiply b n1) n1) (\lambda x:A.(eq A (multiply b n1) (add (multiply ? (inverse ?)) x))) (eq_ind A (pixley ? ? (multiply b n1)) (\lambda x:A.(eq A x (add (multiply ? (inverse ?)) (multiply (multiply b n1) n1)))) (eq_ind A (add ? (inverse ?)) (\lambda x:A.(eq A (pixley ? ? (multiply b n1)) (add (multiply ? (inverse ?)) (multiply (multiply b n1) x)))) (eq_ind_r A (add (multiply ? (multiply b n1)) (multiply (inverse ?) (multiply b n1))) (\lambda x:A.(eq A (pixley ? ? (multiply b n1)) (add (multiply ? (inverse ?)) x))) (H3 ? ? (multiply b n1)) (multiply (multiply b n1) (add ? (inverse ?))) (H5 (multiply b n1) ? (inverse ?))) n1 (H4 ?)) (multiply b n1) (H2 ? (multiply b n1))) (multiply b n1) (eq_ind_r A (multiply n1 (add b b)) (\lambda x:A.(eq A (multiply (multiply b n1) n1) x)) (eq_ind_r A (multiply n1 (add b b)) (\lambda x:A.(eq A (multiply x n1) (multiply n1 (add b b)))) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (multiply (multiply n1 (add b b)) n1) x)) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (multiply x n1) (add (multiply b n1) (multiply b n1)))) (H8 (multiply b n1)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply b n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1)))) (multiply b n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))))) b (eq_ind A (pixley ? ? b) (\lambda x:A.(eq A x (add (multiply ? (inverse ?)) (multiply b n1)))) (eq_ind A (add ? (inverse ?)) (\lambda x:A.(eq A (pixley ? ? b) (add (multiply ? (inverse ?)) (multiply b x)))) (eq_ind_r A (add (multiply ? b) (multiply (inverse ?) b)) (\lambda x:A.(eq A (pixley ? ? b) (add (multiply ? (inverse ?)) x))) (H3 ? ? b) (multiply b (add ? (inverse ?))) (H5 b ? (inverse ?))) n1 (H4 ?)) b (H2 ? b))).
+focus 319. clearbody k1.
+letin k2 \def (eq_ind A (multiply (add a n1) n1) (\lambda x:A.(eq A x (add a n1))) (eq_ind_r A (add (multiply ? (inverse ?)) (multiply (add a n1) n1)) (\lambda x:A.(eq A (multiply (add a n1) n1) x)) (eq_ind A (multiply (multiply (add a n1) n1) n1) (\lambda x:A.(eq A (multiply (add a n1) n1) (add (multiply ? (inverse ?)) x))) (eq_ind A (pixley ? ? (multiply (add a n1) n1)) (\lambda x:A.(eq A x (add (multiply ? (inverse ?)) (multiply (multiply (add a n1) n1) n1)))) (eq_ind A (add ? (inverse ?)) (\lambda x:A.(eq A (pixley ? ? (multiply (add a n1) n1)) (add (multiply ? (inverse ?)) (multiply (multiply (add a n1) n1) x)))) (eq_ind_r A (add (multiply ? (multiply (add a n1) n1)) (multiply (inverse ?) (multiply (add a n1) n1))) (\lambda x:A.(eq A (pixley ? ? (multiply (add a n1) n1)) (add (multiply ? (inverse ?)) x))) (H3 ? ? (multiply (add a n1) n1)) (multiply (multiply (add a n1) n1) (add ? (inverse ?))) (H5 (multiply (add a n1) n1) ? (inverse ?))) n1 (H4 ?)) (multiply (add a n1) n1) (H2 ? (multiply (add a n1) n1))) (multiply (add a n1) n1) (eq_ind_r A (multiply n1 (add (add a n1) (add a n1))) (\lambda x:A.(eq A (multiply (multiply (add a n1) n1) n1) x)) (eq_ind_r A (multiply n1 (add (add a n1) (add a n1))) (\lambda x:A.(eq A (multiply x n1) (multiply n1 (add (add a n1) (add a n1))))) (eq_ind_r A (add (multiply (add a n1) n1) (multiply (add a n1) n1)) (\lambda x:A.(eq A (multiply (multiply n1 (add (add a n1) (add a n1))) n1) x)) (eq_ind_r A (add (multiply (add a n1) n1) (multiply (add a n1) n1)) (\lambda x:A.(eq A (multiply x n1) (add (multiply (add a n1) n1) (multiply (add a n1) n1)))) (H8 (multiply (add a n1) n1)) (multiply n1 (add (add a n1) (add a n1))) (H5 n1 (add a n1) (add a n1))) (multiply n1 (add (add a n1) (add a n1))) (H5 n1 (add a n1) (add a n1))) (multiply (add a n1) n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply (add a n1) x) (multiply n1 (add (add a n1) (add a n1))))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply (add a n1) (add n1 n1)) (multiply x (add (add a n1) (add a n1))))) (eq_ind_r A (add (multiply (add a n1) (add n1 n1)) (multiply (add a n1) (add n1 n1))) (\lambda x:A.(eq A (multiply (add a n1) (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (\lambda x:A.(eq A (multiply (add a n1) (add n1 n1)) (add (multiply (add a n1) (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (\lambda x:A.(eq A x (add (multiply (add a n1) (add n1 n1)) (add (multiply n1 (add a n1)) (multiply n1 (add a n1)))))) (eq_ind_r A (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (\lambda x:A.(eq A (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (add x (add (multiply n1 (add a n1)) (multiply n1 (add a n1)))))) (eq_ind A (multiply (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) n1) (\lambda x:A.(eq A x (add (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (add (multiply n1 (add a n1)) (multiply n1 (add a n1)))))) (H7 (multiply n1 (add a n1))) (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (H8 (multiply n1 (add a n1)))) (multiply (add a n1) (add n1 n1)) (H5 (add a n1) n1 n1)) (multiply (add a n1) (add n1 n1)) (H5 (add a n1) n1 n1)) (multiply (add a n1) (add n1 n1)) (H5 (add a n1) n1 n1)) (multiply (add n1 n1) (add (add a n1) (add a n1))) (H5 (add n1 n1) (add a n1) (add a n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1)))) (multiply (add a n1) n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply (add a n1) x) (multiply n1 (add (add a n1) (add a n1))))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply (add a n1) (add n1 n1)) (multiply x (add (add a n1) (add a n1))))) (eq_ind_r A (add (multiply (add a n1) (add n1 n1)) (multiply (add a n1) (add n1 n1))) (\lambda x:A.(eq A (multiply (add a n1) (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (\lambda x:A.(eq A (multiply (add a n1) (add n1 n1)) (add (multiply (add a n1) (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (\lambda x:A.(eq A x (add (multiply (add a n1) (add n1 n1)) (add (multiply n1 (add a n1)) (multiply n1 (add a n1)))))) (eq_ind_r A (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (\lambda x:A.(eq A (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (add x (add (multiply n1 (add a n1)) (multiply n1 (add a n1)))))) (eq_ind A (multiply (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) n1) (\lambda x:A.(eq A x (add (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (add (multiply n1 (add a n1)) (multiply n1 (add a n1)))))) (H7 (multiply n1 (add a n1))) (add (multiply n1 (add a n1)) (multiply n1 (add a n1))) (H8 (multiply n1 (add a n1)))) (multiply (add a n1) (add n1 n1)) (H5 (add a n1) n1 n1)) (multiply (add a n1) (add n1 n1)) (H5 (add a n1) n1 n1)) (multiply (add a n1) (add n1 n1)) (H5 (add a n1) n1 n1)) (multiply (add n1 n1) (add (add a n1) (add a n1))) (H5 (add n1 n1) (add a n1) (add a n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))))) (add a n1) (eq_ind A (pixley ? ? (add a n1)) (\lambda x:A.(eq A x (add (multiply ? (inverse ?)) (multiply (add a n1) n1)))) (eq_ind A (add ? (inverse ?)) (\lambda x:A.(eq A (pixley ? ? (add a n1)) (add (multiply ? (inverse ?)) (multiply (add a n1) x)))) (eq_ind_r A (add (multiply ? (add a n1)) (multiply (inverse ?) (add a n1))) (\lambda x:A.(eq A (pixley ? ? (add a n1)) (add (multiply ? (inverse ?)) x))) (H3 ? ? (add a n1)) (multiply (add a n1) (add ? (inverse ?))) (H5 (add a n1) ? (inverse ?))) n1 (H4 ?)) (add a n1) (H2 ? (add a n1)))) n1 (H6 a n1)).
+focus 476. clearbody k2.
+letin k3 \def (eq_ind_r A (add (multiply ? (inverse ?)) (multiply b n1)) (\lambda x:A.(eq A (multiply b n1) x)) (eq_ind A (multiply (multiply b n1) n1) (\lambda x:A.(eq A (multiply b n1) (add (multiply ? (inverse ?)) x))) (eq_ind A (pixley ? ? (multiply b n1)) (\lambda x:A.(eq A x (add (multiply ? (inverse ?)) (multiply (multiply b n1) n1)))) (eq_ind A (add ? (inverse ?)) (\lambda x:A.(eq A (pixley ? ? (multiply b n1)) (add (multiply ? (inverse ?)) (multiply (multiply b n1) x)))) (eq_ind_r A (add (multiply ? (multiply b n1)) (multiply (inverse ?) (multiply b n1))) (\lambda x:A.(eq A (pixley ? ? (multiply b n1)) (add (multiply ? (inverse ?)) x))) (H3 ? ? (multiply b n1)) (multiply (multiply b n1) (add ? (inverse ?))) (H5 (multiply b n1) ? (inverse ?))) n1 (H4 ?)) (multiply b n1) (H2 ? (multiply b n1))) (multiply b n1) (eq_ind_r A (multiply n1 (add b b)) (\lambda x:A.(eq A (multiply (multiply b n1) n1) x)) (eq_ind_r A (multiply n1 (add b b)) (\lambda x:A.(eq A (multiply x n1) (multiply n1 (add b b)))) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (multiply (multiply n1 (add b b)) n1) x)) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (multiply x n1) (add (multiply b n1) (multiply b n1)))) (H8 (multiply b n1)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply b n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1)))) (multiply b n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))))) b (eq_ind A (pixley ? ? b) (\lambda x:A.(eq A x (add (multiply ? (inverse ?)) (multiply b n1)))) (eq_ind A (add ? (inverse ?)) (\lambda x:A.(eq A (pixley ? ? b) (add (multiply ? (inverse ?)) (multiply b x)))) (eq_ind_r A (add (multiply ? b) (multiply (inverse ?) b)) (\lambda x:A.(eq A (pixley ? ? b) (add (multiply ? (inverse ?)) x))) (H3 ? ? b) (multiply b (add ? (inverse ?))) (H5 b ? (inverse ?))) n1 (H4 ?)) b (H2 ? b))).
+focus 633. clearbody k3.
+exact
+(eq_ind A b (\lambda x:A.(eq A x b)) (refl_equal A b) (add (multiply a b) b) (eq_ind A (multiply b n1) (\lambda x:A.(eq A x (add (multiply a b) b))) (eq_ind_r A (add a n1) (\lambda x:A.(eq A (multiply b x) (add (multiply a b) b))) (eq_ind_r A (multiply n1 b) (\lambda x:A.(eq A (multiply b (add a n1)) (add (multiply a b) x))) (H5 b a n1) b (eq_ind A (multiply b n1) (\lambda x:A.(eq A b (multiply n1 x))) (eq_ind A (multiply b n1) (\lambda x:A.(eq A x (multiply n1 (multiply b n1)))) (eq_ind_r A (add b b) (\lambda x:A.(eq A (multiply b n1) (multiply n1 x))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) (multiply b n1) (eq_ind_r A (multiply n1 (add b b)) (\lambda x:A.(eq A x (add b b))) (eq_ind A (multiply (add b b) n1) (\lambda x:A.(eq A (multiply n1 (add b b)) x)) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply n1 (add b b)) (multiply (add b b) x))) (eq_ind_r A (add (multiply n1 (add b b)) (multiply n1 (add b b))) (\lambda x:A.(eq A (multiply n1 (add b b)) x)) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (multiply n1 (add b b)) (add (multiply n1 (add b b)) x))) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A x (add (multiply n1 (add b b)) (add (multiply b n1) (multiply b n1))))) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (add (multiply b n1) (multiply b n1)) (add x (add (multiply b n1) (multiply b n1))))) (eq_ind A (multiply (add (multiply b n1) (multiply b n1)) n1) (\lambda x:A.(eq A x (add (add (multiply b n1) (multiply b n1)) (add (multiply b n1) (multiply b n1))))) (H7 (multiply b n1)) (add (multiply b n1) (multiply b n1)) (H8 (multiply b n1))) (multiply n1 (add b b)) (H5 n1 b b)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply (add b b) (add n1 n1)) (H5 (add b b) n1 n1)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) (add b b) (H8 b)) (multiply b n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))))) b ?) b ?)) n1 ?) b ?)).
+auto.
+auto.
+auto.
+auto.
+unfocus.
+auto.
+unfocus.
+auto.
+unfocus.
+auto.
+unfocus.
+auto.
+qed.