\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{BOO002-0.ax} Boolean algebra axioms






$x + y{=}x + y\qquad\mbox{cnf}(\mbox{closure\_of\_addition},\mbox{axiom})$

$x\cdot y{=}x\cdot y\qquad\mbox{cnf}(\mbox{closure\_of\_multiplication},\mbox{axiom})$

$x + y{=}z \ \Rightarrow \ y + x{=}z\qquad\mbox{cnf}(\mbox{commutativity\_of\_addition},\mbox{axiom})$

$x\cdot y{=}z \ \Rightarrow \ y\cdot x{=}z\qquad\mbox{cnf}(\mbox{commutativity\_of\_multiplication},\mbox{axiom})$

$0 + x{=}x\qquad\mbox{cnf}(\mbox{additive\_identity}_1,\mbox{axiom})$

$x + 0{=}x\qquad\mbox{cnf}(\mbox{additive\_identity}_2,\mbox{axiom})$

$1\cdot x{=}x\qquad\mbox{cnf}(\mbox{multiplicative\_identity}_1,\mbox{axiom})$

$x\cdot 1{=}x\qquad\mbox{cnf}(\mbox{multiplicative\_identity}_2,\mbox{axiom})$

$( x\cdot y{=}v_1\mbox{ and }x\cdot z{=}v_2\mbox{ and }y + z{=}v_3\mbox{ and }x\cdot v_3{=}v_4 ) \ \Rightarrow \ v_1 + v_2{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_1,\mbox{axiom})$

$( x\cdot y{=}v_1\mbox{ and }x\cdot z{=}v_2\mbox{ and }y + z{=}v_3\mbox{ and }v_1 + v_2{=}v_4 ) \ \Rightarrow \ x\cdot v_3{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_2,\mbox{axiom})$

$( y\cdot x{=}v_1\mbox{ and }z\cdot x{=}v_2\mbox{ and }y + z{=}v_3\mbox{ and }v_3\cdot x{=}v_4 ) \ \Rightarrow \ v_1 + v_2{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_3,\mbox{axiom})$

$( y\cdot x{=}v_1\mbox{ and }z\cdot x{=}v_2\mbox{ and }y + z{=}v_3\mbox{ and }v_1 + v_2{=}v_4 ) \ \Rightarrow \ v_3\cdot x{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_4,\mbox{axiom})$

$( x + y{=}v_1\mbox{ and }x + z{=}v_2\mbox{ and }y\cdot z{=}v_3\mbox{ and }x + v_3{=}v_4 ) \ \Rightarrow \ v_1\cdot v_2{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_5,\mbox{axiom})$

$( x + y{=}v_1\mbox{ and }x + z{=}v_2\mbox{ and }y\cdot z{=}v_3\mbox{ and }v_1\cdot v_2{=}v_4 ) \ \Rightarrow \ x + v_3{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_6,\mbox{axiom})$

$( y + x{=}v_1\mbox{ and }z + x{=}v_2\mbox{ and }y\cdot z{=}v_3\mbox{ and }v_3 + x{=}v_4 ) \ \Rightarrow \ v_1\cdot v_2{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_7,\mbox{axiom})$

$( y + x{=}v_1\mbox{ and }z + x{=}v_2\mbox{ and }y\cdot z{=}v_3\mbox{ and }v_1\cdot v_2{=}v_4 ) \ \Rightarrow \ v_3 + x{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_8,\mbox{axiom})$

$x' + x{=}1\qquad\mbox{cnf}(\mbox{additive\_inverse}_1,\mbox{axiom})$

$x + x'{=}1\qquad\mbox{cnf}(\mbox{additive\_inverse}_2,\mbox{axiom})$

$x'\cdot x{=}0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse}_1,\mbox{axiom})$

$x\cdot x'{=}0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse}_2,\mbox{axiom})$

$( x + y{=}u\mbox{ and }x + y{=}v ) \ \Rightarrow \ u = v\qquad\mbox{cnf}(\mbox{addition\_is\_well\_defined},\mbox{axiom})$

$( x\cdot y{=}u\mbox{ and }x\cdot y{=}v ) \ \Rightarrow \ u = v\qquad\mbox{cnf}(\mbox{multiplication\_is\_well\_defined},\mbox{axiom})$

\medskip\textbf{BOO001-0.ax} Ternary Boolean algebra (equality) axioms






$m(m(v,w,x),y,m(v,w,z)) = m(v,w,m(x,y,z))\qquad\mbox{cnf}(\mbox{associativity},\mbox{axiom})$

$m(y,x,x) = x\qquad\mbox{cnf}(\mbox{ternary\_multiply}_1,\mbox{axiom})$

$m(x,x,y) = x\qquad\mbox{cnf}(\mbox{ternary\_multiply}_2,\mbox{axiom})$

$m(y',y,x) = x\qquad\mbox{cnf}(\mbox{left\_inverse},\mbox{axiom})$

$m(x,y,y') = x\qquad\mbox{cnf}(\mbox{right\_inverse},\mbox{axiom})$

\medskip\textbf{BOO003-0.ax} Boolean algebra (equality) axioms






$x + y = y + x\qquad\mbox{cnf}(\mbox{commutativity\_of\_add},\mbox{axiom})$

$x\cdot y = y\cdot x\qquad\mbox{cnf}(\mbox{commutativity\_of\_multiply},\mbox{axiom})$

$x\cdot y + z = ( x + z )\cdot ( y + z )\qquad\mbox{cnf}(\mbox{distributivity}_1,\mbox{axiom})$

$x + y\cdot z = ( x + y )\cdot ( x + z )\qquad\mbox{cnf}(\mbox{distributivity}_2,\mbox{axiom})$

$( x + y )\cdot z = x\cdot z + y\cdot z\qquad\mbox{cnf}(\mbox{distributivity}_3,\mbox{axiom})$

$x\cdot ( y + z ) = x\cdot y + x\cdot z\qquad\mbox{cnf}(\mbox{distributivity}_4,\mbox{axiom})$

$x + x' = 1\qquad\mbox{cnf}(\mbox{additive\_inverse}_1,\mbox{axiom})$

$x' + x = 1\qquad\mbox{cnf}(\mbox{additive\_inverse}_2,\mbox{axiom})$

$x\cdot x' = 0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse}_1,\mbox{axiom})$

$x'\cdot x = 0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse}_2,\mbox{axiom})$

$x\cdot 1 = x\qquad\mbox{cnf}(\mbox{multiplicative\_id}_1,\mbox{axiom})$

$1\cdot x = x\qquad\mbox{cnf}(\mbox{multiplicative\_id}_2,\mbox{axiom})$

$x + 0 = x\qquad\mbox{cnf}(\mbox{additive\_id}_1,\mbox{axiom})$

$0 + x = x\qquad\mbox{cnf}(\mbox{additive\_id}_2,\mbox{axiom})$

\medskip\textbf{BOO004-0.ax} Boolean algebra (equality) axioms






$x + y = y + x\qquad\mbox{cnf}(\mbox{commutativity\_of\_add},\mbox{axiom})$

$x\cdot y = y\cdot x\qquad\mbox{cnf}(\mbox{commutativity\_of\_multiply},\mbox{axiom})$

$x + y\cdot z = ( x + y )\cdot ( x + z )\qquad\mbox{cnf}(\mbox{distributivity}_1,\mbox{axiom})$

$x\cdot ( y + z ) = x\cdot y + x\cdot z\qquad\mbox{cnf}(\mbox{distributivity}_2,\mbox{axiom})$

$x + 0 = x\qquad\mbox{cnf}(\mbox{additive\_id}_1,\mbox{axiom})$

$x\cdot 1 = x\qquad\mbox{cnf}(\mbox{multiplicative\_id}_1,\mbox{axiom})$

$x + x' = 1\qquad\mbox{cnf}(\mbox{additive\_inverse}_1,\mbox{axiom})$

$x\cdot x' = 0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse}_1,\mbox{axiom})$

\medskip\textbf{BOO011-4.p} Inverse of additive identity = Multiplicative identity






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$0'\ne 1\qquad\mbox{cnf}(\mbox{prove\_inverse\_of\_1\_is}_0,\mbox{negated\_conjecture})$

\medskip\textbf{BOO084-1.p} Axiom C4 for Boolean algebra in the Sheffer stroke, part 2






$( a\uparrow ( a\uparrow ( a\uparrow b ) ) )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_4,\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO087-1.p} Axiom C6 for Boolean algebra in the Sheffer stroke, part 1






$( a\uparrow ( a\uparrow ( b\uparrow c ) ) )\uparrow ( c\uparrow ( a\uparrow b ) ) = c\qquad\mbox{cnf}(c_6,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO107-1.p} Axiom C16 for Boolean algebra in the Sheffer stroke, part 1






$( ( ( a\uparrow b )\uparrow c )\uparrow c )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_{16},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO001-1.p} In B3 algebra, inverse is an involution






$\mbox{include}(\mbox{'Axioms/BOO001-0.ax'})$

