\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{ROB001-0.ax} Robbins algebra axioms






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

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

$-( -( x + y ) + -( x + -y ) ) = x\qquad\mbox{cnf}(\mbox{robbins\_axiom},\mbox{axiom})$

\medskip\textbf{ROB001-1.ax} Robbins algebra numbers axioms






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

$\mbox{positive\_integer}(x) \ \Rightarrow \ \mbox{successor}(v)\cdot x = x + v\cdot x\qquad\mbox{cnf}(\mbox{times\_by\_adding},\mbox{axiom})$

$\mbox{positive\_integer}(1)\qquad\mbox{cnf}(\mbox{one},\mbox{axiom})$

$\mbox{positive\_integer}(x) \ \Rightarrow \ \mbox{positive\_integer}(\mbox{successor}(x))\qquad\mbox{cnf}(\mbox{next\_integer},\mbox{axiom})$

\medskip\textbf{ROB006-1.p} Exists absorbed element =$>$ Boolean

If there are elements c and d such that c+d=d, then the
 algebra is Boolean.




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

$c + d = d\qquad\mbox{cnf}(\mbox{absorbtion},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB017-1.p} If -(2f + h) = -(3f + h) = -h then 2f + h = 3f + h

That is, 2f+h absorbs f.




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

$-( f + ( f + h ) ) = -h\qquad\mbox{cnf}(\mbox{condition}_1,\mbox{hypothesis})$

$-( f + ( f + ( f + h ) ) ) = -h\qquad\mbox{cnf}(\mbox{condition}_2,\mbox{hypothesis})$

$-( x + -y ) = -y \ \Rightarrow \ -( y + ( x + -( x + -y ) ) ) = -y\qquad\mbox{cnf}(\mbox{lemma\_3}_7,\mbox{axiom})$

$f + ( f + ( f + h ) )\ne f + ( f + h )\qquad\mbox{cnf}(\mbox{prove\_result},\mbox{negated\_conjecture})$

\medskip\textbf{ROB010-1.p} If -(a + -b) = c then -(c + -(b + a)) = a






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

$-( a + -b ) = c\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

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

\medskip\textbf{ROB004-1.p} c = -d, c + d=d, and c + c=c =$>$ Boolean

If there exist c, d such that c = -d, c+d=d, and c+c=c, then
 the algebra is Boolean.




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

$-d = c\qquad\mbox{cnf}(\mbox{negate\_d\_is\_c},\mbox{hypothesis})$

$c + d = d\qquad\mbox{cnf}(\mbox{c\_plus\_d\_is\_d},\mbox{hypothesis})$

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

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB003-1.p} X + c=c =$>$ Boolean

If there exists c such that X+c=c, then the algebra
 is Boolean.




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

$x + c = c\qquad\mbox{cnf}(\mbox{there\_exists\_a\_constant},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB022-1.p} c + -c=c =$>$ Boolean

If there is an element c such that c + -c = c then the
 algebra is Boolean.




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

$c + -c = c\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB032-2.p} Robbins =$>$ Exists absorbed element, with auxilliary definitions






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

$g(a) = -( a + -a )\qquad\mbox{cnf}(\mbox{sos}_{04},\mbox{axiom})$

$h(a) = a + ( a + ( a + g(a) ) )\qquad\mbox{cnf}(\mbox{sos}_{05},\mbox{axiom})$

$x_4 + x_5\ne x_5\qquad\mbox{cnf}(\mbox{goals},\mbox{negated\_conjecture})$

\medskip\textbf{ROB001-1.p} Is every Robbins algebra Boolean?






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

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB006-3.p} c + d=d =$>$ Boolean

If there are elements c and d such that c+d=d, then the
 algebra is Boolean.




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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$x + x\ne x\qquad\mbox{cnf}(\mbox{idempotence},\mbox{axiom})$

$( -( x + y ) = -y\mbox{ and }\mbox{positive\_integer}(v_2) ) \ \Rightarrow \ -( y + v_2\cdot ( x + -( x + -y ) ) ) = -y\qquad\mbox{cnf}(\mbox{corollary\_3}_7,\mbox{axiom})$

$-( x + -y ) = -y \ \Rightarrow \ y + \mbox{successor}(\mbox{successor}(1))\cdot ( x + -( x + -y ) ) = y + \mbox{successor}(1)\cdot ( x + -( x + -y ) )\qquad\mbox{cnf}(\mbox{corollary\_3\_9}_1,\mbox{axiom})$

