From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 May 2006 12:46:32 +0000 (+0000)
Subject: Recently introduced bug in CicRefine.eat_prods fixed: a whd was now missing.
X-Git-Tag: make_still_working~7321
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=098d4ba18dfe92d25cb5e513231d952d14938bb6;p=helm.git

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/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index e99ce5cd7..90643164d 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/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/helm/software/matita/tests/hard_refine.ma b/helm/software/matita/tests/hard_refine.ma
new file mode 100644
index 000000000..b528414df
--- /dev/null
+++ b/helm/software/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.