+∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply X Y (inverse Y)) X.
+∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply (inverse Y) Y X) X.
+∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply X X Y) X.
+∀H3:∀X:Univ.∀Y:Univ.eq Univ (multiply Y X X) X.
+∀H4:∀V:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply V W X) Y (multiply V W Z)) (multiply V W (multiply X Y Z)).eq Univ (inverse (inverse a)) a
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply (inverse Y) Y X) X.
+∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply X X Y) X.
+∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply Y X X) X.
+∀H3:∀V:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply V W X) Y (multiply V W Z)) (multiply V W (multiply X Y Z)).eq Univ (multiply a (inverse a) b) b
+∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply (inverse Y) Y X) X.
+∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply X X Y) X.
+∀H3:∀X:Univ.∀Y:Univ.eq Univ (multiply Y X X) X.
+∀H4:∀V:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply V W X) Y (multiply V W Z)) (multiply V W (multiply X Y Z)).eq Univ (multiply a (inverse a) b) b
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply X Y (inverse Y)) X.
+∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply (inverse Y) Y X) X.
+∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply X X Y) X.
+∀H3:∀V:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply V W X) Y (multiply V W Z)) (multiply V W (multiply X Y Z)).eq Univ (multiply y x x) x
+(* ----3 properties of Boolean algebra and the corresponding duals. *)
+
+(* ----Existence of 0 and 1. *)
+
+(* ----Associativity of the 2 operations. *)
+
+(* ----Denial of conclusion: *)
+ntheorem prove_multiply_add_property:
+ ∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
+∀a:Univ.
+∀add:∀_:Univ.∀_:Univ.Univ.
+∀b:Univ.
+∀c:Univ.
+∀inverse:∀_:Univ.Univ.
+∀multiply:∀_:Univ.∀_:Univ.Univ.
+∀n0:Univ.
+∀n1:Univ.
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (add X Y) Z) (add X (add Y Z)).
+∀H2:∀X:Univ.eq Univ (multiply X (inverse X)) n0.
+∀H3:∀X:Univ.eq Univ (add X (inverse X)) n1.
+∀H4:∀X:Univ.∀Y:Univ.eq Univ (add (multiply X (inverse X)) Y) Y.
+∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply (add X Y) (add Y Z)) Y) Y.
+∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y (add X Z))) X.
+∀H7:∀X:Univ.∀Y:Univ.eq Univ (multiply (add X (inverse X)) Y) Y.
+∀H8:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (add (multiply X Y) (multiply Y Z)) Y) Y.
+∀H9:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (multiply Y (multiply X Z))) X.
+∀H10:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (multiply X Y) (add (multiply Y Z) (multiply Z X))) (multiply (add X Y) (multiply (add Y Z) (add Z X))).eq Univ (multiply a (add b c)) (add (multiply b a) (multiply c a))
+(* ----3 properties of Boolean algebra and the corresponding duals. *)
+
+(* ----Majority polynomials: *)
+
+(* ----A simple propery of Boolean Algebra fails to hold. *)
+ntheorem prove_inverse_involution:
+ ∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
+∀a:Univ.
+∀add:∀_:Univ.∀_:Univ.Univ.
+∀inverse:∀_:Univ.Univ.
+∀multiply:∀_:Univ.∀_:Univ.Univ.
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply (add (multiply X Y) Y) (add X Y)) Y.
+∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply (add (multiply X X) Y) (add X X)) X.
+∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply (add (multiply X Y) X) (add X Y)) X.
+∀H3:∀X:Univ.∀Y:Univ.eq Univ (multiply (add X (inverse X)) Y) Y.
+∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (add (multiply X Y) (multiply Y Z)) Y) Y.
+∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (multiply Y (multiply X Z))) X.
+∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (multiply X Y) (add (multiply Y Z) (multiply Z X))) (multiply (add X Y) (multiply (add Y Z) (add Z X))).eq Univ (inverse (inverse a)) a
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply X Y (inverse Y)) X.
+∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply (inverse Y) Y X) X.
+∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply X X Y) X.
+∀H3:∀X:Univ.∀Y:Univ.eq Univ (multiply Y X X) X.
+∀H4:∀V:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply V W X) Y (multiply V W Z)) (multiply V W (multiply X Y Z)).eq Univ (multiply (multiply a (inverse a) b) (inverse (multiply (multiply c d e) f (multiply c d g))) (multiply d (multiply g f e) c)) b
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (multiply (multiply A (inverse A) B) (inverse (multiply (multiply C D E) F (multiply C D G))) (multiply D (multiply G F E) C)) B.eq Univ (multiply (multiply d e a) b (multiply d e c)) (multiply d e (multiply a b c))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (multiply (multiply A (inverse A) B) (inverse (multiply (multiply C D E) F (multiply C D G))) (multiply D (multiply G F E) C)) B.eq Univ (multiply b a a) a
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (multiply (multiply A (inverse A) B) (inverse (multiply (multiply C D E) F (multiply C D G))) (multiply D (multiply G F E) C)) B.eq Univ (multiply a b (inverse b)) a
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (multiply (multiply A (inverse A) B) (inverse (multiply (multiply C D E) F (multiply C D G))) (multiply D (multiply G F E) C)) B.eq Univ (multiply a a b) a
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (multiply (multiply A (inverse A) B) (inverse (multiply (multiply C D E) F (multiply C D G))) (multiply D (multiply G F E) C)) B.eq Univ (multiply (inverse b) b a) a
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (inverse (add (inverse (add (inverse (add A B)) C)) (inverse (add A (inverse (add (inverse C) (inverse (add C D)))))))) C.eq Univ (add b a) (add a b)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (inverse (add (inverse (add (inverse (add A B)) C)) (inverse (add A (inverse (add (inverse C) (inverse (add C D)))))))) C.eq Univ (add (add a b) c) (add a (add b c))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand A (nand (nand B A) A)) (nand B (nand C A))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand A (nand (nand B A) A)) (nand B (nand A C))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand A (nand A (nand B A))) (nand B (nand C A))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand A (nand A (nand A B))) (nand B (nand C A))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand A (nand A (nand A B))) (nand B (nand A C))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand A (nand A (nand B C))) (nand B (nand C A))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand A (nand A (nand B C))) (nand C (nand A B))) C.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand A (nand A (nand B B))) (nand B (nand C A))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand (nand A (nand A B)) A) (nand B (nand C A))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand (nand A (nand B B)) A) (nand B (nand C A))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand (nand A (nand B C)) A) (nand B (nand A C))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand (nand A (nand B C)) A) (nand C (nand A B))) C.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand (nand A (nand A B)) A) (nand B (nand A C))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand (nand (nand A B) A) A) (nand B (nand C A))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand (nand (nand A B) A) A) (nand B (nand A C))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand (nand (nand A B) C) C) (nand B (nand A C))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (nand (nand (nand (nand A B) C) C) (nand B (nand C A))) B.eq Univ (nand a (nand b (nand a c))) (nand (nand (nand c b) b) a)
+∀H0:∀X:Univ.eq Univ (apply (apply (apply s (apply b X)) i) (apply (apply s (apply b X)) i)) (apply x (apply (apply (apply s (apply b X)) i) (apply (apply s (apply b X)) i))).
+∀H1:∀X:Univ.eq Univ (apply i X) X.
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).
+∀H3:∀X:Univ.∀Y:Univ.eq Univ (apply (apply k X) Y) X.
+∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).∃Y:Univ.eq Univ Y (apply combinator Y)
+∀H0:∀X:Univ.eq Univ (weak_fixed_point X) (apply (apply (apply s (apply c (apply b X))) (apply s (apply c (apply b X)))) (apply s (apply c (apply b X)))).
+∀H1:∀X:Univ.eq Univ (apply i X) X.
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply c X) Y) Z) (apply (apply X Z) Y).
+∀H3:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).
+∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).eq Univ (weak_fixed_point fixed_pt) (apply fixed_pt (weak_fixed_point fixed_pt))
+∀H1:∀X:Univ.∀Y:Univ.eq Univ (apply (apply w X) Y) (apply (apply X Y) Y).
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).fixed_point (apply (apply b (apply w w)) (apply (apply b w) (apply (apply b b) b)))
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply k X) Y) X.
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).eq Univ (apply (apply (apply (apply s (apply k (apply s (apply (apply s k) k)))) (apply (apply s (apply (apply s k) k)) (apply (apply s k) k))) x) y) (apply y (apply (apply x x) y))
+∀H0:eq Univ strong_fixed_point (apply (apply s (apply k (apply (apply s (apply (apply s k) k)) (apply (apply s k) k)))) (apply (apply s (apply k (apply (apply s s) (apply s k)))) (apply (apply s (apply k s)) k))).
+∀H1:∀X:Univ.∀Y:Univ.eq Univ (apply (apply k X) Y) X.
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).eq Univ (apply strong_fixed_point fixed_pt) (apply fixed_pt (apply strong_fixed_point fixed_pt))
+∀H0:eq Univ strong_fixed_point (apply (apply s (apply k (apply (apply s (apply (apply s k) k)) (apply (apply s k) k)))) (apply (apply s (apply (apply s (apply k s)) k)) (apply k (apply (apply s (apply (apply s k) k)) (apply (apply s k) k))))).
+∀H1:∀X:Univ.∀Y:Univ.eq Univ (apply (apply k X) Y) X.
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).eq Univ (apply strong_fixed_point fixed_pt) (apply fixed_pt (apply strong_fixed_point fixed_pt))
+∀H0:eq Univ strong_fixed_point (apply (apply s (apply k (apply (apply (apply s s) (apply (apply s k) k)) (apply (apply s s) (apply s k))))) (apply (apply s (apply k s)) k)).
+∀H1:∀X:Univ.∀Y:Univ.eq Univ (apply (apply k X) Y) X.
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).eq Univ (apply strong_fixed_point fixed_pt) (apply fixed_pt (apply strong_fixed_point fixed_pt))
+∀H0:eq Univ strong_fixed_point (apply (apply b (apply (apply b (apply (apply h (apply (apply b (apply (apply b h) (apply b b))) (apply h (apply (apply b h) (apply b b))))) h)) b)) b).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply h X) Y) Z) (apply (apply (apply X Y) Z) Y).
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply strong_fixed_point fixed_pt) (apply fixed_pt (apply strong_fixed_point fixed_pt))
+∀H0:eq Univ strong_fixed_point (apply (apply b (apply (apply b (apply (apply n (apply (apply b b) (apply (apply n (apply (apply b b) n)) n))) n)) b)) b).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply n X) Y) Z) (apply (apply (apply X Z) Y) Z).
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply strong_fixed_point fixed_pt) (apply fixed_pt (apply strong_fixed_point fixed_pt))
+∀H0:eq Univ strong_fixed_point (apply (apply b (apply (apply b (apply (apply n (apply (apply b b) (apply (apply n (apply n (apply b b))) n))) n)) b)) b).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply n X) Y) Z) (apply (apply (apply X Z) Y) Z).
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply strong_fixed_point fixed_pt) (apply fixed_pt (apply strong_fixed_point fixed_pt))
+∀H0:eq Univ strong_fixed_point (apply (apply b (apply (apply b (apply (apply n (apply n (apply (apply b (apply b b)) (apply n (apply (apply b b) n))))) n)) b)) b).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply n X) Y) Z) (apply (apply (apply X Z) Y) Z).
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply strong_fixed_point fixed_pt) (apply fixed_pt (apply strong_fixed_point fixed_pt))
+∀H0:eq Univ strong_fixed_point (apply (apply b (apply (apply b (apply (apply n (apply n (apply (apply b (apply b b)) (apply n (apply n (apply b b)))))) n)) b)) b).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply n X) Y) Z) (apply (apply (apply X Z) Y) Z).
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply strong_fixed_point fixed_pt) (apply fixed_pt (apply strong_fixed_point fixed_pt))
+(* ----Hypothesis: For all birds x, y, and z, there exists a bird u such *)
+
+(* ----that for all w, uw = x(y(zw)). *)
+
+(* ----Finding clause (using xy to replace response(x,y)): *)
+
+(* ---- - (FAx FAy FAz TEu FAw (uw = x(y(zw)))). *)
+
+(* ---- TEx TEy TEz FAu TEw -(uw = x(y(zw))). *)
+
+(* ---- Letting w = f(u), x = A, y = B, and z = C, *)
+
+(* ---- -[(u)f(u) = A(B((C)f(u)))]. *)
+ntheorem prove_bird_exists:
+ ∀Univ:Type.∀U:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.
+∀a:Univ.
+∀b:Univ.
+∀c:Univ.
+∀compose:∀_:Univ.∀_:Univ.Univ.
+∀f:∀_:Univ.Univ.
+∀response:∀_:Univ.∀_:Univ.Univ.
+∀H0:∀W:Univ.∀X:Univ.∀Y:Univ.eq Univ (response (compose X Y) W) (response X (response Y W)).∃U:Univ.eq Univ (response U (f U)) (response a (response b (response c (f U))))
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t b)) (apply (apply b b) t)) x) y) z) (apply y (apply x z))
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t b)) b)) t) x) y) z) (apply y (apply x z))
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t t)) (apply (apply b b) b)) x) y) z) (apply x (apply z y))
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t t)) b)) b) x) y) z) (apply x (apply z y))
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b b) t)) x) y) z) (apply (apply x z) y)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t (apply (apply b b) t))) b)) t) x) y) z) (apply (apply x z) y)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t t)) (apply (apply b b) (apply (apply b b) t))) x) y) z) (apply (apply z y) x)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t t)) b)) (apply (apply b b) t)) x) y) z) (apply (apply z y) x)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t t)) (apply (apply b (apply (apply b b) b)) t)) x) y) z) (apply (apply z y) x)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t t)) (apply (apply b b) b))) t) x) y) z) (apply (apply z y) x)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b b) (apply (apply b b) t))) x) y) z) (apply (apply z x) y)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t (apply (apply b b) t))) b)) (apply (apply b b) t)) x) y) z) (apply (apply z x) y)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b (apply (apply b b) b)) t)) x) y) z) (apply (apply z x) y)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b b) b))) t) x) y) z) (apply (apply z x) y)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply (apply b (apply t (apply (apply b b) t))) b)) b)) t) x) y) z) (apply (apply z x) y)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b b) (apply (apply b t) t))) x) y) z) (apply (apply z x) y)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t (apply (apply b b) t))) b)) (apply (apply b t) t)) x) y) z) (apply (apply z x) y)
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply t X) Y) (apply Y X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b (apply (apply b b) t)) t)) x) y) z) (apply (apply z x) y)
+∀H0:∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (inverse (multiply (multiply (inverse (multiply (inverse Y) (multiply (inverse X) W))) Z) (inverse (multiply Y Z))))) W.eq Univ (multiply a (multiply b c)) (multiply (multiply a b) c)
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (multiply (multiply X (multiply (multiply X Y) Z)) (multiply identity (multiply Z Z)))) Y.eq Univ (multiply a (multiply a a)) identity
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (multiply (multiply X (multiply (multiply X Y) Z)) (multiply identity (multiply Z Z)))) Y.eq Univ (multiply identity a) a
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (multiply (multiply X (multiply (multiply X Y) Z)) (multiply identity (multiply Z Z)))) Y.eq Univ (multiply a identity) a
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (multiply (multiply X (multiply (multiply X Y) Z)) (multiply identity (multiply Z Z)))) Y.eq Univ (multiply (multiply a b) c) (multiply a (multiply b c))
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Y (multiply (multiply Y (multiply (multiply Y Y) (multiply X Z))) (multiply Z (multiply Z Z)))) X.eq Univ (multiply a (multiply a (multiply a a))) identity
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Y (multiply (multiply Y (multiply (multiply Y Y) (multiply X Z))) (multiply Z (multiply Z Z)))) X.eq Univ (multiply identity a) a
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Y (multiply (multiply Y (multiply (multiply Y Y) (multiply X Z))) (multiply Z (multiply Z Z)))) X.eq Univ (multiply a identity) a
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Y (multiply (multiply Y (multiply (multiply Y Y) (multiply X Z))) (multiply Z (multiply Z Z)))) X.eq Univ (multiply (multiply a b) c) (multiply a (multiply b c))
+∀H14:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound a (greatest_lower_bound b c)) (greatest_lower_bound (least_upper_bound a b) (least_upper_bound a c))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#c.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14;
+∀H14:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound a (least_upper_bound b c)) (least_upper_bound (greatest_lower_bound a b) (greatest_lower_bound a c))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#c.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14;
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (greatest_lower_bound X (least_upper_bound Y Z)) (least_upper_bound (greatest_lower_bound X Y) (greatest_lower_bound X Z)).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (least_upper_bound X (greatest_lower_bound Y Z)) (greatest_lower_bound (least_upper_bound X Y) (least_upper_bound X Z)).
+∀H2:∀X:Univ.eq Univ (negative_part X) (greatest_lower_bound X identity).
+∀H3:∀X:Univ.eq Univ (positive_part X) (least_upper_bound X identity).
+∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (greatest_lower_bound Y Z) X) (greatest_lower_bound (multiply Y X) (multiply Z X)).
+∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (least_upper_bound Y Z) X) (least_upper_bound (multiply Y X) (multiply Z X)).
+∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (greatest_lower_bound Y Z)) (greatest_lower_bound (multiply X Y) (multiply X Z)).
+∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (least_upper_bound Y Z)) (least_upper_bound (multiply X Y) (multiply X Z)).
+∀H8:∀X:Univ.∀Y:Univ.eq Univ (greatest_lower_bound X (least_upper_bound X Y)) X.
+∀H9:∀X:Univ.∀Y:Univ.eq Univ (least_upper_bound X (greatest_lower_bound X Y)) X.
+∀H10:∀X:Univ.eq Univ (greatest_lower_bound X X) X.
+∀H11:∀X:Univ.eq Univ (least_upper_bound X X) X.
+∀H12:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (least_upper_bound X (least_upper_bound Y Z)) (least_upper_bound (least_upper_bound X Y) Z).
+∀H13:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (greatest_lower_bound X (greatest_lower_bound Y Z)) (greatest_lower_bound (greatest_lower_bound X Y) Z).
+∀H14:∀X:Univ.∀Y:Univ.eq Univ (least_upper_bound X Y) (least_upper_bound Y X).
+∀H15:∀X:Univ.∀Y:Univ.eq Univ (greatest_lower_bound X Y) (greatest_lower_bound Y X).
+∀H16:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (greatest_lower_bound X (least_upper_bound Y Z)) (least_upper_bound (greatest_lower_bound X Y) (greatest_lower_bound X Z)).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (least_upper_bound X (greatest_lower_bound Y Z)) (greatest_lower_bound (least_upper_bound X Y) (least_upper_bound X Z)).
+∀H2:∀X:Univ.eq Univ (negative_part X) (greatest_lower_bound X identity).
+∀H3:∀X:Univ.eq Univ (positive_part X) (least_upper_bound X identity).
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (greatest_lower_bound X (least_upper_bound Y Z)) (least_upper_bound (greatest_lower_bound X Y) (greatest_lower_bound X Z)).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (least_upper_bound X (greatest_lower_bound Y Z)) (greatest_lower_bound (least_upper_bound X Y) (least_upper_bound X Z)).
+∀H2:∀X:Univ.eq Univ (negative_part X) (greatest_lower_bound X identity).
+∀H3:∀X:Univ.eq Univ (positive_part X) (least_upper_bound X identity).
+∀H4:∀A:Univ.∀B:Univ.eq Univ (inverse (least_upper_bound A B)) (greatest_lower_bound (inverse A) (inverse B)).
+∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (greatest_lower_bound Y Z) X) (greatest_lower_bound (multiply Y X) (multiply Z X)).
+∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (least_upper_bound Y Z) X) (least_upper_bound (multiply Y X) (multiply Z X)).
+∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (greatest_lower_bound Y Z)) (greatest_lower_bound (multiply X Y) (multiply X Z)).
+∀H8:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (least_upper_bound Y Z)) (least_upper_bound (multiply X Y) (multiply X Z)).
+∀H9:∀X:Univ.∀Y:Univ.eq Univ (greatest_lower_bound X (least_upper_bound X Y)) X.
+∀H10:∀X:Univ.∀Y:Univ.eq Univ (least_upper_bound X (greatest_lower_bound X Y)) X.
+∀H11:∀X:Univ.eq Univ (greatest_lower_bound X X) X.
+∀H12:∀X:Univ.eq Univ (least_upper_bound X X) X.
+∀H13:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (least_upper_bound X (least_upper_bound Y Z)) (least_upper_bound (least_upper_bound X Y) Z).
+∀H14:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (greatest_lower_bound X (greatest_lower_bound Y Z)) (greatest_lower_bound (greatest_lower_bound X Y) Z).
+∀H15:∀X:Univ.∀Y:Univ.eq Univ (least_upper_bound X Y) (least_upper_bound Y X).
+∀H16:∀X:Univ.∀Y:Univ.eq Univ (greatest_lower_bound X Y) (greatest_lower_bound Y X).
+∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).
+∀H15:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (multiply (inverse c) (multiply a c)) (multiply (inverse c) (multiply b c))) (multiply (inverse c) (multiply b c))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#c.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15;
+∀H15:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (multiply (inverse c) (multiply a c)) (multiply (inverse c) (multiply b c))) (multiply (inverse c) (multiply a c))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#c.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15;
+∀H14:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (multiply c (multiply (least_upper_bound a b) d)) (least_upper_bound (multiply c (multiply a d)) (multiply c (multiply b d)))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#c.
+#d.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14;
+∀H15:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (multiply c (multiply (least_upper_bound a b) d)) (least_upper_bound (multiply c (multiply a d)) (multiply c (multiply b d)))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#c.
+#d.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15;
+∀H17:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (greatest_lower_bound a (multiply b c)) (multiply (greatest_lower_bound a b) (greatest_lower_bound a c))) (multiply (greatest_lower_bound a b) (greatest_lower_bound a c))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#c.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17;
+∀H17:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (greatest_lower_bound a (multiply b c)) (multiply (greatest_lower_bound a b) (greatest_lower_bound a c))) (greatest_lower_bound a (multiply b c))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#c.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17;
+∀H14:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (least_upper_bound (multiply a b) identity) (multiply (least_upper_bound a identity) (least_upper_bound b identity))) (multiply (least_upper_bound a identity) (least_upper_bound b identity))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14;
+∀H17:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (least_upper_bound (multiply a b) identity) (multiply (least_upper_bound a identity) (least_upper_bound b identity))) (multiply (least_upper_bound a identity) (least_upper_bound b identity))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17;
+∀H14:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (least_upper_bound (multiply a b) identity) (multiply (least_upper_bound a identity) (least_upper_bound b identity))) (least_upper_bound (multiply a b) identity)
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14;
+∀H17:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (least_upper_bound (multiply a b) identity) (multiply (least_upper_bound a identity) (least_upper_bound b identity))) (least_upper_bound (multiply a b) identity)
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17;
+∀H14:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (multiply a b) identity) (multiply a (inverse (greatest_lower_bound a (inverse b))))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14;
+∀H17:∀X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (multiply a b) identity) (multiply a (inverse (greatest_lower_bound a (inverse b))))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#greatest_lower_bound.
+#identity.
+#inverse.
+#least_upper_bound.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17;
+∀H0:eq Univ (least_upper_bound (greatest_lower_bound a (multiply b c)) (multiply (greatest_lower_bound a b) (greatest_lower_bound a c))) (multiply (greatest_lower_bound a b) (greatest_lower_bound a c)).
+∀H1:eq Univ (greatest_lower_bound a b) identity.
+∀H2:eq Univ (least_upper_bound identity c) c.
+∀H3:eq Univ (least_upper_bound identity b) b.
+∀H4:eq Univ (least_upper_bound identity a) a.
+∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (greatest_lower_bound Y Z) X) (greatest_lower_bound (multiply Y X) (multiply Z X)).
+∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (least_upper_bound Y Z) X) (least_upper_bound (multiply Y X) (multiply Z X)).
+∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (greatest_lower_bound Y Z)) (greatest_lower_bound (multiply X Y) (multiply X Z)).
+∀H8:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (least_upper_bound Y Z)) (least_upper_bound (multiply X Y) (multiply X Z)).
+∀H9:∀X:Univ.∀Y:Univ.eq Univ (greatest_lower_bound X (least_upper_bound X Y)) X.
+∀H10:∀X:Univ.∀Y:Univ.eq Univ (least_upper_bound X (greatest_lower_bound X Y)) X.
+∀H11:∀X:Univ.eq Univ (greatest_lower_bound X X) X.
+∀H12:∀X:Univ.eq Univ (least_upper_bound X X) X.
+∀H13:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (least_upper_bound X (least_upper_bound Y Z)) (least_upper_bound (least_upper_bound X Y) Z).
+∀H14:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (greatest_lower_bound X (greatest_lower_bound Y Z)) (greatest_lower_bound (greatest_lower_bound X Y) Z).
+∀H15:∀X:Univ.∀Y:Univ.eq Univ (least_upper_bound X Y) (least_upper_bound Y X).
+∀H16:∀X:Univ.∀Y:Univ.eq Univ (greatest_lower_bound X Y) (greatest_lower_bound Y X).
+∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).
+∀H0:eq Univ (greatest_lower_bound (greatest_lower_bound a (multiply b c)) (multiply (greatest_lower_bound a b) (greatest_lower_bound a c))) (greatest_lower_bound a (multiply b c)).
+∀H1:eq Univ (greatest_lower_bound a b) identity.
+∀H2:eq Univ (greatest_lower_bound identity c) identity.
+∀H3:eq Univ (greatest_lower_bound identity b) identity.
+∀H4:eq Univ (greatest_lower_bound identity a) identity.
+∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (greatest_lower_bound Y Z) X) (greatest_lower_bound (multiply Y X) (multiply Z X)).
+∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (least_upper_bound Y Z) X) (least_upper_bound (multiply Y X) (multiply Z X)).
+∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (greatest_lower_bound Y Z)) (greatest_lower_bound (multiply X Y) (multiply X Z)).
+∀H8:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (least_upper_bound Y Z)) (least_upper_bound (multiply X Y) (multiply X Z)).
+∀H9:∀X:Univ.∀Y:Univ.eq Univ (greatest_lower_bound X (least_upper_bound X Y)) X.
+∀H10:∀X:Univ.∀Y:Univ.eq Univ (least_upper_bound X (greatest_lower_bound X Y)) X.
+∀H11:∀X:Univ.eq Univ (greatest_lower_bound X X) X.
+∀H12:∀X:Univ.eq Univ (least_upper_bound X X) X.
+∀H13:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (least_upper_bound X (least_upper_bound Y Z)) (least_upper_bound (least_upper_bound X Y) Z).
+∀H14:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (greatest_lower_bound X (greatest_lower_bound Y Z)) (greatest_lower_bound (greatest_lower_bound X Y) Z).
+∀H15:∀X:Univ.∀Y:Univ.eq Univ (least_upper_bound X Y) (least_upper_bound Y X).
+∀H16:∀X:Univ.∀Y:Univ.eq Univ (greatest_lower_bound X Y) (greatest_lower_bound Y X).
+∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply X (multiply Y Y)) (multiply Y (multiply Y X)).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).eq Univ (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a b))))))) (multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b b)))))))
+∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply X (multiply Y (multiply Y Y))) (multiply Y (multiply Y (multiply Y X))).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).eq Univ (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a b))))))))))))))))) (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b (multiply b (multiply b (multiply b (multiply b (multiply b b)))))))))))))))))
+∀H0:∀U:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply U (inverse (multiply Y (multiply (multiply (multiply Z (inverse Z)) (inverse (multiply U Y))) U)))) U.eq Univ (multiply x (inverse (multiply y (multiply (multiply (multiply z (inverse z)) (inverse (multiply u y))) x)))) u
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (inverse (multiply A (multiply B (multiply (multiply (inverse B) C) (inverse (multiply D (multiply A C))))))) D.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (inverse (multiply A (multiply B (multiply (multiply (inverse B) C) (inverse (multiply D (multiply A C))))))) D.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (inverse (multiply A (multiply B (multiply (multiply (inverse B) C) (inverse (multiply D (multiply A C))))))) D.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
+∀H0:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).
+∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide (divide A A) B) C) (divide (divide (divide A A) A) C))) B.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).
+∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide (divide A A) B) C) (divide (divide (divide A A) A) C))) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
+∀H0:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).
+∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide (divide A A) B) C) (divide (divide (divide A A) A) C))) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
+∀H0:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).
+∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide (divide B B) B) C) (divide (divide (divide B B) A) C))) B.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).
+∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide (divide B B) B) C) (divide (divide (divide B B) A) C))) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
+∀H0:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).
+∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide (divide B B) B) C) (divide (divide (divide B B) A) C))) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
+∀H0:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).
+∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide (divide (divide A A) (divide A (divide B (divide (divide (divide A A) A) C)))) C) B.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).
+∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide (divide (divide A A) (divide A (divide B (divide (divide (divide A A) A) C)))) C) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
+∀H0:∀A:Univ.∀B:Univ.eq Univ (inverse A) (divide (divide B B) A).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (multiply A B) (divide A (divide (divide C C) B)).
+∀H2:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide (divide (divide A A) (divide A (divide B (divide (divide (divide A A) A) C)))) C) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide (divide identity (divide A (divide B (divide (divide (divide A A) A) C)))) C) B.eq Univ (multiply (inverse a1) a1) identity
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide (divide identity (divide A (divide B (divide (divide (divide A A) A) C)))) C) B.eq Univ (multiply identity a2) a2
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide (divide identity (divide A (divide B (divide (divide (divide A A) A) C)))) C) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide (divide (divide A A) (divide A (divide B (divide (divide identity A) C)))) C) B.eq Univ (multiply (inverse a1) a1) identity
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide (divide (divide A A) (divide A (divide B (divide (divide identity A) C)))) C) B.eq Univ (multiply identity a2) a2
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide (divide (divide A A) (divide A (divide B (divide (divide identity A) C)))) C) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide identity B) C) (divide (divide (divide A A) A) C))) B.eq Univ (multiply (inverse a1) a1) identity
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide identity B) C) (divide (divide (divide A A) A) C))) B.eq Univ (multiply identity a2) a2
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide identity B) C) (divide (divide (divide A A) A) C))) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide (divide A A) B) C) (divide (divide identity A) C))) B.eq Univ (multiply (inverse a1) a1) identity
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide (divide A A) B) C) (divide (divide identity A) C))) B.eq Univ (multiply identity a2) a2
+∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (divide A (divide (divide (divide (divide A A) B) C) (divide (divide identity A) C))) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (inverse B)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (divide (divide A A) (divide B (divide (divide C (divide D B)) (inverse D)))) C.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (inverse B)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (divide (inverse (divide A (divide B (divide C D)))) (divide (divide D C) A)) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (inverse B)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (divide (inverse (divide (divide (divide A B) C) (divide D C))) (divide B A)) D.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (inverse B)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (divide (inverse (divide (divide (divide A A) B) (divide C (divide B D)))) D) C.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (double_divide (double_divide (double_divide A (double_divide B identity)) (double_divide (double_divide C (double_divide D (double_divide D identity))) (double_divide A identity))) B) C.eq Univ (multiply (inverse a1) a1) identity
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (double_divide (double_divide (double_divide A (double_divide B identity)) (double_divide (double_divide C (double_divide D (double_divide D identity))) (double_divide A identity))) B) C.eq Univ (multiply identity a2) a2
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (double_divide (double_divide (double_divide A (double_divide B identity)) (double_divide (double_divide C (double_divide D (double_divide D identity))) (double_divide A identity))) B) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide A B) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply (inverse a1) a1) identity
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide A B) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply identity a2) a2
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.eq Univ (multiply (inverse (multiply (inverse (multiply (inverse (multiply A B)) (multiply B A))) (multiply (inverse (multiply C D)) (multiply C (inverse (multiply (multiply E (inverse F)) (inverse D))))))) F) E.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide A C)) (double_divide identity C))) (double_divide identity identity)) B.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide A C)) (double_divide C identity))) (double_divide identity identity)) B.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide C A)) (double_divide C identity))) (double_divide identity identity)) B.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide B A) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply (inverse a1) a1) identity
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide B A) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply identity a2) a2
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide B A) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.eq Univ identity (double_divide A (inverse A)).
+∀H1:∀A:Univ.eq Univ (inverse A) (double_divide A identity).
+∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (double_divide (double_divide B A) identity).
+∀H3:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide identity B) (double_divide C (double_divide B A)))) (double_divide identity identity)) C.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (inverse (double_divide B A)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide A (inverse (double_divide (inverse (double_divide (double_divide A B) (inverse C))) B))) C.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (inverse (double_divide B A)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (inverse (double_divide (double_divide A B) (inverse (double_divide A (inverse C))))) B) C.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (inverse (double_divide B A)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (inverse (double_divide (double_divide A B) (inverse (double_divide A (inverse (double_divide C B)))))) C.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (inverse (double_divide B A)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (double_divide A B) (inverse (double_divide A (inverse (double_divide (inverse C) B))))) C.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (inverse (double_divide B A)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (inverse (double_divide (inverse (double_divide A (inverse (double_divide B (double_divide A C))))) C)) B.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (inverse (double_divide B A)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (inverse (double_divide A (inverse (double_divide (inverse B) (double_divide A C))))) C) B.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (inverse (double_divide B A)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (inverse (double_divide (inverse (double_divide (inverse (double_divide A B)) C)) (double_divide A C))) B.eq Univ (multiply a b) (multiply b a)
+∀H0:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (inverse (double_divide B A)).
+∀H1:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (double_divide (inverse (double_divide (inverse (double_divide A (inverse B))) C)) (double_divide A C)) B.eq Univ (multiply a b) (multiply b a)
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (join X (meet Y Z)) (join Z (meet X Y))) (join (meet Z (join X (meet Y Z))) (meet X (join Y Z))).
+∀H1:∀U:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join X (meet Y (join Z (meet X U)))) (meet (join X (meet Y (join X Z))) (join X (meet (join X Y) (join Z U)))).
+∀H2:∀U:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet X (join Y (meet Z (join X U)))) (join (meet X (join Y (meet X Z))) (meet X (join (meet X Y) (meet Z U)))).
+∀H3:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join X Y) Z) (join X (join Y Z)).
+∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet X Y) Z) (meet X (meet Y Z)).
+∀H5:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
+∀H6:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
+∀H7:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.
+∀H8:∀X:Univ.∀Y:Univ.eq Univ (meet X (join X Y)) X.
+∀H9:∀X:Univ.eq Univ (join X X) X.
+∀H10:∀X:Univ.eq Univ (meet X X) X.eq Univ (meet a (meet (join b c) (join b d))) (meet (meet a (meet (join b c) (join b d))) (join (meet a (join b (meet c d))) (join (meet a c) (meet a d))))
+∀H3:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join X Y) Z) (join X (join Y Z)).
+∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet X Y) Z) (meet X (meet Y Z)).
+∀H5:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
+∀H6:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
+∀H7:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.
+∀H8:∀X:Univ.eq Univ (meet (complement X) X) n0.
+∀H9:∀X:Univ.eq Univ (join (complement X) X) n1.eq Univ (join a (join (meet (complement a) (meet (join a (complement b)) (join a b))) (meet (complement a) (join (meet (complement a) b) (meet (complement a) (complement b)))))) n1
+∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join X Y) Z) (join X (join Y Z)).
+∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet X Y) Z) (meet X (meet Y Z)).
+∀H7:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
+∀H8:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
+∀H9:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.
+∀H10:∀X:Univ.∀Y:Univ.eq Univ (meet X (join X Y)) X.
+∀H11:∀X:Univ.eq Univ (join X X) X.
+∀H12:∀X:Univ.eq Univ (meet X X) X.eq Univ (join a (meet (complement b) (join (complement a) (meet (complement b) (join a (meet (complement b) (complement a))))))) (join a (meet (complement b) (join (complement a) (meet (complement b) (join a (meet (complement b) (join (complement a) (meet (complement b) a))))))))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#b.
+#complement.
+#join.
+#meet.
+#n0.
+#n1.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12;
+∀H0:∀A:Univ.∀B:Univ.eq Univ (meet A B) (complement (join (complement A) (complement B))).
+∀H1:∀A:Univ.eq Univ (meet (complement A) A) n0.
+∀H2:∀A:Univ.eq Univ (join (complement A) A) n1.
+∀H3:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join X Y) Z) (join X (join Y Z)).
+∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet X Y) Z) (meet X (meet Y Z)).
+∀H5:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
+∀H6:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
+∀H7:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.
+∀H8:∀X:Univ.∀Y:Univ.eq Univ (meet X (join X Y)) X.
+∀H9:∀X:Univ.eq Univ (join X X) X.
+∀H10:∀X:Univ.eq Univ (meet X X) X.eq Univ (meet (join a (complement b)) (join (join (meet a b) (meet (complement a) b)) (meet (complement a) (complement b)))) (join (meet a b) (meet (complement a) (complement b)))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f (f B A) (f A C)) D) (f A (f (f A (f (f B B) B)) C))) A.eq Univ (f a (f (f b c) (f b c))) (f c (f (f b a) (f b a)))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f B A) (f (f (f (f B A) A) (f C A)) (f (f A A) D))) A.eq Univ (f a (f (f b c) (f b c))) (f c (f (f b a) (f b a)))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f (f B A) (f A C)) D) (f A (f (f C (f (f A A) C)) C))) A.eq Univ (f a (f (f b c) (f b c))) (f c (f (f b a) (f b a)))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f B (f A B)) B) (f A (f C (f (f A B) (f (f C C) D))))) A.eq Univ (f a (f b (f a (f c c)))) (f a (f c (f a (f b b))))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f B A) (f (f (f A A) C) (f (f (f (f (f A B) C) C) A) (f A D)))) A.eq Univ (f a (f (f b c) (f b c))) (f c (f (f b a) (f b a)))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f B A) (f (f (f A A) C) (f (f (f (f (f A B) C) C) A) (f A D)))) A.eq Univ (f a (f b (f a (f c c)))) (f a (f c (f a (f b b))))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f (f B A) (f C A)) D) (f A (f (f (f (f (f (f B B) A) C) C) A) B))) A.eq Univ (f a (f (f b c) (f b c))) (f c (f (f b a) (f b a)))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f (f B A) (f C A)) D) (f A (f (f (f (f (f (f B B) A) C) C) A) B))) A.eq Univ (f a (f b (f a (f c c)))) (f a (f c (f a (f b b))))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f (f B A) (f A C)) D) (f A (f (f (f B (f B (f (f C C) A))) A) C))) A.eq Univ (f a (f (f b c) (f b c))) (f c (f (f b a) (f b a)))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (f (f (f (f B A) (f A C)) D) (f A (f (f (f B (f B (f (f C C) A))) A) C))) A.eq Univ (f a (f b (f a (f c c)))) (f a (f c (f a (f b b))))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet D B) (meet B E)) B)) (meet (join (meet B (meet (meet (join D (join B E)) (join F B)) B)) (meet G (join B (meet (meet (join D (join B E)) (join F B)) B)))) (join A (join (join (meet D B) (meet B E)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (meet a a) a
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet D B) (meet B E)) B)) (meet (join (meet B (meet (meet (join D (join B E)) (join F B)) B)) (meet G (join B (meet (meet (join D (join B E)) (join F B)) B)))) (join A (join (join (meet D B) (meet B E)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (meet a b) (meet b a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet D B) (meet B E)) B)) (meet (join (meet B (meet (meet (join D (join B E)) (join F B)) B)) (meet G (join B (meet (meet (join D (join B E)) (join F B)) B)))) (join A (join (join (meet D B) (meet B E)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (meet (meet a b) c) (meet a (meet b c))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet D B) (meet B E)) B)) (meet (join (meet B (meet (meet (join D (join B E)) (join F B)) B)) (meet G (join B (meet (meet (join D (join B E)) (join F B)) B)))) (join A (join (join (meet D B) (meet B E)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (join a a) a
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet D B) (meet B E)) B)) (meet (join (meet B (meet (meet (join D (join B E)) (join F B)) B)) (meet G (join B (meet (meet (join D (join B E)) (join F B)) B)))) (join A (join (join (meet D B) (meet B E)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (join a b) (join b a)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet D B) (meet B E)) B)) (meet (join (meet B (meet (meet (join D (join B E)) (join F B)) B)) (meet G (join B (meet (meet (join D (join B E)) (join F B)) B)))) (join A (join (join (meet D B) (meet B E)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (join (join a b) c) (join a (join b c))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet D B) (meet B E)) B)) (meet (join (meet B (meet (meet (join D (join B E)) (join F B)) B)) (meet G (join B (meet (meet (join D (join B E)) (join F B)) B)))) (join A (join (join (meet D B) (meet B E)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (meet a (join a b)) a
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀G:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet D B) (meet B E)) B)) (meet (join (meet B (meet (meet (join D (join B E)) (join F B)) B)) (meet G (join B (meet (meet (join D (join B E)) (join F B)) B)))) (join A (join (join (meet D B) (meet B E)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (join a (meet a b)) a
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet B D) (meet E B)) B)) (meet (join (meet B (meet (meet (join B D) (join E B)) B)) (meet F (join B (meet (meet (join B D) (join E B)) B)))) (join A (join (join (meet B D) (meet E B)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (meet a a) a
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet B D) (meet E B)) B)) (meet (join (meet B (meet (meet (join B D) (join E B)) B)) (meet F (join B (meet (meet (join B D) (join E B)) B)))) (join A (join (join (meet B D) (meet E B)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (meet b a) (meet a b)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet B D) (meet E B)) B)) (meet (join (meet B (meet (meet (join B D) (join E B)) B)) (meet F (join B (meet (meet (join B D) (join E B)) B)))) (join A (join (join (meet B D) (meet E B)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (join a a) a
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet B D) (meet E B)) B)) (meet (join (meet B (meet (meet (join B D) (join E B)) B)) (meet F (join B (meet (meet (join B D) (join E B)) B)))) (join A (join (join (meet B D) (meet E B)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (join b a) (join a b)
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet B D) (meet E B)) B)) (meet (join (meet B (meet (meet (join B D) (join E B)) B)) (meet F (join B (meet (meet (join B D) (join E B)) B)))) (join A (join (join (meet B D) (meet E B)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (meet (meet (join a b) (join c b)) b) b
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.eq Univ (join (meet (join (meet A B) (meet B (join A B))) C) (meet (join (meet A (join (join (meet B D) (meet E B)) B)) (meet (join (meet B (meet (meet (join B D) (join E B)) B)) (meet F (join B (meet (meet (join B D) (join E B)) B)))) (join A (join (join (meet B D) (meet E B)) B)))) (join (join (meet A B) (meet B (join A B))) C))) B.eq Univ (join (join (meet a b) (meet c b)) b) b
+(* ----Distributive property of product over sum *)
+
+(* ----Right alternative law *)
+
+(* ----Associator *)
+
+(* ----Commutator *)
+
+(* ----Middle associator identity *)
+
+(* ----Left alternative law *)
+
+(* ----Definition of s *)
+
+(* ----Right Moufang *)
+
+(* ----Left Moufang *)
+
+(* ----Middle Moufang *)
+ntheorem prove_skew_symmetry:
+ ∀Univ:Type.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.
+∀a:Univ.
+∀add:∀_:Univ.∀_:Univ.Univ.
+∀additive_identity:Univ.
+∀additive_inverse:∀_:Univ.Univ.
+∀associator:∀_:Univ.∀_:Univ.∀_:Univ.Univ.
+∀b:Univ.
+∀c:Univ.
+∀commutator:∀_:Univ.∀_:Univ.Univ.
+∀d:Univ.
+∀multiply:∀_:Univ.∀_:Univ.Univ.
+∀s:∀_:Univ.∀_:Univ.∀_:Univ.∀_:Univ.Univ.
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) (multiply Z X)) (multiply (multiply X (multiply Y Z)) X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X (multiply Y X)) Z) (multiply X (multiply Y (multiply X Z))).
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Z (multiply X (multiply Y X))) (multiply (multiply (multiply Z X) Y) X).
+∀H3:∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (s W X Y Z) (add (add (associator (multiply W X) Y Z) (additive_inverse (multiply X (associator W Y Z)))) (additive_inverse (multiply (associator X Y Z) W))).
+∀H4:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X X) Y) (multiply X (multiply X Y)).
+∀H5:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply (associator X X Y) X) (associator X X Y)) additive_identity.
+∀H6:∀X:Univ.∀Y:Univ.eq Univ (commutator X Y) (add (multiply Y X) (additive_inverse (multiply X Y))).
+∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (associator X Y Z) (add (multiply (multiply X Y) Z) (additive_inverse (multiply X (multiply Y Z)))).
+∀H8:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X Y) Y) (multiply X (multiply Y Y)).
+∀H9:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
+∀H10:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
+∀H11:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
+∀H12:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
+∀H13:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) (multiply Z X)) (multiply (multiply X (multiply Y Z)) X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X (multiply Y X)) Z) (multiply X (multiply Y (multiply X Z))).
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Z (multiply X (multiply Y X))) (multiply (multiply (multiply Z X) Y) X).
+∀H3:∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (s W X Y Z) (add (add (associator (multiply W X) Y Z) (additive_inverse (multiply X (associator W Y Z)))) (additive_inverse (multiply (associator X Y Z) W))).
+∀H4:∀X:Univ.∀Y:Univ.eq Univ (commutator X Y) (add (multiply Y X) (additive_inverse (multiply X Y))).
+∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (associator X Y Z) (add (multiply (multiply X Y) Z) (additive_inverse (multiply X (multiply Y Z)))).
+∀H6:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X X) Y) (multiply X (multiply X Y)).
+∀H7:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X Y) Y) (multiply X (multiply Y Y)).
+∀H8:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
+∀H9:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).
+∀H10:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
+∀H11:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
+(* ----The next 7 clauses are extra lemmas which Stevens found useful *)
+
+(* ----Definition of s *)
+
+(* ----Right Moufang *)
+
+(* ----Left Moufang *)
+ntheorem prove_skew_symmetry:
+ ∀Univ:Type.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.
+∀a:Univ.
+∀add:∀_:Univ.∀_:Univ.Univ.
+∀additive_identity:Univ.
+∀additive_inverse:∀_:Univ.Univ.
+∀associator:∀_:Univ.∀_:Univ.∀_:Univ.Univ.
+∀b:Univ.
+∀c:Univ.
+∀commutator:∀_:Univ.∀_:Univ.Univ.
+∀d:Univ.
+∀multiply:∀_:Univ.∀_:Univ.Univ.
+∀s:∀_:Univ.∀_:Univ.∀_:Univ.∀_:Univ.Univ.
+∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) (multiply Z X)) (multiply (multiply X (multiply Y Z)) X).
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X (multiply Y X)) Z) (multiply X (multiply Y (multiply X Z))).
+∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Z (multiply X (multiply Y X))) (multiply (multiply (multiply Z X) Y) X).
+∀H3:∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (s W X Y Z) (add (add (associator (multiply W X) Y Z) (additive_inverse (multiply X (associator W Y Z)))) (additive_inverse (multiply (associator X Y Z) W))).
+∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) (additive_inverse Z)) (add (additive_inverse (multiply X Z)) (additive_inverse (multiply Y Z))).
+∀H5:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (additive_inverse X) (add Y Z)) (add (additive_inverse (multiply X Y)) (additive_inverse (multiply X Z))).
+∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X (additive_inverse Y)) Z) (add (multiply X Z) (additive_inverse (multiply Y Z))).
+∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y (additive_inverse Z))) (add (multiply X Y) (additive_inverse (multiply X Z))).
+∀H8:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
+∀H9:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
+∀H10:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).
+∀H11:∀X:Univ.∀Y:Univ.eq Univ (commutator X Y) (add (multiply Y X) (additive_inverse (multiply X Y))).
+∀H12:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (associator X Y Z) (add (multiply (multiply X Y) Z) (additive_inverse (multiply X (multiply Y Z)))).
+∀H13:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X X) Y) (multiply X (multiply X Y)).
+∀H14:∀X:Univ.∀Y:Univ.eq Univ (multiply (multiply X Y) Y) (multiply X (multiply Y Y)).
+∀H15:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
+∀H16:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).
+∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) Z) (add (multiply X Z) (multiply Y Z)).
+∀H18:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply X Y) (multiply X Z)).
+∀H15:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
+∀H16:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).
+∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) (additive_inverse Z)) (add (additive_inverse (multiply X Z)) (additive_inverse (multiply Y Z))).
+∀H18:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (additive_inverse X) (add Y Z)) (add (additive_inverse (multiply X Y)) (additive_inverse (multiply X Z))).
+∀H19:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X (additive_inverse Y)) Z) (add (multiply X Z) (additive_inverse (multiply Y Z))).
+∀H20:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y (additive_inverse Z))) (add (multiply X Y) (additive_inverse (multiply X Z))).
+∀H21:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
+∀H22:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
+∀H23:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).eq Univ (add (associator a b c) (associator a c b)) additive_identity
+.
+#Univ.
+#U.
+#V.
+#X.
+#Y.
+#Z.
+#a.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#b.
+#c.
+#commutator.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+#H18.
+#H19.
+#H20.
+#H21.
+#H22.
+#H23.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17,H18,H19,H20,H21,H22,H23;
+∀H13:∀X:Univ.eq Univ (add X additive_identity) X.
+∀H14:∀X:Univ.eq Univ (add additive_identity X) X.eq Univ (add (add (associator (multiply a b) c d) (associator a b (multiply c d))) (additive_inverse (add (add (associator a (multiply b c) d) (multiply a (associator b c d))) (multiply (associator a b c) d)))) additive_identity
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#b.
+#c.
+#commutator.
+#d.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14;
+∀H20:∀X:Univ.eq Univ (add X additive_identity) X.
+∀H21:∀X:Univ.eq Univ (add additive_identity X) X.eq Univ (add (add (associator (multiply a b) c d) (associator a b (multiply c d))) (additive_inverse (add (add (associator a (multiply b c) d) (multiply a (associator b c d))) (multiply (associator a b c) d)))) additive_identity
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#a.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#b.
+#c.
+#commutator.
+#d.
+#multiply.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+#H18.
+#H19.
+#H20.
+#H21.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17,H18,H19,H20,H21;
+∀H12:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
+∀H13:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add (multiply (associator x x y) (multiply (associator x x y) (associator x x y))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) additive_identity
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#commutator.
+#multiply.
+#x.
+#y.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13;
+∀H12:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
+∀H13:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).
+∀H14:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) (additive_inverse Z)) (add (additive_inverse (multiply X Z)) (additive_inverse (multiply Y Z))).
+∀H15:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (additive_inverse X) (add Y Z)) (add (additive_inverse (multiply X Y)) (additive_inverse (multiply X Z))).
+∀H16:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X (additive_inverse Y)) Z) (add (multiply X Z) (additive_inverse (multiply Y Z))).
+∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y (additive_inverse Z))) (add (multiply X Y) (additive_inverse (multiply X Z))).
+∀H18:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
+∀H19:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
+∀H20:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).eq Univ (add (multiply (associator x x y) (multiply (associator x x y) (associator x x y))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) additive_identity
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#commutator.
+#multiply.
+#x.
+#y.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+#H18.
+#H19.
+#H20.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17,H18,H19,H20;
+∀H12:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
+∀H13:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (multiply (multiply (multiply (associator x x y) (associator x x y)) x) (multiply (associator x x y) (associator x x y))) additive_identity
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#commutator.
+#multiply.
+#x.
+#y.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13;
+∀H12:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
+∀H13:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).
+∀H14:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) (additive_inverse Z)) (add (additive_inverse (multiply X Z)) (additive_inverse (multiply Y Z))).
+∀H15:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (additive_inverse X) (add Y Z)) (add (additive_inverse (multiply X Y)) (additive_inverse (multiply X Z))).
+∀H16:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X (additive_inverse Y)) Z) (add (multiply X Z) (additive_inverse (multiply Y Z))).
+∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y (additive_inverse Z))) (add (multiply X Y) (additive_inverse (multiply X Z))).
+∀H18:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
+∀H19:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
+∀H20:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).eq Univ (multiply (multiply (multiply (associator x x y) (associator x x y)) x) (multiply (associator x x y) (associator x x y))) additive_identity
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#commutator.
+#multiply.
+#x.
+#y.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+#H18.
+#H19.
+#H20.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17,H18,H19,H20;
+∀H12:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
+∀H13:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add (add (add (add (add (multiply (associator x x y) (multiply (associator x x y) (associator x x y))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) additive_identity
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#commutator.
+#multiply.
+#x.
+#y.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13;
+∀H12:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (add Y Z)) (add (add X Y) Z).
+∀H13:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).
+∀H14:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X Y) (additive_inverse Z)) (add (additive_inverse (multiply X Z)) (additive_inverse (multiply Y Z))).
+∀H15:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (additive_inverse X) (add Y Z)) (add (additive_inverse (multiply X Y)) (additive_inverse (multiply X Z))).
+∀H16:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (add X (additive_inverse Y)) Z) (add (multiply X Z) (additive_inverse (multiply Y Z))).
+∀H17:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y (additive_inverse Z))) (add (multiply X Y) (additive_inverse (multiply X Z))).
+∀H18:∀X:Univ.∀Y:Univ.eq Univ (multiply X (additive_inverse Y)) (additive_inverse (multiply X Y)).
+∀H19:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) Y) (additive_inverse (multiply X Y)).
+∀H20:∀X:Univ.∀Y:Univ.eq Univ (multiply (additive_inverse X) (additive_inverse Y)) (multiply X Y).eq Univ (add (add (add (add (add (multiply (associator x x y) (multiply (associator x x y) (associator x x y))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) (multiply (associator x x y) (multiply (associator x x y) (associator x x y)))) additive_identity
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#commutator.
+#multiply.
+#x.
+#y.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+#H18.
+#H19.
+#H20.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17,H18,H19,H20;
+∀H13:∀X:Univ.eq Univ (add X additive_identity) X.
+∀H14:∀X:Univ.eq Univ (add additive_identity X) X.eq Univ (add (associator (multiply x y) z w) (associator x y (commutator z w))) (add (multiply x (associator y z w)) (multiply (associator x z w) y))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#commutator.
+#multiply.
+#w.
+#x.
+#y.
+#z.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14;
+∀H20:∀X:Univ.eq Univ (add X additive_identity) X.
+∀H21:∀X:Univ.eq Univ (add additive_identity X) X.eq Univ (add (associator (multiply x y) z w) (associator x y (commutator z w))) (add (multiply x (associator y z w)) (multiply (associator x z w) y))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#commutator.
+#multiply.
+#w.
+#x.
+#y.
+#z.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+#H18.
+#H19.
+#H20.
+#H21.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17,H18,H19,H20,H21;
+∀H14:∀X:Univ.eq Univ (add X additive_identity) X.
+∀H15:∀X:Univ.eq Univ (add additive_identity X) X.eq Univ (add (associator (multiply x y) z w) (associator x y (commutator z w))) (add (multiply x (associator y z w)) (multiply (associator x z w) y))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#commutator.
+#multiply.
+#w.
+#x.
+#y.
+#z.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15;
+∀H21:∀X:Univ.eq Univ (add X additive_identity) X.
+∀H22:∀X:Univ.eq Univ (add additive_identity X) X.eq Univ (add (associator (multiply x y) z w) (associator x y (commutator z w))) (add (multiply x (associator y z w)) (multiply (associator x z w) y))
+.
+#Univ.
+#X.
+#Y.
+#Z.
+#add.
+#additive_identity.
+#additive_inverse.
+#associator.
+#commutator.
+#multiply.
+#w.
+#x.
+#y.
+#z.
+#H0.
+#H1.
+#H2.
+#H3.
+#H4.
+#H5.
+#H6.
+#H7.
+#H8.
+#H9.
+#H10.
+#H11.
+#H12.
+#H13.
+#H14.
+#H15.
+#H16.
+#H17.
+#H18.
+#H19.
+#H20.
+#H21.
+#H22.
+nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9,H10,H11,H12,H13,H14,H15,H16,H17,H18,H19,H20,H21,H22;