$-( -y + -( x + -y ) ) = x \ \Rightarrow \ y + \mbox{successor}(\mbox{successor}(1))\cdot ( x + -( x + -y ) ) = y + \mbox{successor}(1)\cdot ( x + -( x + -y ) )\qquad\mbox{cnf}(\mbox{corollary\_3\_9}_2,\mbox{axiom})$

$c + d = d\qquad\mbox{cnf}(\mbox{absorbtion},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB005-1.p} Exists an idempotent element =$>$ Boolean

If there is an element c such that c+c=c, then the algebra
 is Boolean.




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

$c + c = c\qquad\mbox{cnf}(\mbox{idempotence},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB027-1.p} -(-c) = c =$>$ Boolean

If there are elements c and d such that c+d=d, then the
 algebra is Boolean.




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

$-( -c ) = c\qquad\mbox{cnf}(\mbox{double\_negation},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB020-2.p} -(a + -b)=b =$>$ Exists idempotent element

If there exist a, b such that -(a + -b) = b, the algebra
 is Boolean.




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

$-( a + -b ) = b\qquad\mbox{cnf}(\mbox{condition}_1,\mbox{hypothesis})$

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

\medskip\textbf{ROB035-1.p} Robbins =$>$ Exists absorbed within negation element






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

$g(a) = -( a + -a )\qquad\mbox{cnf}(\mbox{sos}_{04},\mbox{axiom})$

$h(a) = a + ( a + ( a + g(a) ) )\qquad\mbox{cnf}(\mbox{sos}_{05},\mbox{axiom})$

$-( x_8 + x_9 )\ne -x_9\qquad\mbox{cnf}(\mbox{goals},\mbox{negated\_conjecture})$

\medskip\textbf{ROB016-1.p} If -(d + e) = -e then -(e + k(d + -(d + -e))) = -e, for k$>$0






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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$-( d + e ) = -e\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$\mbox{positive\_integer}(k)\qquad\mbox{cnf}(\mbox{k\_positive},\mbox{axiom})$

$( -( -y + -( x + -y ) ) = x\mbox{ and }\mbox{positive\_integer}(\mbox{vk}) ) \ \Rightarrow \ -( y + \mbox{vk}\cdot ( x + -( x + -y ) ) ) = -y\qquad\mbox{cnf}(\mbox{lemma\_3}_6,\mbox{axiom})$

$-( e + k\cdot ( d + -( d + -e ) ) )\ne -e\qquad\mbox{cnf}(\mbox{prove\_result},\mbox{negated\_conjecture})$

\medskip\textbf{ROB025-1.p} -(X + Y) = intersection(-X,-Y) =$>$ Boolean

If for all X and Y, -(X + Y) = intersection(-X,-Y) then the
 algebra is Boolean.




$x{=}x\qquad\mbox{cnf}(\mbox{reflexivity},\mbox{axiom})$

$x{=}y \ \Rightarrow \ y{=}x\qquad\mbox{cnf}(\mbox{symmetry},\mbox{axiom})$

$( x{=}y\mbox{ and }y{=}z ) \ \Rightarrow \ x{=}z\qquad\mbox{cnf}(\mbox{transitivity},\mbox{axiom})$

$a{=}b \ \Rightarrow \ a + c{=}b + c\qquad\mbox{cnf}(\mbox{add\_substitution}_1,\mbox{axiom})$

$d{=}e \ \Rightarrow \ f + d{=}f + e\qquad\mbox{cnf}(\mbox{add\_substitution}_2,\mbox{axiom})$

$g{=}h \ \Rightarrow \ -g{=}-h\qquad\mbox{cnf}(\mbox{inverse\_substitution}_1,\mbox{axiom})$

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

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

$-( -( x + y ) + -( x + -y ) ){=}x\qquad\mbox{cnf}(\mbox{robbins\_axiom},\mbox{axiom})$

$-( x + y ){=}\mbox{intersect}(-x,-y)\qquad\mbox{cnf}(\mbox{the\_condition},\mbox{hypothesis})$

$\neg\,-( a + -b ) + -( -a + -b ){=}b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB033-1.p} Robbins problem with auxilliary definitions






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

$g(a) = -( a + -a )\qquad\mbox{cnf}(\mbox{sos}_{04},\mbox{axiom})$

$h(a) = a + ( a + ( a + g(a) ) )\qquad\mbox{cnf}(\mbox{sos}_{05},\mbox{axiom})$