$( a' )'\ne a\qquad\mbox{cnf}(\mbox{prove\_inverse\_is\_self\_cancelling},\mbox{negated\_conjecture})$

\medskip\textbf{BOO096-1.p} Axiom C10 for Boolean algebra in the Sheffer stroke, part 2






$( ( a\uparrow ( b\uparrow c ) )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{10},\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO109+1.p} Josef Urban's problem using the Wajsberg axiom






$\forall a,b,c,d{:}\;p(( a\uparrow ( b\uparrow c ) )\uparrow ( ( ( d\uparrow c )\uparrow ( ( a\uparrow d )\uparrow ( a\uparrow d ) ) )\uparrow ( a\uparrow ( a\uparrow b ) ) ))\qquad\mbox{fof}(\mbox{wajsbergs\_axiom},\mbox{axiom})$

$\forall p,q,r{:}\;( ( p(p\uparrow ( q\uparrow r ))\mbox{ and }p(p) ) \ \Rightarrow \ p(r) )\qquad\mbox{fof}(\mbox{modus\_ponens\_for\_nand},\mbox{axiom})$

$\forall a,b{:}\;p(( a\uparrow ( b\uparrow b ) )\uparrow ( ( ( b\uparrow b )\uparrow ( ( a\uparrow a )\uparrow ( a\uparrow a ) ) )\uparrow ( ( b\uparrow b )\uparrow ( ( a\uparrow a )\uparrow ( a\uparrow a ) ) ) ))\qquad\mbox{fof}(\mbox{tautology},\mbox{conjecture})$

\medskip\textbf{BOO023-1.p} Half of Padmanabhan's 6-basis with Pixley, part 1.

Part 1 (of 3) of the proof that half of Padmanaban's self-dual
 independent 6-basis for Boolean Algebra, together with a Pixley
 polynomial, is a basis for Boolean algebra.




$( x + y )\cdot y = y\qquad\mbox{cnf}(\mbox{multiply\_add},\mbox{axiom})$

$x\cdot ( y + z ) = y\cdot x + z\cdot x\qquad\mbox{cnf}(\mbox{multiply\_add\_property},\mbox{axiom})$

$x + x' = n_1\qquad\mbox{cnf}(\mbox{additive\_inverse},\mbox{axiom})$

$\mbox{pixley}(x,y,z) = x\cdot y' + ( x\cdot z + y'\cdot z )\qquad\mbox{cnf}(\mbox{pixley\_defn},\mbox{axiom})$

$\mbox{pixley}(x,x,y) = y\qquad\mbox{cnf}(\mbox{pixley}_1,\mbox{axiom})$

$\mbox{pixley}(x,y,y) = x\qquad\mbox{cnf}(\mbox{pixley}_2,\mbox{axiom})$

$\mbox{pixley}(x,y,x) = x\qquad\mbox{cnf}(\mbox{pixley}_3,\mbox{axiom})$

$a + b\cdot c\ne ( a + b )\cdot ( a + c )\qquad\mbox{cnf}(\mbox{prove\_add\_multiply\_property},\mbox{negated\_conjecture})$

\medskip\textbf{BOO003-4.p} Multiplication is idempotent (X * X = X)






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$a\cdot a\ne a\qquad\mbox{cnf}(\mbox{prove\_a\_times\_a\_is\_a},\mbox{negated\_conjecture})$

\medskip\textbf{BOO040-1.p} Single axiom C1 for Boolean algebra in the Sheffer stroke






$( a\uparrow ( ( b\uparrow a )\uparrow a ) )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO043-1.p} Single axiom C4 for Boolean algebra in the Sheffer stroke






$( a\uparrow ( a\uparrow ( a\uparrow b ) ) )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_4,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO018-4.p} Inverse of multiplicative identity = Additive identity






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$1'\ne 0\qquad\mbox{cnf}(\mbox{prove\_inverse\_of\_1\_is}_0,\mbox{negated\_conjecture})$

\medskip\textbf{BOO009-2.p} Multiplication absorption (X * (X + Y) = X)






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a\cdot ( a + b )\ne a\qquad\mbox{cnf}(\mbox{prove\_operation},\mbox{negated\_conjecture})$

\medskip\textbf{BOO089-1.p} Axiom C7 for Boolean algebra in the Sheffer stroke, part 1






$( a\uparrow ( a\uparrow ( b\uparrow b ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_7,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO078-1.p} Axiom C1 for Boolean algebra in the Sheffer stroke, part 2






$( a\uparrow ( ( b\uparrow a )\uparrow a ) )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO007-2.p} Product is associative ( (X * Y) * Z = X * (Y * Z) )






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a\cdot ( b\cdot c )\ne ( a\cdot b )\cdot c\qquad\mbox{cnf}(\mbox{prove\_associativity},\mbox{negated\_conjecture})$

\medskip\textbf{BOO024-1.p} Half of Padmanabhan's 6-basis with Pixley, part 2.

Part 2 (of 3) of the proof that half of Padmanaban's self-dual
 independent 6-basis for Boolean Algebra, together with a Pixley
 polynomial, is a basis for Boolean algebra.




$( x + y )\cdot y = y\qquad\mbox{cnf}(\mbox{multiply\_add},\mbox{axiom})$

$x\cdot ( y + z ) = y\cdot x + z\cdot x\qquad\mbox{cnf}(\mbox{multiply\_add\_property},\mbox{axiom})$

$x + x' = n_1\qquad\mbox{cnf}(\mbox{additive\_inverse},\mbox{axiom})$

$\mbox{pixley}(x,y,z) = x\cdot y' + ( x\cdot z + y'\cdot z )\qquad\mbox{cnf}(\mbox{pixley\_defn},\mbox{axiom})$

$\mbox{pixley}(x,x,y) = y\qquad\mbox{cnf}(\mbox{pixley}_1,\mbox{axiom})$

$\mbox{pixley}(x,y,y) = x\qquad\mbox{cnf}(\mbox{pixley}_2,\mbox{axiom})$

$\mbox{pixley}(x,y,x) = x\qquad\mbox{cnf}(\mbox{pixley}_3,\mbox{axiom})$

$a\cdot b + b\ne b\qquad\mbox{cnf}(\mbox{prove\_add\_multiply},\mbox{negated\_conjecture})$

\medskip\textbf{BOO008-3.p} Sum is associative ( (X + Y) + Z = X + (Y + Z) )






$x + y{=}x + y\qquad\mbox{cnf}(\mbox{closure\_of\_addition},\mbox{axiom})$

$x\cdot y{=}x\cdot y\qquad\mbox{cnf}(\mbox{closure\_of\_multiplication},\mbox{axiom})$

$x + y{=}z \ \Rightarrow \ y + x{=}z\qquad\mbox{cnf}(\mbox{commutativity\_of\_addition},\mbox{axiom})$

$x\cdot y{=}z \ \Rightarrow \ y\cdot x{=}z\qquad\mbox{cnf}(\mbox{commutativity\_of\_multiplication},\mbox{axiom})$

$0 + x{=}x\qquad\mbox{cnf}(\mbox{additive\_identity}_1,\mbox{axiom})$

$x + 0{=}x\qquad\mbox{cnf}(\mbox{additive\_identity}_2,\mbox{axiom})$

$1 + x{=}x\qquad\mbox{cnf}(\mbox{multiplicative\_identity}_1,\mbox{axiom})$

$x + 1{=}x\qquad\mbox{cnf}(\mbox{multiplicative\_identity}_2,\mbox{axiom})$

$( x\cdot y{=}v_1\mbox{ and }x\cdot z{=}v_2\mbox{ and }y + z{=}v_3\mbox{ and }x\cdot v_3{=}v_4 ) \ \Rightarrow \ v_1 + v_2{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_1,\mbox{axiom})$

$( x\cdot y{=}v_1\mbox{ and }x\cdot z{=}v_2\mbox{ and }y + z{=}v_3\mbox{ and }v_1 + v_2{=}v_4 ) \ \Rightarrow \ x\cdot v_3{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_2,\mbox{axiom})$

$( x + y{=}v_1\mbox{ and }x + z{=}v_2\mbox{ and }y\cdot z{=}v_3\mbox{ and }x + v_3{=}v_4 ) \ \Rightarrow \ v_1\cdot v_2{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_5,\mbox{axiom})$

$( x + y{=}v_1\mbox{ and }x + z{=}v_2\mbox{ and }y\cdot z{=}v_3\mbox{ and }v_1\cdot v_2{=}v_4 ) \ \Rightarrow \ x + v_3{=}v_4\qquad\mbox{cnf}(\mbox{distributivity}_6,\mbox{axiom})$

$x' + x{=}1\qquad\mbox{cnf}(\mbox{additive\_inverse}_1,\mbox{axiom})$

$x + x'{=}1\qquad\mbox{cnf}(\mbox{additive\_inverse}_2,\mbox{axiom})$

$x'\cdot x{=}0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse}_1,\mbox{axiom})$

$x\cdot x'{=}0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse}_2,\mbox{axiom})$

$y + z{=}\mbox{y\_plus\_z}\qquad\mbox{cnf}(\mbox{y\_plus\_z},\mbox{hypothesis})$

$x + \mbox{y\_plus\_z}{=}\mbox{x\_\_plus\_y\_plus\_z}\qquad\mbox{cnf}(\mbox{x\_plus\_\_y\_plus\_z},\mbox{hypothesis})$

$x + y{=}\mbox{x\_plus\_y}\qquad\mbox{cnf}(\mbox{x\_plus\_y},\mbox{hypothesis})$

$\mbox{x\_plus\_y} + z{=}\mbox{x\_plus\_y\_\_plus\_z}\qquad\mbox{cnf}(\mbox{x\_plus\_y\_\_plus\_z},\mbox{hypothesis})$

