1 set "baseuri" "cic:/matita/TPTP/BOO024-1".
2 include "../legacy/coq.ma".
3 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
4 (* Inclusion of: BOO024-1.p *)
5 (* -------------------------------------------------------------------------- *)
6 (* File : BOO024-1 : TPTP v3.1.1. Released v2.2.0. *)
7 (* Domain : Boolean Algebra *)
8 (* Problem : Half of Padmanabhan's 6-basis with Pixley, part 2. *)
9 (* Version : [MP96] (equality) axioms : Especial. *)
10 (* English : Part 2 (of 3) of the proof that half of Padmanaban's self-dual *)
11 (* independent 6-basis for Boolean Algebra, together with a Pixley *)
12 (* polynomial, is a basis for Boolean algebra. *)
13 (* Refs : [McC98] McCune (1998), Email to G. Sutcliffe *)
14 (* : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq *)
15 (* Source : [McC98] *)
16 (* Names : DUAL-BA-2-b [MP96] *)
17 (* Status : Unsatisfiable *)
18 (* Rating : 0.00 v2.2.1 *)
19 (* Syntax : Number of clauses : 8 ( 0 non-Horn; 8 unit; 1 RR) *)
20 (* Number of atoms : 8 ( 8 equality) *)
21 (* Maximal clause size : 1 ( 1 average) *)
22 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
23 (* Number of functors : 7 ( 3 constant; 0-3 arity) *)
24 (* Number of variables : 15 ( 2 singleton) *)
25 (* Maximal term depth : 5 ( 2 average) *)
27 (* -------------------------------------------------------------------------- *)
28 (* ----Half of Padmanabhan's self-dual independent 6-basis for Boolean Algebra: *)
29 (* ----pixley(X,Y,Z) is a Pixley polynomial: *)
30 (* ----Denial of conclusion: *)
32 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
33 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
34 alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
35 alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
36 alias id "sym_eq" = "cic:/Coq/Init/Logic/sym_eq.con".
37 alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
39 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))))).
40 \forall HH:(\forall x:A.eq A (multiply (add x x) n1) (add (add x x) (add x x))).
41 \forall HH1:(\forall x:A.eq A (multiply (add x x) n1) (add x x)).
42 ((eq) (A) ((add) ((multiply) (a) (b)) (b)) (b)))))))))))))))) .
44 (* sotto termine piu' piccolo, comunque lentissimo *)
45 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))).
46 focus 162. clearbody k.
47 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))).
48 focus 319. clearbody k1.
49 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)).
50 focus 476. clearbody k2.
51 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))).
52 focus 633. clearbody k3.
54 (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 ?)).
projects / helm.git / blob