$-( x_0 + -x_1 ) + -( -x_0 + -x_1 )\ne x_1\qquad\mbox{cnf}(\mbox{goals},\mbox{negated\_conjecture})$

\medskip\textbf{ROB032-1.p} Robbins =$>$ Exists absorbed element

If there are elements c and d such that c+d=d, then the
 algebra is Boolean.




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

$c + d\ne d\qquad\mbox{cnf}(\mbox{prove\_absorbtion},\mbox{negated\_conjecture})$

\medskip\textbf{ROB015-2.p} If -(-e + -(d + -e)) = d then -(e + k(d + -(d + -e))) = -e

This is the induction step of an induction proof.




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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$-( x + -( y + z ) ) = -( y + -( x + z ) ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{lemma\_3}_2,\mbox{axiom})$

$( -( x + -y ) = z\mbox{ and }\mbox{positive\_integer}(\mbox{vk}) ) \ \Rightarrow \ -( x + -( y + \mbox{vk}\cdot ( x + z ) ) ) = z\qquad\mbox{cnf}(\mbox{lemma\_3}_4,\mbox{axiom})$

$-( -e + -( d + -e ) ) = d\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$\mbox{positive\_integer}(k)\qquad\mbox{cnf}(\mbox{k\_positive},\mbox{axiom})$

$-( e + k\cdot ( d + -( d + -e ) ) )\ne -e\qquad\mbox{cnf}(\mbox{base\_step},\mbox{axiom})$

$-( e + \mbox{successor}(k)\cdot ( d + -( d + -e ) ) )\ne -e\qquad\mbox{cnf}(\mbox{prove\_induction\_step},\mbox{negated\_conjecture})$

\medskip\textbf{ROB014-1.p} If -(-e + -(d + -e)) = d then -(e + k(d + -(d + -e))) = -e, k=1

This is the base step of an induction proof.




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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$-( -e + -( d + -e ) ) = d\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$-( e + 1\cdot ( d + -( d + -e ) ) )\ne -e\qquad\mbox{cnf}(\mbox{prove\_base\_step},\mbox{negated\_conjecture})$

\medskip\textbf{ROB029-1.p} Robbins algebra numbers axioms






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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

\medskip\textbf{ROB015-1.p} If -(-e + -(d + -e)) = d then -(e + k(d + -(d + -e))) = -e

This is the induction step of an induction proof.




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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$-( -e + -( d + -e ) ) = d\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$\mbox{positive\_integer}(k)\qquad\mbox{cnf}(\mbox{k\_positive},\mbox{axiom})$

$-( e + k\cdot ( d + -( d + -e ) ) )\ne -e\qquad\mbox{cnf}(\mbox{base\_step},\mbox{axiom})$

$-( e + \mbox{successor}(k)\cdot ( d + -( d + -e ) ) )\ne -e\qquad\mbox{cnf}(\mbox{prove\_induction\_step},\mbox{negated\_conjecture})$

\medskip\textbf{ROB007-4.p} Absorbed within negation element =$>$ Exists idempotent element

If there exist a, b such that -(a+b) = -b, then the algebra
 is Boolean.




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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$x + y\ne y\qquad\mbox{cnf}(\mbox{absorbtion},\mbox{axiom})$

$-( x + -y ) = -y \ \Rightarrow \ y + \mbox{successor}(\mbox{successor}(1))\cdot ( x + -( x + -y ) ) = y + \mbox{successor}(1)\cdot ( x + -( x + -y ) )\qquad\mbox{cnf}(\mbox{corollary\_3\_9}_1,\mbox{axiom})$

$-( -y + -( x + -y ) ) = x \ \Rightarrow \ y + \mbox{successor}(\mbox{successor}(1))\cdot ( x + -( x + -y ) ) = y + \mbox{successor}(1)\cdot ( x + -( x + -y ) )\qquad\mbox{cnf}(\mbox{corollary\_3\_9}_2,\mbox{axiom})$

$-( a + b ) = -b\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

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

\medskip\textbf{ROB026-1.p} c + d = c =$>$ Boolean

If there are elements c and d such that c+d=d, then the
 algebra is Boolean.




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

$c + d = c\qquad\mbox{cnf}(\mbox{identity\_constant},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB028-1.p} Robbins algebra axioms






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

\medskip\textbf{ROB007-1.p} Absorbed within negation element =$>$ Boolean

If there exist a, b such that -(a+b) = -b, then the algebra
 is Boolean.




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