$\mbox{x\_\_plus\_y\_plus\_z}\ne \mbox{x\_plus\_y\_\_plus\_z}\qquad\mbox{cnf}(\mbox{prove\_equality},\mbox{negated\_conjecture})$

\medskip\textbf{BOO004-1.p} Addition is idempotent (X + X = X)






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$\neg\,x + x{=}x\qquad\mbox{cnf}(\mbox{prove\_both\_equalities},\mbox{negated\_conjecture})$

\medskip\textbf{BOO014-2.p} DeMorgan for inverse and product (X+Y)$\wedge$-1 = (X$\wedge$-1) * (Y$\wedge$-1)






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a + b = c\qquad\mbox{cnf}(\mbox{a\_plus\_b\_is\_c},\mbox{hypothesis})$

$a'\cdot b' = d\qquad\mbox{cnf}(\mbox{a\_inverse\_times\_b\_inverse\_is\_d},\mbox{hypothesis})$

$c'\ne d\qquad\mbox{cnf}(\mbox{prove\_c\_inverse\_is\_d},\mbox{negated\_conjecture})$

\medskip\textbf{BOO052-1.p} Single axiom C13 for Boolean algebra in the Sheffer stroke






$( ( ( a\uparrow b )\uparrow a )\uparrow a )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_{13},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO060-1.p} Single non-axiom M6C for Boolean algebra in the Sheffer stroke






$( ( a\uparrow ( b\uparrow b ) )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(\mbox{m6C},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO100-1.p} Axiom C12 for Boolean algebra in the Sheffer stroke, part 2






$( ( a\uparrow ( a\uparrow b ) )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{12},\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO006-4.p} Multiplication is bounded (X * 0 = 0)






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$a\cdot 0\ne 0\qquad\mbox{cnf}(\mbox{prove\_right\_identity},\mbox{negated\_conjecture})$

\medskip\textbf{BOO083-1.p} Axiom C4 for Boolean algebra in the Sheffer stroke, part 1






$( a\uparrow ( a\uparrow ( a\uparrow b ) ) )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_4,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO092-1.p} Axiom C8 for Boolean algebra in the Sheffer stroke, part 2






$( ( a\uparrow ( a\uparrow b ) )\uparrow a )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_8,\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO038-1.p} DN-1 is a single axiom for Boolean algebra

Show that equation DN-1 is a single axiom for Boolean algebra
 in terms of disjunction and negation by deriving the Huntington
 3-basis.




$( ( ( a + b )' + c )' + ( a + ( c' + ( c + d )' )' )' )' = c\qquad\mbox{cnf}(\mbox{dn}_1,\mbox{axiom})$

$( b + a = a + b\mbox{ and }( a + b ) + c = a + ( b + c ) ) \ \Rightarrow \ ( a' + b )' + ( a' + b' )'\ne a\qquad\mbox{cnf}(\mbox{huntinton},\mbox{negated\_conjecture})$

\medskip\textbf{BOO103-1.p} Axiom C14 for Boolean algebra in the Sheffer stroke, part 1






$( ( ( a\uparrow b )\uparrow a )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{14},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO051-1.p} Single axiom C12 for Boolean algebra in the Sheffer stroke






$( ( a\uparrow ( a\uparrow b ) )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{12},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO013-2.p} The inverse of X is unique






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a + b = 1\qquad\mbox{cnf}(\mbox{b\_and\_multiplicative\_identity},\mbox{hypothesis})$

$a + c = 1\qquad\mbox{cnf}(\mbox{c\_and\_multiplicative\_identity},\mbox{hypothesis})$

$a\cdot b = 0\qquad\mbox{cnf}(\mbox{b\_a\_additive\_identity},\mbox{hypothesis})$

$a\cdot c = 0\qquad\mbox{cnf}(\mbox{c\_a\_additive\_identity},\mbox{hypothesis})$

$b\ne c\qquad\mbox{cnf}(\mbox{prove\_b\_is\_a},\mbox{negated\_conjecture})$

\medskip\textbf{BOO047-1.p} Single axiom C8 for Boolean algebra in the Sheffer stroke






$( ( a\uparrow ( a\uparrow b ) )\uparrow a )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_8,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO106-1.p} Axiom C15 for Boolean algebra in the Sheffer stroke, part 2






$( ( ( a\uparrow b )\uparrow c )\uparrow c )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{15},\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO091-1.p} Axiom C8 for Boolean algebra in the Sheffer stroke, part 1






$( ( a\uparrow ( a\uparrow b ) )\uparrow a )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_8,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO008-2.p} Sum is associative ( (X + Y) + Z = X + (Y + Z) )






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a + ( b + c )\ne ( a + b ) + c\qquad\mbox{cnf}(\mbox{prove\_associativity},\mbox{negated\_conjecture})$

\medskip\textbf{BOO069-1.p} Ternary Boolean Algebra Single axiom is complete, part 3






