From dd759c366bc713e36e8405ff6b9534fdff0885e9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 26 May 2006 12:46:32 +0000 Subject: [PATCH] Recently introduced bug in CicRefine.eat_prods fixed: a whd was now missing. Added a test to verify the performances of refinement. --- components/cic_unification/cicRefine.ml | 2 +- matita/tests/hard_refine.ma | 67 +++++++++++++++++++++++++ 2 files changed, 68 insertions(+), 1 deletion(-) create mode 100644 matita/tests/hard_refine.ma diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index e99ce5cd7..90643164d 100644 --- 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 index 000000000..b528414df --- /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. -- 2.39.2