$-( a + b ) = -b\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB013-1.p} If -(a + b) = c then -(c + -(-b + a)) = a






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

$-( a + b ) = c\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

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

\medskip\textbf{ROB007-3.p} Absorbed within negation element =$>$ Boolean

If there exist a, b such that -(a+b) = -b, then the algebra
 is Boolean.




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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$x + y\ne y\qquad\mbox{cnf}(\mbox{absorbtion},\mbox{axiom})$

$-( x + -y ) = -y \ \Rightarrow \ y + \mbox{successor}(\mbox{successor}(1))\cdot ( x + -( x + -y ) ) = y + \mbox{successor}(1)\cdot ( x + -( x + -y ) )\qquad\mbox{cnf}(\mbox{corollary\_3\_9}_1,\mbox{axiom})$

$-( -y + -( x + -y ) ) = x \ \Rightarrow \ y + \mbox{successor}(\mbox{successor}(1))\cdot ( x + -( x + -y ) ) = y + \mbox{successor}(1)\cdot ( x + -( x + -y ) )\qquad\mbox{cnf}(\mbox{corollary\_3\_9}_2,\mbox{axiom})$

$-( a + b ) = -b\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB034-1.p} Robbins =$>$ Exists absorbed element, with auxilliary definitions






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

$g(a) = -( a + -a )\qquad\mbox{cnf}(\mbox{sos}_{04},\mbox{axiom})$

$h(a) = a + ( a + ( a + g(a) ) )\qquad\mbox{cnf}(\mbox{sos}_{05},\mbox{axiom})$

$x_2 + x_3\ne x_2\qquad\mbox{cnf}(\mbox{goals},\mbox{negated\_conjecture})$

\medskip\textbf{ROB023-1.p} X + X=X =$>$ Boolean

If for all X X + X = X then the algebra is Boolean.




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

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

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB020-1.p} -(a + -b)=b =$>$ Boolean

If there exist a, b such that -(a + -b) = b, the algebra
 is Boolean.




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

$-( a + -b ) = b\qquad\mbox{cnf}(\mbox{condition}_1,\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB008-1.p} If -(a + -(b + c)) = -(a + b + -c) then a+b=a






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

$-( a + -( b + c ) ) = -( a + ( b + -c ) )\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

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

\medskip\textbf{ROB014-2.p} If -(-e + -(d + -e)) = d then -(e + k(d + -(d + -e))) = -e, k=1

This is the base step of an induction proof.




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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$-( x + -( y + z ) ) = -( y + -( x + z ) ) \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{lemma\_3}_2,\mbox{axiom})$

$( -( x + -y ) = z\mbox{ and }\mbox{positive\_integer}(\mbox{vk}) ) \ \Rightarrow \ -( x + -( y + \mbox{vk}\cdot ( x + z ) ) ) = z\qquad\mbox{cnf}(\mbox{lemma\_3}_4,\mbox{axiom})$

$-( -e + -( d + -e ) ) = d\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$-( e + 1\cdot ( d + -( d + -e ) ) )\ne -e\qquad\mbox{cnf}(\mbox{prove\_base\_step},\mbox{negated\_conjecture})$

\medskip\textbf{ROB007-2.p} Absorbed within negation element =$>$ Exists idempotent element

If there exist a, b such that -(a+b) = -b, then the algebra
 is Boolean.




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

$-( a + b ) = -b\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

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

\medskip\textbf{ROB012-1.p} If -(a + -b) = c then -(a + -(b + k(a + c))) = c, k=k + 1

This is the induction step of an induction proof.




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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$-( a + -b ) = c\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$\mbox{positive\_integer}(k)\qquad\mbox{cnf}(\mbox{k\_an\_integer},\mbox{hypothesis})$

$-( a + -( b + k\cdot ( a + c ) ) ) = c\qquad\mbox{cnf}(\mbox{base\_step},\mbox{axiom})$

$-( a + -( b + \mbox{successor}(k)\cdot ( a + c ) ) )\ne c\qquad\mbox{cnf}(\mbox{prove\_induction\_step},\mbox{negated\_conjecture})$

\medskip\textbf{ROB024-1.p} -(a + (a + b)) + -(a + -b) = a =$>$ Boolean

If there exist a and b so that -(a + (a + b)) + -(a + -b)
 = a then the algebra is Boolean.




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

