1 include "logic/equality.ma".
3 (* Inclusion of: BOO026-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : BOO026-1 : TPTP v3.7.0. Released v2.2.0. *)
9 (* Domain : Boolean Algebra *)
11 (* Problem : Absorption from self-dual independent 2-basis *)
13 (* Version : [MP96] (eqiality) axioms : Especial. *)
15 (* English : This is part of a proof that there exists an independent self-dual *)
17 (* 2-basis for Boolean Algebra. You may note that the basis *)
19 (* below has more than 2 equations; but don't worry, it can be *)
21 (* reduced to 2 (large) equations by Pixley reduction. *)
23 (* Refs : [Wos98] Wos (1998), Automating the Search for Elegant Proofs *)
25 (* : [McC98] McCune (1998), Email to G. Sutcliffe *)
27 (* : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq *)
29 (* Source : [McC98] *)
31 (* Names : DUAL-BA-3 [MP96] *)
33 (* : DUAL-BA-3 [Wos98] *)
35 (* Status : Unsatisfiable *)
37 (* Rating : 0.11 v3.4.0, 0.12 v3.3.0, 0.07 v3.1.0, 0.11 v2.7.0, 0.00 v2.2.1 *)
39 (* Syntax : Number of clauses : 11 ( 0 non-Horn; 11 unit; 1 RR) *)
41 (* Number of atoms : 11 ( 11 equality) *)
43 (* Maximal clause size : 1 ( 1 average) *)
45 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
47 (* Number of functors : 7 ( 4 constant; 0-2 arity) *)
49 (* Number of variables : 20 ( 0 singleton) *)
51 (* Maximal term depth : 5 ( 3 average) *)
53 (* Comments : The original proof has 816 steps. Wos later found a 99-step *)
57 (* -------------------------------------------------------------------------- *)
59 (* ----Two Boolean algebra properties and their duals: *)
61 (* ----Expanded Pixley properties and their duals: *)
63 (* ----Denial of the conclusion: *)
64 ntheorem prove_multiply_add:
65 (∀Univ:Type.∀X:Univ.∀Y:Univ.∀Z:Univ.
67 ∀add:∀_:Univ.∀_:Univ.Univ.
69 ∀inverse:∀_:Univ.Univ.
70 ∀multiply:∀_:Univ.∀_:Univ.Univ.
73 ∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply (add X (inverse Y)) (multiply (add X X) (add (inverse Y) X))) X.
74 ∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply (add X (inverse Y)) (multiply (add X Y) (add (inverse Y) Y))) X.
75 ∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply (add X (inverse X)) (multiply (add X Y) (add (inverse X) Y))) Y.
76 ∀H3:∀X:Univ.∀Y:Univ.eq Univ (add (multiply X (inverse Y)) (add (multiply X X) (multiply (inverse Y) X))) X.
77 ∀H4:∀X:Univ.∀Y:Univ.eq Univ (add (multiply X (inverse Y)) (add (multiply X Y) (multiply (inverse Y) Y))) X.
78 ∀H5:∀X:Univ.∀Y:Univ.eq Univ (add (multiply X (inverse X)) (add (multiply X Y) (multiply (inverse X) Y))) Y.
79 ∀H6:∀X:Univ.eq Univ (multiply X (inverse X)) n0.
80 ∀H7:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add X (multiply Y Z)) (multiply (add Y X) (add Z X)).
81 ∀H8:∀X:Univ.eq Univ (add X (inverse X)) n1.
82 ∀H9:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply X (add Y Z)) (add (multiply Y X) (multiply Z X)).eq Univ (multiply (add a b) b) b)
105 nauto by H0,H1,H2,H3,H4,H5,H6,H7,H8,H9 ##;
106 ntry (nassumption) ##;
109 (* -------------------------------------------------------------------------- *)