$m(m(a,a',b),( m(m(c,d,e),f,m(c,d,g)) )',m(d,m(g,f,e),c)) = b\qquad\mbox{cnf}(\mbox{single\_axiom},\mbox{axiom})$

$m(a,b,b')\ne a\qquad\mbox{cnf}(\mbox{prove\_tba\_axioms}_3,\mbox{negated\_conjecture})$

\medskip\textbf{BOO086-1.p} Axiom C5 for Boolean algebra in the Sheffer stroke, part 2






$( a\uparrow ( a\uparrow ( b\uparrow c ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_5,\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO008-4.p} Sum is associative ( (X + Y) + Z = X + (Y + Z) )






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$a + ( b + c )\ne ( a + b ) + c\qquad\mbox{cnf}(\mbox{prove\_associativity},\mbox{negated\_conjecture})$

\medskip\textbf{BOO005-2.p} Addition is bounded (X + 1 = 1)






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a + 1\ne 1\qquad\mbox{cnf}(\mbox{prove\_a\_plus\_1\_is\_a},\mbox{negated\_conjecture})$

\medskip\textbf{BOO101-1.p} Axiom C13 for Boolean algebra in the Sheffer stroke, part 1






$( ( ( a\uparrow b )\uparrow a )\uparrow a )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_{13},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO074-1.p} DN-1 is a single axiom for Boolean algebra, part 3






$( ( ( a + b )' + c )' + ( a + ( c' + ( c + d )' )' )' )' = c\qquad\mbox{cnf}(\mbox{dn}_1,\mbox{axiom})$

$( a' + b )' + ( a' + b' )'\ne a\qquad\mbox{cnf}(\mbox{huntinton}_3,\mbox{negated\_conjecture})$

\medskip\textbf{BOO025-1.p} Half of Padmanabhan's 6-basis with Pixley, part 3.

Part 3 (of 3) of the proof that half of Padmanaban's self-dual
 independent 6-basis for Boolean Algebra, together with a Pixley
 polynomial, is a basis for Boolean algebra.




$( x + y )\cdot y = y\qquad\mbox{cnf}(\mbox{multiply\_add},\mbox{axiom})$

$x\cdot ( y + z ) = y\cdot x + z\cdot x\qquad\mbox{cnf}(\mbox{multiply\_add\_property},\mbox{axiom})$

$x + x' = n_1\qquad\mbox{cnf}(\mbox{additive\_inverse},\mbox{axiom})$

$\mbox{pixley}(x,y,z) = x\cdot y' + ( x\cdot z + y'\cdot z )\qquad\mbox{cnf}(\mbox{pixley\_defn},\mbox{axiom})$

$\mbox{pixley}(x,x,y) = y\qquad\mbox{cnf}(\mbox{pixley}_1,\mbox{axiom})$

$\mbox{pixley}(x,y,y) = x\qquad\mbox{cnf}(\mbox{pixley}_2,\mbox{axiom})$

$\mbox{pixley}(x,y,x) = x\qquad\mbox{cnf}(\mbox{pixley}_3,\mbox{axiom})$

$b\cdot b'\ne a\cdot a'\qquad\mbox{cnf}(\mbox{prove\_equal\_identity},\mbox{negated\_conjecture})$

\medskip\textbf{BOO028-1.p} Self-dual 2-basis from majority reduction, part 1.

This is part of a proof that there exists an independent
 self-dual-2-basis for Boolean algebra by majority reduction.




$x + y\cdot ( x\cdot z ) = x\qquad\mbox{cnf}(l_1,\mbox{axiom})$

$( x\cdot y + y\cdot z ) + y = y\qquad\mbox{cnf}(l_3,\mbox{axiom})$

$( x + y )\cdot ( x + y' ) = x\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$x\cdot ( y + ( x + z ) ) = x\qquad\mbox{cnf}(l_2,\mbox{axiom})$

$( ( x + y )\cdot ( y + z ) )\cdot y = y\qquad\mbox{cnf}(l_4,\mbox{axiom})$

$x\cdot y + x\cdot y' = x\qquad\mbox{cnf}(b_2,\mbox{axiom})$

$x + y = y + x\qquad\mbox{cnf}(\mbox{commutativity\_of\_add},\mbox{axiom})$

$x\cdot y = y\cdot x\qquad\mbox{cnf}(\mbox{commutativity\_of\_multiply},\mbox{axiom})$

$( x + y ) + z = x + ( y + z )\qquad\mbox{cnf}(\mbox{associativity\_of\_add},\mbox{axiom})$

$( x\cdot y )\cdot z = x\cdot ( y\cdot z )\qquad\mbox{cnf}(\mbox{associativity\_of\_multiply},\mbox{axiom})$

$a\cdot ( b + c )\ne b\cdot a + c\cdot a\qquad\mbox{cnf}(\mbox{prove\_multiply\_add\_property},\mbox{negated\_conjecture})$

\medskip\textbf{BOO053-1.p} Single axiom C14 for Boolean algebra in the Sheffer stroke






$( ( ( a\uparrow b )\uparrow a )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{14},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO022-1.p} A Basis for Boolean Algebra

This theorem starts with a (self-dual independent) 6-basis
 for Boolean algebra and derives associativity of product.




$( x + y )\cdot y = y\qquad\mbox{cnf}(\mbox{multiply\_add},\mbox{axiom})$

$x\cdot ( y + z ) = y\cdot x + z\cdot x\qquad\mbox{cnf}(\mbox{multiply\_add\_property},\mbox{axiom})$

$x + x' = n_1\qquad\mbox{cnf}(\mbox{additive\_inverse},\mbox{axiom})$

$x\cdot y + y = y\qquad\mbox{cnf}(\mbox{add\_multiply},\mbox{axiom})$

$x + y\cdot z = ( y + x )\cdot ( z + x )\qquad\mbox{cnf}(\mbox{add\_multiply\_property},\mbox{axiom})$

$x\cdot x' = n_0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse},\mbox{axiom})$

$( a\cdot b )\cdot c\ne a\cdot ( b\cdot c )\qquad\mbox{cnf}(\mbox{prove\_associativity\_of\_multiply},\mbox{negated\_conjecture})$

\medskip\textbf{BOO068-1.p} Ternary Boolean Algebra Single axiom is complete, part 2






$m(m(a,a',b),( m(m(c,d,e),f,m(c,d,g)) )',m(d,m(g,f,e),c)) = b\qquad\mbox{cnf}(\mbox{single\_axiom},\mbox{axiom})$

$m(b,a,a)\ne a\qquad\mbox{cnf}(\mbox{prove\_tba\_axioms}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO007-1.p} Product is associative ( (X * Y) * Z = X * (Y * Z) )






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$y\cdot z{=}\mbox{y\_times\_z}\qquad\mbox{cnf}(\mbox{y\_times\_z},\mbox{hypothesis})$

$x\cdot \mbox{y\_times\_z}{=}\mbox{x\_times\_\_y\_times\_z}\qquad\mbox{cnf}(\mbox{x\_times\_\_y\_times\_z},\mbox{hypothesis})$

$x\cdot y{=}\mbox{x\_times\_y}\qquad\mbox{cnf}(\mbox{x\_times\_y},\mbox{hypothesis})$

$\mbox{x\_times\_y}\cdot z{=}\mbox{x\_times\_y\_\_times\_z}\qquad\mbox{cnf}(\mbox{x\_times\_y\_\_times\_z},\mbox{hypothesis})$

$\mbox{x\_times\_\_y\_times\_z}\ne \mbox{x\_times\_y\_\_times\_z}\qquad\mbox{cnf}(\mbox{prove\_equality},\mbox{negated\_conjecture})$

\medskip\textbf{BOO002-1.p} In B3 algebra, X * X$\wedge$-1 * Y = Y






$m(m(v,w,x),y,m(v,w,z)) = m(v,w,m(x,y,z))\qquad\mbox{cnf}(\mbox{associativity},\mbox{axiom})$

$m(y,x,x) = x\qquad\mbox{cnf}(\mbox{ternary\_multiply}_1,\mbox{axiom})$

$m(x,x,y) = x\qquad\mbox{cnf}(\mbox{ternary\_multiply}_2,\mbox{axiom})$

$m(y',y,x) = x\qquad\mbox{cnf}(\mbox{left\_inverse},\mbox{axiom})$

$m(a,a',b)\ne b\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{BOO004-4.p} Addition is idempotent (X + X = X)






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$a + a\ne a\qquad\mbox{cnf}(\mbox{prove\_a\_plus\_a\_is\_a},\mbox{negated\_conjecture})$

\medskip\textbf{BOO015-1.p} DeMorgan for inverse and sum (X$\wedge$-1 + Y$\wedge$-1) = (X * Y)$\wedge$-1






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$x\cdot y{=}\mbox{x\_times\_y}\qquad\mbox{cnf}(\mbox{x\_times\_y},\mbox{negated\_conjecture})$

$x' + y'{=}\mbox{x\_inverse\_plus\_y\_inverse}\qquad\mbox{cnf}(\mbox{x\_inverse\_plus\_y\_inverse},\mbox{negated\_conjecture})$

$\mbox{x\_times\_y}'\ne \mbox{x\_inverse\_plus\_y\_inverse}\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{BOO072-1.p} DN-1 is a single axiom for Boolean algebra, part 1






$( ( ( a + b )' + c )' + ( a + ( c' + ( c + d )' )' )' )' = c\qquad\mbox{cnf}(\mbox{dn}_1,\mbox{axiom})$

$b + a\ne a + b\qquad\mbox{cnf}(\mbox{huntinton}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO034-1.p} Ternary Boolean Algebra Single axiom is sound.

We show that that an equation (which turns out to be a single
 axiom for TBA) can be derived from the axioms of TBA.




$\mbox{include}(\mbox{'Axioms/BOO001-0.ax'})$

$m(m(a,a',b),( m(m(c,d,e),f,m(c,d,g)) )',m(d,m(g,f,e),c))\ne b\qquad\mbox{cnf}(\mbox{prove\_single\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{BOO033-1.p} Independence of a system of Boolean algebra.

This is part of a proof that a self-dual 3-basis for
 Boolean algebra is independent.




$x\cdot y + ( y\cdot z + z\cdot x ) = ( x + y )\cdot ( ( y + z )\cdot ( z + x ) )\qquad\mbox{cnf}(\mbox{distributivity},\mbox{axiom})$

$x + y\cdot ( x\cdot z ) = x\qquad\mbox{cnf}(l_1,\mbox{axiom})$

$( x\cdot y + y\cdot z ) + y = y\qquad\mbox{cnf}(l_3,\mbox{axiom})$

$( x + x' )\cdot y = y\qquad\mbox{cnf}(\mbox{property}_3,\mbox{axiom})$

$( x\cdot y + x )\cdot ( x + y ) = x\qquad\mbox{cnf}(\mbox{majority}_1,\mbox{axiom})$

$( x\cdot x + y )\cdot ( x + x ) = x\qquad\mbox{cnf}(\mbox{majority}_2,\mbox{axiom})$

$( x\cdot y + y )\cdot ( x + y ) = y\qquad\mbox{cnf}(\mbox{majority}_3,\mbox{axiom})$

$( a' )'\ne a\qquad\mbox{cnf}(\mbox{prove\_inverse\_involution},\mbox{negated\_conjecture})$

\medskip\textbf{BOO067-1.p} Ternary Boolean Algebra Single axiom is complete, part 1






$m(m(a,a',b),( m(m(c,d,e),f,m(c,d,g)) )',m(d,m(g,f,e),c)) = b\qquad\mbox{cnf}(\mbox{single\_axiom},\mbox{axiom})$

$m(m(d,e,a),b,m(d,e,c))\ne m(d,e,m(a,b,c))\qquad\mbox{cnf}(\mbox{prove\_tba\_axioms}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO088-1.p} Axiom C6 for Boolean algebra in the Sheffer stroke, part 2






$( a\uparrow ( a\uparrow ( b\uparrow c ) ) )\uparrow ( c\uparrow ( a\uparrow b ) ) = c\qquad\mbox{cnf}(c_6,\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO093-1.p} Axiom C9 for Boolean algebra in the Sheffer stroke, part 1






$( ( a\uparrow ( b\uparrow b ) )\uparrow a )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_9,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO009-4.p} Multiplication absorption (X * (X + Y) = X)






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$a\cdot ( a + b )\ne a\qquad\mbox{cnf}(\mbox{prove\_operation},\mbox{negated\_conjecture})$

\medskip\textbf{BOO026-1.p} Absorption from self-dual independent 2-basis

This is part of a proof that there exists an independent self-dual
 2-basis for Boolean Algebra.  You may note that the basis
 below has more than 2 equations; but don't worry, it can be
 reduced to 2 (large) equations by Pixley reduction.




$x\cdot ( y + z ) = y\cdot x + z\cdot x\qquad\mbox{cnf}(\mbox{multiply\_add\_property},\mbox{axiom})$

$x + x' = n_1\qquad\mbox{cnf}(\mbox{additive\_inverse},\mbox{axiom})$

$x + y\cdot z = ( y + x )\cdot ( z + x )\qquad\mbox{cnf}(\mbox{add\_multiply\_property},\mbox{axiom})$

$x\cdot x' = n_0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse},\mbox{axiom})$

$x\cdot x' + ( x\cdot y + x'\cdot y ) = y\qquad\mbox{cnf}(\mbox{pixley}_1,\mbox{axiom})$

$x\cdot y' + ( x\cdot y + y'\cdot y ) = x\qquad\mbox{cnf}(\mbox{pixley}_2,\mbox{axiom})$

$x\cdot y' + ( x\cdot x + y'\cdot x ) = x\qquad\mbox{cnf}(\mbox{pixley}_3,\mbox{axiom})$

$( x + x' )\cdot ( ( x + y )\cdot ( x' + y ) ) = y\qquad\mbox{cnf}(\mbox{pixley1\_dual},\mbox{axiom})$

$( x + y' )\cdot ( ( x + y )\cdot ( y' + y ) ) = x\qquad\mbox{cnf}(\mbox{pixley2\_dual},\mbox{axiom})$

$( x + y' )\cdot ( ( x + x )\cdot ( y' + x ) ) = x\qquad\mbox{cnf}(\mbox{pixley3\_dual},\mbox{axiom})$

$( a + b )\cdot b\ne b\qquad\mbox{cnf}(\mbox{prove\_multiply\_add},\mbox{negated\_conjecture})$

\medskip\textbf{BOO011-1.p} Inverse of additive identity = Multiplicative identity

The inverse of the additive identity is the multiplicative
 identity.




$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$0'\ne 1\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{BOO013-3.p} The inverse of X is unique






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$( x' )' = x\qquad\mbox{cnf}(\mbox{inverse\_is\_an\_involution},\mbox{axiom})$

$x + y{=}1\qquad\mbox{cnf}(\mbox{sum\_to\_multiplicative\_identity}_1,\mbox{negated\_conjecture})$

$x + z{=}1\qquad\mbox{cnf}(\mbox{sum\_to\_multiplicative\_identity}_2,\mbox{negated\_conjecture})$

$x\cdot y{=}0\qquad\mbox{cnf}(\mbox{product\_to\_additive\_identity}_1,\mbox{negated\_conjecture})$

$x\cdot z{=}0\qquad\mbox{cnf}(\mbox{product\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$y\ne z\qquad\mbox{cnf}(\mbox{prove\_both\_inverse\_are\_equal},\mbox{negated\_conjecture})$

\medskip\textbf{BOO003-1.p} Multiplication is idempotent (X * X = X)






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$\neg\,x\cdot x{=}x\qquad\mbox{cnf}(\mbox{prove\_both\_equalities},\mbox{negated\_conjecture})$

\medskip\textbf{BOO070-1.p} Ternary Boolean Algebra Single axiom is complete, part 4






$m(m(a,a',b),( m(m(c,d,e),f,m(c,d,g)) )',m(d,m(g,f,e),c)) = b\qquad\mbox{cnf}(\mbox{single\_axiom},\mbox{axiom})$

$m(a,a,b)\ne a\qquad\mbox{cnf}(\mbox{prove\_tba\_axioms}_4,\mbox{negated\_conjecture})$

\medskip\textbf{BOO015-2.p} DeMorgan for inverse and sum (X$\wedge$-1 + Y$\wedge$-1) = (X * Y)$\wedge$-1






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a\cdot b = c\qquad\mbox{cnf}(\mbox{a\_times\_b\_is\_c},\mbox{hypothesis})$

$a' + b' = d\qquad\mbox{cnf}(\mbox{a\_inverse\_plus\_b\_inverse\_is\_d},\mbox{hypothesis})$

$c'\ne d\qquad\mbox{cnf}(\mbox{prove\_c\_inverse\_is\_d},\mbox{negated\_conjecture})$

\medskip\textbf{BOO030-1.p} Independence of a BA 2-basis by majority reduction.

This shows that the self-dual 2-basis for Boolean algebra
 (majority reduction) of problem DUAL-BA-5 is independent,
 in particular, that half of the 2-basis is not a basis.




$x + y\cdot ( x\cdot z ) = x\qquad\mbox{cnf}(l_1,\mbox{axiom})$

$( x\cdot y + y\cdot z ) + y = y\qquad\mbox{cnf}(l_3,\mbox{axiom})$

$( x + y )\cdot ( x + y' ) = x\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$( x\cdot y + x )\cdot ( x + y ) = x\qquad\mbox{cnf}(\mbox{majority}_1,\mbox{axiom})$

$( x\cdot x + y )\cdot ( x + x ) = x\qquad\mbox{cnf}(\mbox{majority}_2,\mbox{axiom})$

$( x\cdot y + y )\cdot ( x + y ) = y\qquad\mbox{cnf}(\mbox{majority}_3,\mbox{axiom})$

$( a' )'\ne a\qquad\mbox{cnf}(\mbox{prove\_inverse\_involution},\mbox{negated\_conjecture})$

\medskip\textbf{BOO020-1.p} Frink's Theorem

Prove that Frink's implicational basis for Boolean algebra
 implies Huntington's equational basis for Boolean algebra.




$x + x = x\qquad\mbox{cnf}(\mbox{frink}_1,\mbox{axiom})$

$( ( x + y ) + z ) + u = ( y + z ) + x \ \Rightarrow \ ( ( x + y ) + z ) + u' = n_0\qquad\mbox{cnf}(\mbox{frink}_2,\mbox{axiom})$

$( ( x + y ) + z ) + u' = n_0 \ \Rightarrow \ ( ( x + y ) + z ) + u = ( y + z ) + x\qquad\mbox{cnf}(\mbox{frink}_3,\mbox{axiom})$

$( ( a + b' )' + ( a' + b' )' = b\mbox{ and }( a + b ) + c = a + ( b + c ) ) \ \Rightarrow \ b + a\ne a + b\qquad\mbox{cnf}(\mbox{prove\_huntington},\mbox{negated\_conjecture})$

\medskip\textbf{BOO037-2.p} Boolean algebra (equality) axioms






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

\medskip\textbf{BOO014-1.p} DeMorgan for inverse and product (X+Y)$\wedge$-1 = (X$\wedge$-1) * (Y$\wedge$-1)






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$x + y{=}\mbox{x\_plus\_y}\qquad\mbox{cnf}(\mbox{x\_plus\_y},\mbox{negated\_conjecture})$

$x'\cdot y'{=}\mbox{x\_inverse\_times\_y\_inverse}\qquad\mbox{cnf}(\mbox{x\_inverse\_times\_y\_inverse},\mbox{negated\_conjecture})$

$\mbox{x\_plus\_y}'\ne \mbox{x\_inverse\_times\_y\_inverse}\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{BOO097-1.p} Axiom C11 for Boolean algebra in the Sheffer stroke, part 1






$( ( a\uparrow ( b\uparrow c ) )\uparrow a )\uparrow ( c\uparrow ( a\uparrow b ) ) = c\qquad\mbox{cnf}(c_{11},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO055-1.p} Single axiom C16 for Boolean algebra in the Sheffer stroke






$( ( ( a\uparrow b )\uparrow c )\uparrow c )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_{16},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO071-1.p} Ternary Boolean Algebra Single axiom is complete, part 5






$m(m(a,a',b),( m(m(c,d,e),f,m(c,d,g)) )',m(d,m(g,f,e),c)) = b\qquad\mbox{cnf}(\mbox{single\_axiom},\mbox{axiom})$

$m(b',b,a)\ne a\qquad\mbox{cnf}(\mbox{prove\_tba\_axioms}_5,\mbox{negated\_conjecture})$

\medskip\textbf{BOO012-1.p} Inverse is an involution






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$( x' )'\ne x\qquad\mbox{cnf}(\mbox{prove\_inverse\_is\_an\_involution},\mbox{negated\_conjecture})$

\medskip\textbf{BOO056-1.p} Single non-axiom M5A for Boolean algebra in the Sheffer stroke






$( a\uparrow ( ( b\uparrow c )\uparrow a ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(\mbox{m5A},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO102-1.p} Axiom C13 for Boolean algebra in the Sheffer stroke, part 2






$( ( ( a\uparrow b )\uparrow a )\uparrow a )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_{13},\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO010-4.p} Addition absorbtion (X + (X * Y) = X)






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$a + a\cdot b\ne a\qquad\mbox{cnf}(\mbox{prove\_a\_plus\_ab\_is\_a},\mbox{negated\_conjecture})$

\medskip\textbf{BOO048-1.p} Single axiom C9 for Boolean algebra in the Sheffer stroke






$( ( a\uparrow ( b\uparrow b ) )\uparrow a )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_9,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO016-1.p} Relating product and sum (X * Y = Z $\to$ X + Z = X)






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$x\cdot y{=}z\qquad\mbox{cnf}(\mbox{x\_times\_y},\mbox{hypothesis})$

$\neg\,x + z{=}x\qquad\mbox{cnf}(\mbox{prove\_sum},\mbox{negated\_conjecture})$

\medskip\textbf{BOO105-1.p} Axiom C15 for Boolean algebra in the Sheffer stroke, part 1






$( ( ( a\uparrow b )\uparrow c )\uparrow c )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{15},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO044-1.p} Single axiom C5 for Boolean algebra in the Sheffer stroke






$( a\uparrow ( a\uparrow ( b\uparrow c ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_5,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO032-1.p} Independence of a system of Boolean algebra

This is part of a proof that a self-dual 3-basis for Boolean
 algebra is independent.




$x + y\cdot ( x\cdot z ) = x\qquad\mbox{cnf}(l_1,\mbox{axiom})$

$( x\cdot y + y\cdot z ) + y = y\qquad\mbox{cnf}(l_3,\mbox{axiom})$

$( x + x' )\cdot y = y\qquad\mbox{cnf}(\mbox{property}_3,\mbox{axiom})$

$x\cdot ( y + ( x + z ) ) = x\qquad\mbox{cnf}(l_2,\mbox{axiom})$

$( ( x + y )\cdot ( y + z ) )\cdot y = y\qquad\mbox{cnf}(l_4,\mbox{axiom})$

$x\cdot x' + y = y\qquad\mbox{cnf}(\mbox{property3\_dual},\mbox{axiom})$

$( x + y )\cdot x + x\cdot y = x\qquad\mbox{cnf}(\mbox{majority}_1,\mbox{axiom})$

$( x + x )\cdot y + x\cdot x = x\qquad\mbox{cnf}(\mbox{majority}_2,\mbox{axiom})$

$( x + y )\cdot y + x\cdot y = y\qquad\mbox{cnf}(\mbox{majority}_3,\mbox{axiom})$

$( x\cdot y + x )\cdot ( x + y ) = x\qquad\mbox{cnf}(\mbox{majority1\_dual},\mbox{axiom})$

$( x\cdot x + y )\cdot ( x + x ) = x\qquad\mbox{cnf}(\mbox{majority2\_dual},\mbox{axiom})$

$( x\cdot y + y )\cdot ( x + y ) = y\qquad\mbox{cnf}(\mbox{majority3\_dual},\mbox{axiom})$

$( a' )'\ne a\qquad\mbox{cnf}(\mbox{prove\_inverse\_involution},\mbox{negated\_conjecture})$

\medskip\textbf{BOO012-4.p} Inverse is an involution






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$( x' )'\ne x\qquad\mbox{cnf}(\mbox{prove\_inverse\_is\_an\_involution},\mbox{negated\_conjecture})$

\medskip\textbf{BOO006-1.p} Multiplication is bounded (X * 0 = 0)






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$\neg\,x\cdot 0{=}0\qquad\mbox{cnf}(\mbox{prove\_equations},\mbox{negated\_conjecture})$

\medskip\textbf{BOO011-2.p} Inverse of additive identity = Multiplicative identity

The inverse of the additive identity is the multiplicative
 identity.




$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$0'\ne 1\qquad\mbox{cnf}(\mbox{prove\_inverse\_of\_1\_is}_0,\mbox{negated\_conjecture})$

\medskip\textbf{BOO010-2.p} Addition absorbtion (X + (X * Y) = X)






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a + a\cdot b\ne a\qquad\mbox{cnf}(\mbox{prove\_a\_plus\_ab\_is\_a},\mbox{negated\_conjecture})$

\medskip\textbf{BOO013-4.p} The inverse of X is unique






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$a + b = 1\qquad\mbox{cnf}(\mbox{b\_a\_multiplicative\_identity},\mbox{hypothesis})$

$a\cdot b = 0\qquad\mbox{cnf}(\mbox{b\_an\_additive\_identity},\mbox{hypothesis})$

$b\ne a'\qquad\mbox{cnf}(\mbox{prove\_a\_inverse\_is\_b},\mbox{negated\_conjecture})$

\medskip\textbf{BOO010-1.p} Addition absorbtion (X + (X * Y) = X)






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$\neg\,x + x\cdot y{=}x\qquad\mbox{cnf}(\mbox{prove\_equations},\mbox{negated\_conjecture})$

\medskip\textbf{BOO077-1.p} Axiom C1 for Boolean algebra in the Sheffer stroke, part 1






$( a\uparrow ( ( b\uparrow a )\uparrow a ) )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO003-2.p} Multiplication is idempotent (X * X = X)






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a\cdot a\ne a\qquad\mbox{cnf}(\mbox{prove\_a\_times\_a\_is\_a},\mbox{negated\_conjecture})$

\medskip\textbf{BOO031-1.p} Dual BA 3-basis, proof of distributivity.

This is part of a proof of the existence of a self-dual
 3-basis for Boolean algebra by majority reduction.




$x\cdot y + ( y\cdot z + z\cdot x ) = ( x + y )\cdot ( ( y + z )\cdot ( z + x ) )\qquad\mbox{cnf}(\mbox{distributivity},\mbox{axiom})$

$x + y\cdot ( x\cdot z ) = x\qquad\mbox{cnf}(l_1,\mbox{axiom})$

$( x\cdot y + y\cdot z ) + y = y\qquad\mbox{cnf}(l_3,\mbox{axiom})$

$( x + x' )\cdot y = y\qquad\mbox{cnf}(\mbox{property}_3,\mbox{axiom})$

$x\cdot ( y + ( x + z ) ) = x\qquad\mbox{cnf}(l_2,\mbox{axiom})$

$( ( x + y )\cdot ( y + z ) )\cdot y = y\qquad\mbox{cnf}(l_4,\mbox{axiom})$

$x\cdot x' + y = y\qquad\mbox{cnf}(\mbox{property3\_dual},\mbox{axiom})$

$x + x' = n_1\qquad\mbox{cnf}(\mbox{additive\_inverse},\mbox{axiom})$

$x\cdot x' = n_0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse},\mbox{axiom})$

$( x + y ) + z = x + ( y + z )\qquad\mbox{cnf}(\mbox{associativity\_of\_add},\mbox{axiom})$

$( x\cdot y )\cdot z = x\cdot ( y\cdot z )\qquad\mbox{cnf}(\mbox{associativity\_of\_multiply},\mbox{axiom})$

$a\cdot ( b + c )\ne b\cdot a + c\cdot a\qquad\mbox{cnf}(\mbox{prove\_multiply\_add\_property},\mbox{negated\_conjecture})$

\medskip\textbf{BOO079-1.p} Axiom C2 for Boolean algebra in the Sheffer stroke, part 1






$( a\uparrow ( a\uparrow ( b\uparrow a ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO080-1.p} Axiom C2 for Boolean algebra in the Sheffer stroke, part 2






$( a\uparrow ( a\uparrow ( b\uparrow a ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO075-1.p} Sh-1 is a single axiom for Boolean algebra, part 1






$( a\uparrow ( ( b\uparrow a )\uparrow a ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(\mbox{sh}_1,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO027-1.p} Independence of self-dual 2-basis.

Show that half of the self-dual 2-basis in DUAL-BA-3 is not
 a basis for Boolean Algebra.




$x\cdot ( y + z ) = y\cdot x + z\cdot x\qquad\mbox{cnf}(\mbox{multiply\_add\_property},\mbox{axiom})$

$x + x' = 1\qquad\mbox{cnf}(\mbox{additive\_inverse},\mbox{axiom})$

$x\cdot x' + ( x\cdot y + x'\cdot y ) = y\qquad\mbox{cnf}(\mbox{pixley}_1,\mbox{axiom})$

$x\cdot y' + ( x\cdot y + y'\cdot y ) = x\qquad\mbox{cnf}(\mbox{pixley}_2,\mbox{axiom})$

$x\cdot y' + ( x\cdot x + y'\cdot x ) = x\qquad\mbox{cnf}(\mbox{pixley}_3,\mbox{axiom})$

$a + a\ne a\qquad\mbox{cnf}(\mbox{prove\_idempotence},\mbox{negated\_conjecture})$

\medskip\textbf{BOO042-1.p} Single axiom C3 for Boolean algebra in the Sheffer stroke






$( a\uparrow ( a\uparrow ( a\uparrow b ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO013-1.p} The inverse of X is unique






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$x + y{=}1\qquad\mbox{cnf}(\mbox{sum\_to\_multiplicative\_identity}_1,\mbox{negated\_conjecture})$

$x + z{=}1\qquad\mbox{cnf}(\mbox{sum\_to\_multiplicative\_identity}_2,\mbox{negated\_conjecture})$

$x\cdot y{=}0\qquad\mbox{cnf}(\mbox{product\_to\_additive\_identity}_1,\mbox{negated\_conjecture})$

$x\cdot z{=}0\qquad\mbox{cnf}(\mbox{product\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$y\ne z\qquad\mbox{cnf}(\mbox{prove\_both\_inverse\_are\_equal},\mbox{negated\_conjecture})$

\medskip\textbf{BOO005-1.p} Addition is bounded (X + 1 = 1)






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$\neg\,x + 1{=}1\qquad\mbox{cnf}(\mbox{prove\_equations},\mbox{negated\_conjecture})$

\medskip\textbf{BOO029-1.p} Self-dual 2-basis from majority reduction, part 3.

This is part of a proof that there exists an independent
 self-dual-2-basis for Boolean algebra by majority reduction.




$x + y\cdot ( x\cdot z ) = x\qquad\mbox{cnf}(l_1,\mbox{axiom})$

$( x\cdot y + y\cdot z ) + y = y\qquad\mbox{cnf}(l_3,\mbox{axiom})$

$( x + y )\cdot ( x + y' ) = x\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$x\cdot ( y + ( x + z ) ) = x\qquad\mbox{cnf}(l_2,\mbox{axiom})$

$( ( x + y )\cdot ( y + z ) )\cdot y = y\qquad\mbox{cnf}(l_4,\mbox{axiom})$

$x\cdot y + x\cdot y' = x\qquad\mbox{cnf}(b_2,\mbox{axiom})$

$x + y = y + x\qquad\mbox{cnf}(\mbox{commutativity\_of\_add},\mbox{axiom})$

$x\cdot y = y\cdot x\qquad\mbox{cnf}(\mbox{commutativity\_of\_multiply},\mbox{axiom})$

$( x + y ) + z = x + ( y + z )\qquad\mbox{cnf}(\mbox{associativity\_of\_add},\mbox{axiom})$

$( x\cdot y )\cdot z = x\cdot ( y\cdot z )\qquad\mbox{cnf}(\mbox{associativity\_of\_multiply},\mbox{axiom})$

$b + b'\ne a + a'\qquad\mbox{cnf}(\mbox{prove\_equal\_inverse},\mbox{negated\_conjecture})$

\medskip\textbf{BOO054-1.p} Single axiom C15 for Boolean algebra in the Sheffer stroke






$( ( ( a\uparrow b )\uparrow c )\uparrow c )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{15},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO037-3.p} Boolean algebra (equality) axioms






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

\medskip\textbf{BOO066-1.p} Single non-axiom M8A for Boolean algebra in the Sheffer stroke






$( ( a\uparrow ( b\uparrow c ) )\uparrow a )\uparrow ( c\uparrow ( b\uparrow a ) ) = c\qquad\mbox{cnf}(\mbox{m8A},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO081-1.p} Axiom C3 for Boolean algebra in the Sheffer stroke, part 1






$( a\uparrow ( a\uparrow ( a\uparrow b ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO076-1.p} Sh-1 is a single axiom for Boolean algebra, part 2






$( a\uparrow ( ( b\uparrow a )\uparrow a ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(\mbox{sh}_1,\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO061-1.p} Single non-axiom M6D for Boolean algebra in the Sheffer stroke






$( a\uparrow ( a\uparrow ( b\uparrow b ) ) )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(\mbox{m6D},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO059-1.p} Single non-axiom M6B for Boolean algebra in the Sheffer stroke






$( a\uparrow ( a\uparrow ( b\uparrow a ) ) )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(\mbox{m6B},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO007-4.p} Product is associative ( (X * Y) * Z = X * (Y * Z) )






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$a\cdot ( b\cdot c )\ne ( a\cdot b )\cdot c\qquad\mbox{cnf}(\mbox{prove\_associativity},\mbox{negated\_conjecture})$

\medskip\textbf{BOO021-1.p} A Basis for Boolean Algebra

This theorem starts with a (self-dual independent) basis\_
 for Boolean algebra and derives commutativity of product.




$( x + y )\cdot y = y\qquad\mbox{cnf}(\mbox{multiply\_add},\mbox{axiom})$

$x\cdot ( y + z ) = y\cdot x + z\cdot x\qquad\mbox{cnf}(\mbox{multiply\_add\_property},\mbox{axiom})$

$x + x' = n_1\qquad\mbox{cnf}(\mbox{additive\_inverse},\mbox{axiom})$

$x\cdot y + y = y\qquad\mbox{cnf}(\mbox{add\_multiply},\mbox{axiom})$

$x + y\cdot z = ( y + x )\cdot ( z + x )\qquad\mbox{cnf}(\mbox{add\_multiply\_property},\mbox{axiom})$

$x\cdot x' = n_0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse},\mbox{axiom})$

$b\cdot a\ne a\cdot b\qquad\mbox{cnf}(\mbox{prove\_commutativity\_of\_multiply},\mbox{negated\_conjecture})$

\medskip\textbf{BOO012-3.p} Inverse is an involution






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$x + x{=}x\qquad\mbox{cnf}(\mbox{x\_plus\_x\_is\_x},\mbox{axiom})$

$x\cdot x{=}x\qquad\mbox{cnf}(\mbox{x\_times\_x\_is\_x},\mbox{axiom})$

$x + 1{=}1\qquad\mbox{cnf}(\mbox{x\_plus\_multiplicative\_identity},\mbox{axiom})$

$x\cdot 0{=}0\qquad\mbox{cnf}(\mbox{x\_times\_additive\_identity},\mbox{axiom})$

$x\cdot y{=}z \ \Rightarrow \ x + z{=}x\qquad\mbox{cnf}(\mbox{sum\_product\_dual}_1,\mbox{axiom})$

$x + y{=}z \ \Rightarrow \ x\cdot z{=}x\qquad\mbox{cnf}(\mbox{sum\_product\_dual}_2,\mbox{axiom})$

$x + x\cdot y{=}x\qquad\mbox{cnf}(\mbox{sum\_and\_multiply},\mbox{axiom})$

$x\cdot ( x + y ){=}x\qquad\mbox{cnf}(\mbox{product\_and\_add},\mbox{axiom})$

$( x + y{=}\mbox{x\_plus\_Y}\mbox{ and }y + z{=}\mbox{y\_plus\_Z}\mbox{ and }x + \mbox{y\_plus\_Z}{=}\mbox{x\_plus\_Y\_plus\_Z} ) \ \Rightarrow \ \mbox{x\_plus\_Y} + z{=}\mbox{x\_plus\_Y\_plus\_Z}\qquad\mbox{cnf}(\mbox{associaticity\_of\_sum}_1,\mbox{axiom})$

$( x + y{=}\mbox{x\_plus\_Y}\mbox{ and }y + z{=}\mbox{y\_plus\_Z}\mbox{ and }x + \mbox{y\_plus\_Z}{=}\mbox{x\_plus\_Y\_plus\_Z} ) \ \Rightarrow \ \mbox{x\_plus\_Y} + z{=}\mbox{x\_plus\_Y\_plus\_Z}\qquad\mbox{cnf}(\mbox{associaticity\_of\_sum}_2,\mbox{axiom})$

$( x\cdot y{=}\mbox{x\_times\_Y}\mbox{ and }y\cdot z{=}\mbox{y\_times\_Z}\mbox{ and }x\cdot \mbox{y\_times\_Z}{=}\mbox{x\_times\_Y\_times\_Z} ) \ \Rightarrow \ \mbox{x\_times\_Y}\cdot z{=}\mbox{x\_times\_Y\_times\_Z}\qquad\mbox{cnf}(\mbox{associaticity\_of\_product}_1,\mbox{axiom})$

$( x\cdot y{=}\mbox{x\_times\_Y}\mbox{ and }y\cdot z{=}\mbox{y\_times\_Z}\mbox{ and }x\cdot \mbox{y\_times\_Z}{=}\mbox{x\_times\_Y\_times\_Z} ) \ \Rightarrow \ \mbox{x\_times\_Y}\cdot z{=}\mbox{x\_times\_Y\_times\_Z}\qquad\mbox{cnf}(\mbox{associaticity\_of\_product}_2,\mbox{axiom})$

$( x' )'\ne x\qquad\mbox{cnf}(\mbox{prove\_inverse\_is\_an\_involution},\mbox{negated\_conjecture})$

\medskip\textbf{BOO098-1.p} Axiom C11 for Boolean algebra in the Sheffer stroke, part 2






$( ( a\uparrow ( b\uparrow c ) )\uparrow a )\uparrow ( c\uparrow ( a\uparrow b ) ) = c\qquad\mbox{cnf}(c_{11},\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO017-2.p} Relating sum and product (X + Y = Z $\to$ X * Z = X)






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$x + y = z\qquad\mbox{cnf}(\mbox{x\_times\_y},\mbox{hypothesis})$

$x\cdot z\ne x\qquad\mbox{cnf}(\mbox{prove\_sum},\mbox{negated\_conjecture})$

\medskip\textbf{BOO050-1.p} Single axiom C11 for Boolean algebra in the Sheffer stroke






$( ( a\uparrow ( b\uparrow c ) )\uparrow a )\uparrow ( c\uparrow ( a\uparrow b ) ) = c\qquad\mbox{cnf}(c_{11},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO037-1.p} Boolean algebra axioms






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

\medskip\textbf{BOO009-1.p} Multiplication absorption (X * (X + Y) = X)






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$\neg\,x\cdot ( x + y ){=}x\qquad\mbox{cnf}(\mbox{prove\_equations},\mbox{negated\_conjecture})$

\medskip\textbf{BOO035-1.p} Ternary Boolean Algebra Single axiom is complete

We show that that the standard axioms for TAB can be derived
 from an equation that turns out to be a single axiom for TBA.




$m(m(x,x',y),( m(m(z,u,v),w,m(z,u,v_6)) )',m(u,m(v_6,w,v),z)) = y\qquad\mbox{cnf}(\mbox{single\_axiom},\mbox{axiom})$

$( m(m(d,e,a),b,m(d,e,c)) = m(d,e,m(a,b,c))\mbox{ and }m(b,a,a) = a\mbox{ and }m(a,b,b') = a\mbox{ and }m(a,a,b) = a ) \ \Rightarrow \ m(b',b,a)\ne a\qquad\mbox{cnf}(\mbox{prove\_tba\_axioms},\mbox{negated\_conjecture})$

\medskip\textbf{BOO012-2.p} Inverse is an involution






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$( x' )'\ne x\qquad\mbox{cnf}(\mbox{prove\_inverse\_is\_an\_involution},\mbox{negated\_conjecture})$

\medskip\textbf{BOO016-2.p} Relating product and sum (X * Y = Z $\to$ X + Z = X)






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$x\cdot y = z\qquad\mbox{cnf}(\mbox{x\_times\_y},\mbox{hypothesis})$

$x + z\ne x\qquad\mbox{cnf}(\mbox{prove\_sum},\mbox{negated\_conjecture})$

\medskip\textbf{BOO004-2.p} Addition is idempotent (X + X = X)






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a + a\ne a\qquad\mbox{cnf}(\mbox{prove\_a\_plus\_a\_is\_a},\mbox{negated\_conjecture})$

\medskip\textbf{BOO045-1.p} Single axiom C6 for Boolean algebra in the Sheffer stroke






$( a\uparrow ( a\uparrow ( b\uparrow c ) ) )\uparrow ( c\uparrow ( a\uparrow b ) ) = c\qquad\mbox{cnf}(c_6,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO008-1.p} Sum is associative ( (X + Y) + Z = X + (Y + Z) )






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$y + z{=}\mbox{y\_plus\_z}\qquad\mbox{cnf}(\mbox{y\_plus\_z},\mbox{hypothesis})$

$x + \mbox{y\_plus\_z}{=}\mbox{x\_\_plus\_y\_plus\_z}\qquad\mbox{cnf}(\mbox{x\_plus\_\_y\_plus\_z},\mbox{hypothesis})$

$x + y{=}\mbox{x\_plus\_y}\qquad\mbox{cnf}(\mbox{x\_plus\_y},\mbox{hypothesis})$

$\mbox{x\_plus\_y} + z{=}\mbox{x\_plus\_y\_\_plus\_z}\qquad\mbox{cnf}(\mbox{x\_plus\_y\_\_plus\_z},\mbox{hypothesis})$

$\mbox{x\_\_plus\_y\_plus\_z}\ne \mbox{x\_plus\_y\_\_plus\_z}\qquad\mbox{cnf}(\mbox{prove\_equality},\mbox{negated\_conjecture})$

\medskip\textbf{BOO058-1.p} Single non-axiom M6A for Boolean algebra in the Sheffer stroke






$( ( a\uparrow ( b\uparrow a ) )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(\mbox{m6A},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO046-1.p} Single axiom C7 for Boolean algebra in the Sheffer stroke






$( a\uparrow ( a\uparrow ( b\uparrow b ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_7,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO082-1.p} Axiom C3 for Boolean algebra in the Sheffer stroke, part 2






$( a\uparrow ( a\uparrow ( a\uparrow b ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO015-4.p} DeMorgan for inverse and sum (X$\wedge$-1 + Y$\wedge$-1) = (X * Y)$\wedge$-1






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$( a\cdot b )'\ne a' + b'\qquad\mbox{cnf}(\mbox{prove\_c\_inverse\_is\_d},\mbox{negated\_conjecture})$

\medskip\textbf{BOO085-1.p} Axiom C5 for Boolean algebra in the Sheffer stroke, part 1






$( a\uparrow ( a\uparrow ( b\uparrow c ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_5,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO090-1.p} Axiom C7 for Boolean algebra in the Sheffer stroke, part 2






$( a\uparrow ( a\uparrow ( b\uparrow b ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_7,\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO108-1.p} Axiom C16 for Boolean algebra in the Sheffer stroke, part 2






$( ( ( a\uparrow b )\uparrow c )\uparrow c )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_{16},\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO005-4.p} Addition is bounded (X + 1 = 1)






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$a + 1\ne 1\qquad\mbox{cnf}(\mbox{prove\_a\_plus\_1\_is\_a},\mbox{negated\_conjecture})$

\medskip\textbf{BOO039-1.p} Sh-1 is a single axiom for Boolean algebra

Show that equation Sh-1 is a single axiom for Boolean algebra in
 terms of the Sheffer stroke by deriving the Meredith 2-basis.




$( a\uparrow ( ( b\uparrow a )\uparrow a ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(\mbox{sh}_1,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO073-1.p} DN-1 is a single axiom for Boolean algebra, part 2






$( ( ( a + b )' + c )' + ( a + ( c' + ( c + d )' )' )' )' = c\qquad\mbox{cnf}(\mbox{dn}_1,\mbox{axiom})$

$( a + b ) + c\ne a + ( b + c )\qquad\mbox{cnf}(\mbox{huntinton}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO094-1.p} Axiom C9 for Boolean algebra in the Sheffer stroke, part 2






$( ( a\uparrow ( b\uparrow b ) )\uparrow a )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_9,\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO014-4.p} DeMorgan for inverse and product (X+Y)$\wedge$-1 = (X$\wedge$-1) * (Y$\wedge$-1)






$\mbox{include}(\mbox{'Axioms/BOO004-0.ax'})$

$( a + b )'\ne a'\cdot b'\qquad\mbox{cnf}(\mbox{prove\_c\_inverse\_is\_d},\mbox{negated\_conjecture})$

\medskip\textbf{BOO099-1.p} Axiom C12 for Boolean algebra in the Sheffer stroke, part 1






$( ( a\uparrow ( a\uparrow b ) )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{12},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO036-1.p} Ternary Boolean algebra (equality) axioms






$\mbox{include}(\mbox{'Axioms/BOO001-0.ax'})$

\medskip\textbf{BOO104-1.p} Axiom C14 for Boolean algebra in the Sheffer stroke, part 2






$( ( ( a\uparrow b )\uparrow a )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{14},\mbox{axiom})$

$a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_2,\mbox{negated\_conjecture})$

\medskip\textbf{BOO017-1.p} Relating sum and product (X + Y = Z $\to$ X * Z = X)






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$x + y{=}z\qquad\mbox{cnf}(\mbox{x\_plus\_y},\mbox{hypothesis})$

$\neg\,x\cdot z{=}x\qquad\mbox{cnf}(\mbox{prove\_product},\mbox{negated\_conjecture})$

\medskip\textbf{BOO057-1.p} Single non-axiom M5B for Boolean algebra in the Sheffer stroke






$( ( a\uparrow ( b\uparrow c ) )\uparrow a )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(\mbox{m5B},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO041-1.p} Single axiom C2 for Boolean algebra in the Sheffer stroke






$( a\uparrow ( a\uparrow ( b\uparrow a ) ) )\uparrow ( b\uparrow ( c\uparrow a ) ) = b\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO006-2.p} Multiplication is bounded (X * 0 = 0)






$\mbox{include}(\mbox{'Axioms/BOO003-0.ax'})$

$a\cdot 0\ne 0\qquad\mbox{cnf}(\mbox{prove\_right\_identity},\mbox{negated\_conjecture})$

\medskip\textbf{BOO049-1.p} Single axiom C10 for Boolean algebra in the Sheffer stroke






$( ( a\uparrow ( b\uparrow c ) )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{10},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a ) = a \ \Rightarrow \ a\uparrow ( b\uparrow ( a\uparrow c ) )\ne ( ( c\uparrow b )\uparrow b )\uparrow a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis},\mbox{negated\_conjecture})$

\medskip\textbf{BOO014-3.p} DeMorgan for inverse and product (X+Y)$\wedge$-1 = (X$\wedge$-1) * (Y$\wedge$-1)






$\mbox{include}(\mbox{'Axioms/BOO002-0.ax'})$

$( x' )' = x\qquad\mbox{cnf}(\mbox{inverse\_is\_self\_cancelling},\mbox{axiom})$

$( x + y{=}1\mbox{ and }x + z{=}1\mbox{ and }x\cdot y{=}0\mbox{ and }x\cdot z{=}0 ) \ \Rightarrow \ y = z\qquad\mbox{cnf}(\mbox{inverse\_is\_unique},\mbox{axiom})$

$x + y{=}\mbox{x\_plus\_y}\qquad\mbox{cnf}(\mbox{x\_plus\_y},\mbox{hypothesis})$

$x'\cdot y'{=}\mbox{x\_inverse\_times\_y\_inverse}\qquad\mbox{cnf}(\mbox{x\_inverse\_times\_y\_inverse},\mbox{hypothesis})$

$\mbox{x\_plus\_y}'\ne \mbox{x\_inverse\_times\_y\_inverse}\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{BOO095-1.p} Axiom C10 for Boolean algebra in the Sheffer stroke, part 1






$( ( a\uparrow ( b\uparrow c ) )\uparrow a )\uparrow ( b\uparrow ( a\uparrow c ) ) = b\qquad\mbox{cnf}(c_{10},\mbox{axiom})$

$( a\uparrow a )\uparrow ( b\uparrow a )\ne a\qquad\mbox{cnf}(\mbox{prove\_meredith\_2\_basis}_1,\mbox{negated\_conjecture})$

\medskip\textbf{BOO002-2.p} In B3 algebra, X * X$\wedge$-1 * Y = Y






$m(m(v,w,x),y,m(v,w,z)) = m(v,w,m(x,y,z))\qquad\mbox{cnf}(\mbox{associativity},\mbox{axiom})$

$m(y,x,x) = x\qquad\mbox{cnf}(\mbox{ternary\_multiply}_1,\mbox{axiom})$

$m(x,x,y) = x\qquad\mbox{cnf}(\mbox{ternary\_multiply}_2,\mbox{axiom})$

$m(y',y,x) = x\qquad\mbox{cnf}(\mbox{left\_inverse},\mbox{axiom})$

$m(x,y,x) = x\qquad\mbox{cnf}(\mbox{extra\_lemma},\mbox{axiom})$

$m(a,a',b)\ne b\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{BOO019-1.p} Prove the independance of Ternary Boolean algebra axiom






$m(m(v,w,x),y,m(v,w,z)) = m(v,w,m(x,y,z))\qquad\mbox{cnf}(\mbox{associativity},\mbox{axiom})$

$m(x,x,y) = x\qquad\mbox{cnf}(\mbox{ternary\_multiply}_2,\mbox{axiom})$

$m(y',y,x) = x\qquad\mbox{cnf}(\mbox{left\_inverse},\mbox{axiom})$

$m(x,y,y') = x\qquad\mbox{cnf}(\mbox{right\_inverse},\mbox{axiom})$

$m(y,x,x)\ne x\qquad\mbox{cnf}(\mbox{prove\_ternary\_multiply\_1\_independant},\mbox{negated\_conjecture})$

\medskip
\end{document}