$-( -( a + ( a + b ) ) + -( a + -b ) ) = a\qquad\mbox{cnf}(\mbox{the\_condition},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB018-1.p} If -(d + e) = -e then e + 2(d + -(d + -e)) absorbs d + -(d + -e)






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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$-( d + -e ) = -e\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$e + \mbox{successor}(\mbox{successor}(1))\cdot ( d + -( d + -e ) )\ne e + \mbox{successor}(1)\cdot ( d + -( d + -e ) )\qquad\mbox{cnf}(\mbox{prove\_result},\mbox{negated\_conjecture})$

\medskip\textbf{ROB011-1.p} If -(a + -b) = c then -(a + -(b + k(a + c))) = c, k=1

This is the base step of an induction proof.




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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$-( a + -b ) = c\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$-( a + -( b + 1\cdot ( a + c ) ) )\ne c\qquad\mbox{cnf}(\mbox{prove\_base\_step},\mbox{negated\_conjecture})$

\medskip\textbf{ROB031-1.p} Robbins =$>$ Exists absorbed within negation element

If there are elements c and d such that c+d=d, then the
 algebra is Boolean.




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

$-( a + b )\ne -b\qquad\mbox{cnf}(\mbox{prove\_absorption\_within\_negation},\mbox{negated\_conjecture})$

\medskip\textbf{ROB012-2.p} If -(a + -b) = c then -(a + -(b + k(a + c))) = c, k=k + 1

This is the induction step of an induction proof.




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

$\mbox{include}(\mbox{'Axioms/ROB001-1.ax'})$

$-( x + -y ) = z \ \Rightarrow \ -( z + -( y + x ) ) = x\qquad\mbox{cnf}(\mbox{lemma\_3}_3,\mbox{axiom})$

$-( a + -b ) = c\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

$\mbox{positive\_integer}(k)\qquad\mbox{cnf}(\mbox{k\_an\_integer},\mbox{hypothesis})$

$-( a + -( b + k\cdot ( a + c ) ) ) = c\qquad\mbox{cnf}(\mbox{base\_step},\mbox{axiom})$

$-( a + -( b + \mbox{successor}(k)\cdot ( a + c ) ) )\ne c\qquad\mbox{cnf}(\mbox{prove\_induction\_step},\mbox{negated\_conjecture})$

\medskip\textbf{ROB006-2.p} Exists absorbed element =$>$ Exists idempotent element

If there are elements c and d such that c+d=d, then the
 algebra is Boolean.




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

$c + d = d\qquad\mbox{cnf}(\mbox{absorbtion},\mbox{hypothesis})$

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

\medskip\textbf{ROB021-1.p} (-X = -Y)=$>$(X = Y) =$>$ Boolean

If (-X = -Y) =$>$ (X = Y) then the algebra is Boolean.




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

$-x = -y \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{negative\_equality\_implies\_positive\_equality},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip\textbf{ROB030-1.p} Exists absorbed element =$>$ Exists absorbed within negation element

If there are elements c and d such that c+d=d, then the
 algebra is Boolean.




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

$c + d = d\qquad\mbox{cnf}(\mbox{absorbtion},\mbox{hypothesis})$

$-( a + b )\ne -b\qquad\mbox{cnf}(\mbox{prove\_absorption\_within\_negation},\mbox{negated\_conjecture})$

\medskip\textbf{ROB031-2.p} Robbins =$>$ Exists absorbed within negation element






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

$g(a) = -( a + -a )\qquad\mbox{cnf}(\mbox{sos}_{04},\mbox{axiom})$

$h(a) = a + ( a + ( a + g(a) ) )\qquad\mbox{cnf}(\mbox{sos}_{05},\mbox{axiom})$

$-( x_6 + x_7 )\ne -x_6\qquad\mbox{cnf}(\mbox{goals},\mbox{negated\_conjecture})$

\medskip\textbf{ROB009-1.p} If -(a + -(b + c)) = -(b + -(a + c)) then a = b






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

$-( a + -( b + c ) ) = -( b + -( a + c ) )\qquad\mbox{cnf}(\mbox{condition},\mbox{hypothesis})$

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

\medskip\textbf{ROB002-1.p} --X = X =$>$ Boolean

If --X = X then the algebra is Boolean.




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

$-( -x ) = x\qquad\mbox{cnf}(\mbox{double\_negation},\mbox{hypothesis})$

$-( a + -b ) + -( -a + -b )\ne b\qquad\mbox{cnf}(\mbox{prove\_huntingtons\_axiom},\mbox{negated\_conjecture})$

\medskip
\end{document}