\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{RNG003-0.ax} Alternative ring theory (equality) axioms






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

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

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{left\_multiplicative\_zero},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{right\_multiplicative\_zero},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

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

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

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

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

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

$( x\cdot x )\cdot y = x\cdot ( x\cdot y )\qquad\mbox{cnf}(\mbox{left\_alternative},\mbox{axiom})$

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

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

\medskip\textbf{RNG001-0.ax} Ring theory axioms






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

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

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

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

$-x + x{=}0\qquad\mbox{cnf}(\mbox{left\_inverse},\mbox{axiom})$

$x + -x{=}0\qquad\mbox{cnf}(\mbox{right\_inverse},\mbox{axiom})$

$( x + y{=}u\mbox{ and }y + z{=}v\mbox{ and }u + z{=}w ) \ \Rightarrow \ x + v{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_addition}_1,\mbox{axiom})$

$( x + y{=}u\mbox{ and }y + z{=}v\mbox{ and }x + v{=}w ) \ \Rightarrow \ u + z{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_addition}_2,\mbox{axiom})$

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

$( x\cdot y{=}u\mbox{ and }y\cdot z{=}v\mbox{ and }u\cdot z{=}w ) \ \Rightarrow \ x\cdot v{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_multiplication}_1,\mbox{axiom})$

$( x\cdot y{=}u\mbox{ and }y\cdot z{=}v\mbox{ and }x\cdot v{=}w ) \ \Rightarrow \ u\cdot z{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_multiplication}_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{=}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{RNG005-0.ax} Ring theory (equality) axioms






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

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

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

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

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

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

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

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

\medskip\textbf{RNG002-0.ax} Ring theory (equality) axioms






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

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

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

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

$-0 = 0\qquad\mbox{cnf}(\mbox{additive\_inverse\_identity},\mbox{axiom})$

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{multiply\_additive\_id}_1,\mbox{axiom})$

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{multiply\_additive\_id}_2,\mbox{axiom})$

$-( x + y ) = -x + -y\qquad\mbox{cnf}(\mbox{distribute\_additive\_inverse},\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{multiply\_additive\_inverse}_1,\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{multiply\_additive\_inverse}_2,\mbox{axiom})$

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

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

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

\medskip\textbf{RNG004-0.ax} Alternative ring theory (equality) axioms






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

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{left\_multiplicative\_zero},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{right\_multiplicative\_zero},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{add\_inverse},\mbox{axiom})$

$-( x + y ) = -x + -y\qquad\mbox{cnf}(\mbox{sum\_of\_inverses},\mbox{axiom})$

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

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

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

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

$( x\cdot x )\cdot y = x\cdot ( x\cdot y )\qquad\mbox{cnf}(\mbox{left\_alternative},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

$-0 = 0\qquad\mbox{cnf}(\mbox{inverse\_additive\_identity},\mbox{axiom})$

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

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

$x + z = y + z \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{left\_cancellation\_for\_addition},\mbox{axiom})$

$z + x = z + y \ \Rightarrow \ x = y\qquad\mbox{cnf}(\mbox{right\_cancellation\_for\_addition},\mbox{axiom})$

\medskip\textbf{RNG042-3.p} Ring theory (equality) axioms






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

\medskip\textbf{RNG021-7.p} Third part of the linearised form of the associator

The associator can be expressed in another form called
 a linearised form. There are three clauses to be proved
 to establish the equivalence of the two forms.




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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{associator}(u + v,x,y)\ne \mbox{associator}(u,x,y) + \mbox{associator}(v,x,y)\qquad\mbox{cnf}(\mbox{prove\_linearised\_form}_3,\mbox{negated\_conjecture})$

\medskip\textbf{RNG015-6.p} X*(Y+ -Z) = (X*Y) + -(X*Z)






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

$x\cdot ( y + -z )\ne x\cdot y + -x\cdot z\qquad\mbox{cnf}(\mbox{prove\_distributivity},\mbox{negated\_conjecture})$

\medskip\textbf{RNG008-6.p} Boolean rings are commutative

Given a ring in which for all x, x * x = x, prove that for
 all x and y, x * y = y * x.




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

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

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

$x\cdot x{=}x\qquad\mbox{cnf}(\mbox{x\_squared\_is\_x},\mbox{hypothesis})$

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

$\neg\,b\cdot a{=}c\qquad\mbox{cnf}(\mbox{prove\_b\_times\_a\_is\_c},\mbox{negated\_conjecture})$

\medskip\textbf{RNG032-7.p} 6*assr(X,X,Y)$\wedge$6 = additive identity






$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

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

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

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

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

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{left\_multiplicative\_zero},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{right\_multiplicative\_zero},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

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

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

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

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

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

$( ( ( ( \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) )\ne 0\qquad\mbox{cnf}(\mbox{prove\_conjecture}_3,\mbox{negated\_conjecture})$

\medskip\textbf{RNG032-6.p} 6*assr(X,X,Y)$\wedge$6 = additive identity






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

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

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

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

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{left\_multiplicative\_zero},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{right\_multiplicative\_zero},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

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

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

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

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

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

$( ( ( ( \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) )\ne 0\qquad\mbox{cnf}(\mbox{prove\_conjecture}_3,\mbox{negated\_conjecture})$

\medskip\textbf{RNG001-3.p} X.additive\_identity = additive\_identity for any X






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

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

$( x + y{=}u\mbox{ and }y + z{=}v\mbox{ and }u + z{=}w ) \ \Rightarrow \ x + v{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_addition}_1,\mbox{axiom})$

$( x + y{=}u\mbox{ and }y + z{=}v\mbox{ and }x + v{=}w ) \ \Rightarrow \ u + z{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_addition}_2,\mbox{axiom})$

$x\cdot y{=}x\cdot y\qquad\mbox{cnf}(\mbox{closure\_of\_multiplication},\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})$

$\neg\,a\cdot 0{=}0\qquad\mbox{cnf}(\mbox{prove\_a\_times\_additive\_id\_is\_additive\_id},\mbox{negated\_conjecture})$

\medskip\textbf{RNG004-2.p} X*Y = -X*-Y






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

$( x + y{=}z\mbox{ and }x + w{=}z ) \ \Rightarrow \ y = w\qquad\mbox{cnf}(\mbox{cancellation}_1,\mbox{axiom})$

$( x + y{=}z\mbox{ and }w + y{=}z ) \ \Rightarrow \ x = w\qquad\mbox{cnf}(\mbox{cancellation}_2,\mbox{axiom})$

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

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

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

\medskip\textbf{RNG025-9.p} Middle or Flexible Law






$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

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

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

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

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

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{left\_multiplicative\_zero},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{right\_multiplicative\_zero},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

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

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

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

$( x\cdot x )\cdot y = x\cdot ( x\cdot y )\qquad\mbox{cnf}(\mbox{left\_alternative},\mbox{axiom})$

$\mbox{associator}(x,y,u + v) = \mbox{associator}(x,y,u) + \mbox{associator}(x,y,v)\qquad\mbox{cnf}(\mbox{linearised\_associator}_1,\mbox{axiom})$

$\mbox{associator}(x,u + v,y) = \mbox{associator}(x,u,y) + \mbox{associator}(x,v,y)\qquad\mbox{cnf}(\mbox{linearised\_associator}_2,\mbox{axiom})$

$\mbox{associator}(u + v,x,y) = \mbox{associator}(u,x,y) + \mbox{associator}(v,x,y)\qquad\mbox{cnf}(\mbox{linearised\_associator}_3,\mbox{axiom})$

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

$\mbox{associator}(a,b,c) + \mbox{associator}(a,c,b)\ne 0\qquad\mbox{cnf}(\mbox{prove\_flexible\_law},\mbox{negated\_conjecture})$

\medskip\textbf{RNG006-1.p} X*(Y+ -Z) = (X*Y) + -(X*Z)






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

$a\cdot b{=}c \ \Rightarrow \ a\cdot ( -b ){=}-c\qquad\mbox{cnf}(\mbox{product\_lemma}_1,\mbox{axiom})$

$a\cdot b{=}c \ \Rightarrow \ ( -a )\cdot b{=}-c\qquad\mbox{cnf}(\mbox{product\_lemma}_2,\mbox{axiom})$

$a\cdot b{=}c \ \Rightarrow \ ( -a )\cdot ( -b ){=}c\qquad\mbox{cnf}(\mbox{product\_lemma}_3,\mbox{axiom})$

$b + -c{=}\mbox{bS\_Ic}\qquad\mbox{cnf}(\mbox{b\_plus\_inverse\_c},\mbox{hypothesis})$

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

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

$\mbox{aPb} + -\mbox{aPc}{=}\mbox{aPb\_S\_IaPc}\qquad\mbox{cnf}(\mbox{aPb\_plus\_IaPc},\mbox{hypothesis})$

$\neg\,a\cdot \mbox{bS\_Ic}{=}\mbox{aPb\_S\_IaPc}\qquad\mbox{cnf}(\mbox{prove\_a\_times\_bS\_Ic\_is\_aPb\_S\_\_IaPc},\mbox{negated\_conjecture})$

\medskip\textbf{RNG036-7.p} If X*X*X*X*X = X then the ring is commutative

Given a ring in which for all x, x * x * x * x * x = x, prove
 that for all x and y, x * y = y * x.




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

$x\cdot ( x\cdot ( x\cdot ( x\cdot x ) ) ) = x\qquad\mbox{cnf}(\mbox{x\_fifthed\_is\_x},\mbox{hypothesis})$

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

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

\medskip\textbf{RNG008-7.p} Boolean rings are commutative

Given a ring in which for all x, x * x = x, prove that for
 all x and y, x * y = y * x.




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

$x\cdot x = x\qquad\mbox{cnf}(\mbox{boolean\_ring},\mbox{hypothesis})$

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

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

\medskip\textbf{RNG010-2.p} Skew symmetry of the auxilliary function

The left and right Moufang identities imply the skew symmetry
 of s(W,X,Y,Z) = (W*X,Y,Z) - X*(W,Y,Z) - (X,Y,Z)*W.
 Recall that skew symmetry means that the function sign
 changes when any two arguments are swapped. This problem
 proves the case for swapping the first two arguments.




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

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

$( y\cdot x )\cdot y\ne y\cdot ( x\cdot y )\qquad\mbox{cnf}(\mbox{middle\_law},\mbox{axiom})$

$\mbox{associator}(y,x,z)\ne -\mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{associator\_skew\_symmetry}_1,\mbox{axiom})$

$\mbox{associator}(z,y,x)\ne -\mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{associator\_skew\_symmetry}_2,\mbox{axiom})$

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

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

$\mbox{associator}(\mbox{cx}\cdot \mbox{cx},\mbox{cy},\mbox{cz})\ne \mbox{associator}(\mbox{cx},\mbox{cy},\mbox{cz})\cdot \mbox{cx} + \mbox{cx}\cdot \mbox{associator}(\mbox{cx},\mbox{cy},\mbox{cz})\qquad\mbox{cnf}(\mbox{prove\_skew\_symmetry},\mbox{negated\_conjecture})$

\medskip\textbf{RNG010-7.p} Skew symmetry of the auxilliary function

The three Moufang identities imply the skew symmetry
 of s(W,X,Y,Z) = (W*X,Y,Z) - X*(W,Y,Z) - (X,Y,Z)*W.
 Recall that skew symmetry means that the function sign
 changes when any two arguments are swapped. This problem
 proves the case for swapping the first two arguments.




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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$s(w,x,y,z) = ( \mbox{associator}(w\cdot x,y,z) + -x\cdot \mbox{associator}(w,y,z) ) + -\mbox{associator}(x,y,z)\cdot w\qquad\mbox{cnf}(\mbox{defines\_s},\mbox{axiom})$

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

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

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

$s(a,b,c,d)\ne -s(b,a,c,d)\qquad\mbox{cnf}(\mbox{prove\_skew\_symmetry},\mbox{negated\_conjecture})$

\medskip\textbf{RNG002-1.p} Right cancellation for addition






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

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

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

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

\medskip\textbf{RNG028-5.p} Left Moufang identity






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

$( \mbox{cx}\cdot ( \mbox{cy}\cdot \mbox{cx} ) )\cdot \mbox{cz}\ne \mbox{cx}\cdot ( \mbox{cy}\cdot ( \mbox{cx}\cdot \mbox{cz} ) )\qquad\mbox{cnf}(\mbox{prove\_left\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG028-1.p} Left Moufang identity






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

$( \mbox{cx}\cdot ( \mbox{cy}\cdot \mbox{cx} ) )\cdot \mbox{cz}\ne \mbox{cx}\cdot ( \mbox{cy}\cdot ( \mbox{cx}\cdot \mbox{cz} ) )\qquad\mbox{cnf}(\mbox{prove\_left\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG008-3.p} Boolean rings are commutative

Given a ring in which for all x, x * x = x, prove that for
 all x and y, x * y = y * x.




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

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

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_inverse},\mbox{axiom})$

$x\cdot x = x\qquad\mbox{cnf}(\mbox{boolean\_ring},\mbox{hypothesis})$

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

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

\medskip\textbf{RNG026-6.p} Teichmuller Identity






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

$( \mbox{associator}(a\cdot b,c,d) + \mbox{associator}(a,b,c\cdot d) ) + -( ( \mbox{associator}(a,b\cdot c,d) + a\cdot \mbox{associator}(b,c,d) ) + \mbox{associator}(a,b,c)\cdot d )\ne 0\qquad\mbox{cnf}(\mbox{prove\_teichmuller\_identity},\mbox{negated\_conjecture})$

\medskip\textbf{RNG045+1.p} Cauchy-Bouniakowsky-Schwarz inequality 01\_02, 00 expansion






$\forall w_0{:}\;( \mbox{aNaturalNumber}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mNatSort},\mbox{axiom})$

$\mbox{aNaturalNumber}_0(\mbox{sz}_{00})\qquad\mbox{fof}(\mbox{mZeroNat},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aNaturalNumber}_0(w_0) \ \Rightarrow \ ( \mbox{aNaturalNumber}_0(\mbox{szszuzczcdt}_0(w_0))\mbox{ and }\mbox{szszuzczcdt}_0(w_0)\ne \mbox{sz}_{00} ) )\qquad\mbox{fof}(\mbox{mSuccNat},\mbox{axiom})$

$\forall w_0{:}\;( ( \mbox{aNaturalNumber}_0(w_0)\mbox{ and }w_0\ne \mbox{sz}_{00} ) \ \Rightarrow \ \exists w_1{:}\;( \mbox{aNaturalNumber}_0(w_1)\mbox{ and }w_0 = \mbox{szszuzczcdt}_0(w_1) ) )\qquad\mbox{fof}(\mbox{mNatExtr},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aNaturalNumber}_0(w_0)\mbox{ and }\mbox{aNaturalNumber}_0(w_1) ) \ \Rightarrow \ ( \mbox{szszuzczcdt}_0(w_0) = \mbox{szszuzczcdt}_0(w_1) \ \Rightarrow \ w_0 = w_1 ) )\qquad\mbox{fof}(\mbox{mSuccEqu},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aNaturalNumber}_0(w_0)\mbox{ and }\mbox{aNaturalNumber}_0(w_1) ) \ \Rightarrow \ ( \mbox{iLess}_0(w_0,w_1) \ \Rightarrow \ \mbox{\$true} ) )\qquad\mbox{fof}(\mbox{mIHOrd},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aNaturalNumber}_0(w_0) \ \Rightarrow \ \mbox{iLess}_0(w_0,\mbox{szszuzczcdt}_0(w_0)) )\qquad\mbox{fof}(\mbox{mIH},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aScalar}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mScSort},\mbox{axiom})$

$\mbox{aScalar}_0(\mbox{sz0z}_{00})\qquad\mbox{fof}(\mbox{mSZeroSc},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1) ) \ \Rightarrow \ \mbox{aScalar}_0(\mbox{sdtpldt}_0(w_0,w_1)) )\qquad\mbox{fof}(\mbox{mSumSc},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1) ) \ \Rightarrow \ \mbox{aScalar}_0(\mbox{sdtasdt}_0(w_0,w_1)) )\qquad\mbox{fof}(\mbox{mMulSc},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aScalar}_0(w_0) \ \Rightarrow \ \mbox{aScalar}_0(\mbox{smndt}_0(w_0)) )\qquad\mbox{fof}(\mbox{mNegSc},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aScalar}_0(w_0) \ \Rightarrow \ ( \mbox{sdtpldt}_0(w_0,\mbox{sz0z}_{00}) = w_0\mbox{ and }\mbox{sdtpldt}_0(\mbox{sz0z}_{00},w_0) = w_0\mbox{ and }\mbox{sdtasdt}_0(w_0,\mbox{sz0z}_{00}) = \mbox{sz0z}_{00}\mbox{ and }\mbox{sdtasdt}_0(\mbox{sz0z}_{00},w_0) = \mbox{sz0z}_{00}\mbox{ and }\mbox{sdtpldt}_0(w_0,\mbox{smndt}_0(w_0)) = \mbox{sz0z}_{00}\mbox{ and }\mbox{sdtpldt}_0(\mbox{smndt}_0(w_0),w_0) = \mbox{sz0z}_{00}\mbox{ and }\mbox{smndt}_0(\mbox{smndt}_0(w_0)) = w_0\mbox{ and }\mbox{smndt}_0(\mbox{sz0z}_{00}) = \mbox{sz0z}_{00} ) )\qquad\mbox{fof}(\mbox{mScZero},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1)\mbox{ and }\mbox{aScalar}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtpldt}_0(\mbox{sdtpldt}_0(w_0,w_1),w_2) = \mbox{sdtpldt}_0(w_0,\mbox{sdtpldt}_0(w_1,w_2))\mbox{ and }\mbox{sdtpldt}_0(w_0,w_1) = \mbox{sdtpldt}_0(w_1,w_0)\mbox{ and }\mbox{sdtasdt}_0(\mbox{sdtasdt}_0(w_0,w_1),w_2) = \mbox{sdtasdt}_0(w_0,\mbox{sdtasdt}_0(w_1,w_2))\mbox{ and }\mbox{sdtasdt}_0(w_0,w_1) = \mbox{sdtasdt}_0(w_1,w_0) ) )\qquad\mbox{fof}(\mbox{mArith},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1)\mbox{ and }\mbox{aScalar}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtasdt}_0(w_0,\mbox{sdtpldt}_0(w_1,w_2)) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_0,w_1),\mbox{sdtasdt}_0(w_0,w_2))\mbox{ and }\mbox{sdtasdt}_0(\mbox{sdtpldt}_0(w_0,w_1),w_2) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_0,w_2),\mbox{sdtasdt}_0(w_1,w_2)) ) )\qquad\mbox{fof}(\mbox{mDistr},\mbox{axiom})$

$\mbox{aScalar}_0(\mbox{xx})\mbox{ and }\mbox{aScalar}_0(\mbox{xy})\mbox{ and }\mbox{aScalar}_0(\mbox{xu})\mbox{ and }\mbox{aScalar}_0(\mbox{xv})\qquad\mbox{fof}(\mbox{m\_}_{674},\mbox{hypothesis})$

$\mbox{sdtasdt}_0(\mbox{sdtpldt}_0(\mbox{xx},\mbox{xy}),\mbox{sdtpldt}_0(\mbox{xu},\mbox{xv})) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(\mbox{xx},\mbox{sdtpldt}_0(\mbox{xu},\mbox{xv})),\mbox{sdtasdt}_0(\mbox{xy},\mbox{sdtpldt}_0(\mbox{xu},\mbox{xv})))\qquad\mbox{fof}(\mbox{m\_}_{733},\mbox{hypothesis})$

$\mbox{sdtasdt}_0(\mbox{sdtpldt}_0(\mbox{xx},\mbox{xy}),\mbox{sdtpldt}_0(\mbox{xu},\mbox{xv})) = \mbox{sdtpldt}_0(\mbox{sdtpldt}_0(\mbox{sdtasdt}_0(\mbox{xx},\mbox{xu}),\mbox{sdtasdt}_0(\mbox{xx},\mbox{xv})),\mbox{sdtpldt}_0(\mbox{sdtasdt}_0(\mbox{xy},\mbox{xu}),\mbox{sdtasdt}_0(\mbox{xy},\mbox{xv})))\qquad\mbox{fof}(\mbox{m\_\_},\mbox{conjecture})$

\medskip\textbf{RNG083+1.p} Chinese remainder theorem in a ring 02, 00 expansion






$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mElmSort},\mbox{axiom})$

$\mbox{aElement}_0(\mbox{sz}_{00})\qquad\mbox{fof}(\mbox{mSortsC},\mbox{axiom})$

$\mbox{aElement}_0(\mbox{sz}_{10})\qquad\mbox{fof}(\mbox{mSortsC}_{01},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ \mbox{aElement}_0(\mbox{smndt}_0(w_0)) )\qquad\mbox{fof}(\mbox{mSortsU},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1) ) \ \Rightarrow \ \mbox{aElement}_0(\mbox{sdtpldt}_0(w_0,w_1)) )\qquad\mbox{fof}(\mbox{mSortsB},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1) ) \ \Rightarrow \ \mbox{aElement}_0(\mbox{sdtasdt}_0(w_0,w_1)) )\qquad\mbox{fof}(\mbox{mSortsB}_{02},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1) ) \ \Rightarrow \ \mbox{sdtpldt}_0(w_0,w_1) = \mbox{sdtpldt}_0(w_1,w_0) )\qquad\mbox{fof}(\mbox{mAddComm},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ \mbox{sdtpldt}_0(\mbox{sdtpldt}_0(w_0,w_1),w_2) = \mbox{sdtpldt}_0(w_0,\mbox{sdtpldt}_0(w_1,w_2)) )\qquad\mbox{fof}(\mbox{mAddAsso},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ ( \mbox{sdtpldt}_0(w_0,\mbox{sz}_{00}) = w_0\mbox{ and }w_0 = \mbox{sdtpldt}_0(\mbox{sz}_{00},w_0) ) )\qquad\mbox{fof}(\mbox{mAddZero},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ ( \mbox{sdtpldt}_0(w_0,\mbox{smndt}_0(w_0)) = \mbox{sz}_{00}\mbox{ and }\mbox{sz}_{00} = \mbox{sdtpldt}_0(\mbox{smndt}_0(w_0),w_0) ) )\qquad\mbox{fof}(\mbox{mAddInvr},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1) ) \ \Rightarrow \ \mbox{sdtasdt}_0(w_0,w_1) = \mbox{sdtasdt}_0(w_1,w_0) )\qquad\mbox{fof}(\mbox{mMulComm},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ \mbox{sdtasdt}_0(\mbox{sdtasdt}_0(w_0,w_1),w_2) = \mbox{sdtasdt}_0(w_0,\mbox{sdtasdt}_0(w_1,w_2)) )\qquad\mbox{fof}(\mbox{mMulAsso},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ ( \mbox{sdtasdt}_0(w_0,\mbox{sz}_{10}) = w_0\mbox{ and }w_0 = \mbox{sdtasdt}_0(\mbox{sz}_{10},w_0) ) )\qquad\mbox{fof}(\mbox{mMulUnit},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtasdt}_0(w_0,\mbox{sdtpldt}_0(w_1,w_2)) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_0,w_1),\mbox{sdtasdt}_0(w_0,w_2))\mbox{ and }\mbox{sdtasdt}_0(\mbox{sdtpldt}_0(w_1,w_2),w_0) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_1,w_0),\mbox{sdtasdt}_0(w_2,w_0)) ) )\qquad\mbox{fof}(\mbox{mAMDistr},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ ( \mbox{sdtasdt}_0(\mbox{smndt}_0(\mbox{sz}_{10}),w_0) = \mbox{smndt}_0(w_0)\mbox{ and }\mbox{smndt}_0(w_0) = \mbox{sdtasdt}_0(w_0,\mbox{smndt}_0(\mbox{sz}_{10})) ) )\qquad\mbox{fof}(\mbox{mMulMnOne},\mbox{axiom})$

$\mbox{aElement}_0(\mbox{xx})\qquad\mbox{fof}(\mbox{m\_}_{468},\mbox{hypothesis})$

$\mbox{sdtasdt}_0(\mbox{xx},\mbox{sz}_{00}) = \mbox{sz}_{00}\mbox{ and }\mbox{sz}_{00} = \mbox{sdtasdt}_0(\mbox{sz}_{00},\mbox{xx})\qquad\mbox{fof}(\mbox{m\_\_},\mbox{conjecture})$

\medskip\textbf{RNG033-7.p} A fairly complex equation with associators

assr(X.Y,Z,W)+assr(X,Y,comm(Z,W)) = X.assr(Y,Z,W)+assr(X,Z,W).Y




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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{associator}(x\cdot y,z,w) + \mbox{associator}(x,y,\mbox{commutator}(z,w))\ne x\cdot \mbox{associator}(y,z,w) + \mbox{associator}(x,z,w)\cdot y\qquad\mbox{cnf}(\mbox{prove\_challenge},\mbox{negated\_conjecture})$

\medskip\textbf{RNG029-1.p} Middle Moufang identity






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

$( \mbox{cx}\cdot \mbox{cy} )\cdot ( \mbox{cz}\cdot \mbox{cx} )\ne \mbox{cx}\cdot ( ( \mbox{cy}\cdot \mbox{cz} )\cdot \mbox{cx} )\qquad\mbox{cnf}(\mbox{prove\_middle\_law},\mbox{negated\_conjecture})$

\medskip\textbf{RNG005-1.p} (-X*Y) + (X*Y) = additive\_identity






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

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

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

$\neg\,c + d{=}0\qquad\mbox{cnf}(\mbox{prove\_sum\_is\_additive\_id},\mbox{negated\_conjecture})$

\medskip\textbf{RNG026-7.p} Teichmuller Identity






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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$( \mbox{associator}(a\cdot b,c,d) + \mbox{associator}(a,b,c\cdot d) ) + -( ( \mbox{associator}(a,b\cdot c,d) + a\cdot \mbox{associator}(b,c,d) ) + \mbox{associator}(a,b,c)\cdot d )\ne 0\qquad\mbox{cnf}(\mbox{prove\_teichmuller\_identity},\mbox{negated\_conjecture})$

\medskip\textbf{RNG020-6.p} Second part of the linearised form of the associator

The associator can be expressed in another form called
 a linearised form. There are three clauses to be proved
 to establish the equivalence of the two forms.




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

$\mbox{associator}(x,u + v,y)\ne \mbox{associator}(x,u,y) + \mbox{associator}(x,v,y)\qquad\mbox{cnf}(\mbox{prove\_linearised\_form}_2,\mbox{negated\_conjecture})$

\medskip\textbf{RNG009-7.p} If X*X*X = X then the ring is commutative

Given a ring in which for all x, x * x * x = x, prove that
 for all x and y, x * y = y * x.




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

$x\cdot ( x\cdot x ) = x\qquad\mbox{cnf}(\mbox{x\_cubed\_is\_x},\mbox{hypothesis})$

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

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

\medskip\textbf{RNG003-1.p} Left cancellation for addition






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

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

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

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

\medskip\textbf{RNG044+1.p} Cauchy-Bouniakowsky-Schwarz inequality 01, 00 expansion






$\forall w_0{:}\;( \mbox{aNaturalNumber}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mNatSort},\mbox{axiom})$

$\mbox{aNaturalNumber}_0(\mbox{sz}_{00})\qquad\mbox{fof}(\mbox{mZeroNat},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aNaturalNumber}_0(w_0) \ \Rightarrow \ ( \mbox{aNaturalNumber}_0(\mbox{szszuzczcdt}_0(w_0))\mbox{ and }\mbox{szszuzczcdt}_0(w_0)\ne \mbox{sz}_{00} ) )\qquad\mbox{fof}(\mbox{mSuccNat},\mbox{axiom})$

$\forall w_0{:}\;( ( \mbox{aNaturalNumber}_0(w_0)\mbox{ and }w_0\ne \mbox{sz}_{00} ) \ \Rightarrow \ \exists w_1{:}\;( \mbox{aNaturalNumber}_0(w_1)\mbox{ and }w_0 = \mbox{szszuzczcdt}_0(w_1) ) )\qquad\mbox{fof}(\mbox{mNatExtr},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aNaturalNumber}_0(w_0)\mbox{ and }\mbox{aNaturalNumber}_0(w_1) ) \ \Rightarrow \ ( \mbox{szszuzczcdt}_0(w_0) = \mbox{szszuzczcdt}_0(w_1) \ \Rightarrow \ w_0 = w_1 ) )\qquad\mbox{fof}(\mbox{mSuccEqu},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aNaturalNumber}_0(w_0)\mbox{ and }\mbox{aNaturalNumber}_0(w_1) ) \ \Rightarrow \ ( \mbox{iLess}_0(w_0,w_1) \ \Rightarrow \ \mbox{\$true} ) )\qquad\mbox{fof}(\mbox{mIHOrd},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aNaturalNumber}_0(w_0) \ \Rightarrow \ \mbox{iLess}_0(w_0,\mbox{szszuzczcdt}_0(w_0)) )\qquad\mbox{fof}(\mbox{mIH},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aScalar}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mScSort},\mbox{axiom})$

$\mbox{aScalar}_0(\mbox{sz0z}_{00})\qquad\mbox{fof}(\mbox{mSZeroSc},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1) ) \ \Rightarrow \ \mbox{aScalar}_0(\mbox{sdtpldt}_0(w_0,w_1)) )\qquad\mbox{fof}(\mbox{mSumSc},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1) ) \ \Rightarrow \ \mbox{aScalar}_0(\mbox{sdtasdt}_0(w_0,w_1)) )\qquad\mbox{fof}(\mbox{mMulSc},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aScalar}_0(w_0) \ \Rightarrow \ \mbox{aScalar}_0(\mbox{smndt}_0(w_0)) )\qquad\mbox{fof}(\mbox{mNegSc},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aScalar}_0(w_0) \ \Rightarrow \ ( \mbox{sdtpldt}_0(w_0,\mbox{sz0z}_{00}) = w_0\mbox{ and }\mbox{sdtpldt}_0(\mbox{sz0z}_{00},w_0) = w_0\mbox{ and }\mbox{sdtasdt}_0(w_0,\mbox{sz0z}_{00}) = \mbox{sz0z}_{00}\mbox{ and }\mbox{sdtasdt}_0(\mbox{sz0z}_{00},w_0) = \mbox{sz0z}_{00}\mbox{ and }\mbox{sdtpldt}_0(w_0,\mbox{smndt}_0(w_0)) = \mbox{sz0z}_{00}\mbox{ and }\mbox{sdtpldt}_0(\mbox{smndt}_0(w_0),w_0) = \mbox{sz0z}_{00}\mbox{ and }\mbox{smndt}_0(\mbox{smndt}_0(w_0)) = w_0\mbox{ and }\mbox{smndt}_0(\mbox{sz0z}_{00}) = \mbox{sz0z}_{00} ) )\qquad\mbox{fof}(\mbox{mScZero},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1)\mbox{ and }\mbox{aScalar}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtpldt}_0(\mbox{sdtpldt}_0(w_0,w_1),w_2) = \mbox{sdtpldt}_0(w_0,\mbox{sdtpldt}_0(w_1,w_2))\mbox{ and }\mbox{sdtpldt}_0(w_0,w_1) = \mbox{sdtpldt}_0(w_1,w_0)\mbox{ and }\mbox{sdtasdt}_0(\mbox{sdtasdt}_0(w_0,w_1),w_2) = \mbox{sdtasdt}_0(w_0,\mbox{sdtasdt}_0(w_1,w_2))\mbox{ and }\mbox{sdtasdt}_0(w_0,w_1) = \mbox{sdtasdt}_0(w_1,w_0) ) )\qquad\mbox{fof}(\mbox{mArith},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1)\mbox{ and }\mbox{aScalar}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtasdt}_0(w_0,\mbox{sdtpldt}_0(w_1,w_2)) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_0,w_1),\mbox{sdtasdt}_0(w_0,w_2))\mbox{ and }\mbox{sdtasdt}_0(\mbox{sdtpldt}_0(w_0,w_1),w_2) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_0,w_2),\mbox{sdtasdt}_0(w_1,w_2)) ) )\qquad\mbox{fof}(\mbox{mDistr},\mbox{axiom})$

$\mbox{aScalar}_0(\mbox{xx})\mbox{ and }\mbox{aScalar}_0(\mbox{xy})\mbox{ and }\mbox{aScalar}_0(\mbox{xu})\mbox{ and }\mbox{aScalar}_0(\mbox{xv})\qquad\mbox{fof}(\mbox{m\_}_{674},\mbox{hypothesis})$

$\mbox{sdtasdt}_0(\mbox{sdtpldt}_0(\mbox{xx},\mbox{xy}),\mbox{sdtpldt}_0(\mbox{xu},\mbox{xv})) = \mbox{sdtpldt}_0(\mbox{sdtpldt}_0(\mbox{sdtasdt}_0(\mbox{xx},\mbox{xu}),\mbox{sdtasdt}_0(\mbox{xx},\mbox{xv})),\mbox{sdtpldt}_0(\mbox{sdtasdt}_0(\mbox{xy},\mbox{xu}),\mbox{sdtasdt}_0(\mbox{xy},\mbox{xv})))\qquad\mbox{fof}(\mbox{m\_\_},\mbox{conjecture})$

\medskip\textbf{RNG027-9.p} Right Moufang identity






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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{associator}(x,x\cdot y,z)\ne \mbox{associator}(x,y,z)\cdot x\qquad\mbox{cnf}(\mbox{prove\_right\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG007-5.p} In Boolean rings, X is its own inverse

Given a ring in which for all x, x * x = x, prove that for
 all x, x + x = additive\_identity.




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

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

$-( -x ) + 0{=}x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$x\cdot 0{=}0\qquad\mbox{cnf}(\mbox{multiply\_additive\_id}_1,\mbox{axiom})$

$0\cdot x{=}0\qquad\mbox{cnf}(\mbox{multiply\_additive\_id}_2,\mbox{axiom})$

$-x + -y{=}-( x + y )\qquad\mbox{cnf}(\mbox{distribute\_additive\_inverse},\mbox{axiom})$

$x\cdot ( -y ){=}-x\cdot y\qquad\mbox{cnf}(\mbox{multiply\_additive\_inverse},\mbox{axiom})$

$x\cdot x{=}x\qquad\mbox{cnf}(\mbox{x\_squared\_is\_x},\mbox{hypothesis})$

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

\medskip\textbf{RNG041-1.p} Unknown






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

$0\cdot a{=}0\qquad\mbox{cnf}(\mbox{multiplicative\_identity}_1,\mbox{hypothesis})$

$a\cdot 0{=}0\qquad\mbox{cnf}(\mbox{multiplicative\_identity}_2,\mbox{hypothesis})$

$a\cdot 1{=}a\qquad\mbox{cnf}(\mbox{right\_multiplicative\_identity},\mbox{hypothesis})$

$1\cdot a{=}a\qquad\mbox{cnf}(\mbox{left\_multiplicative\_identity},\mbox{hypothesis})$

$a\cdot h(a){=}1\mbox{ or }a = 0\qquad\mbox{cnf}(\mbox{clause}_{41},\mbox{hypothesis})$

$h(a)\cdot a{=}1\mbox{ or }a = 0\qquad\mbox{cnf}(\mbox{clause}_{42},\mbox{hypothesis})$

$a\cdot b{=}0\qquad\mbox{cnf}(\mbox{a\_times\_b},\mbox{negated\_conjecture})$

$a\ne 0\qquad\mbox{cnf}(\mbox{a\_not\_additive\_identity},\mbox{negated\_conjecture})$

$b\ne 0\qquad\mbox{cnf}(\mbox{prove\_b\_is\_additive\_identity},\mbox{negated\_conjecture})$

\medskip\textbf{RNG029-2.p} Middle Moufang identity






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

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

$( y\cdot x )\cdot y = y\cdot ( x\cdot y )\qquad\mbox{cnf}(\mbox{middle\_law},\mbox{axiom})$

$\mbox{associator}(y,x,z) = -\mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{associator\_skew\_symmetry}_1,\mbox{axiom})$

$\mbox{associator}(z,y,x) = -\mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{associator\_skew\_symmetry}_2,\mbox{axiom})$

$( \mbox{cx}\cdot \mbox{cy} )\cdot ( \mbox{cz}\cdot \mbox{cx} )\ne \mbox{cx}\cdot ( ( \mbox{cy}\cdot \mbox{cz} )\cdot \mbox{cx} )\qquad\mbox{cnf}(\mbox{prove\_middle\_law},\mbox{negated\_conjecture})$

\medskip\textbf{RNG042-1.p} Ring theory axioms






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

\medskip\textbf{RNG029-6.p} Middle Moufang identity






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

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

\medskip\textbf{RNG010-1.p} Skew symmetry of the auxilliary function

The left and right Moufang identities imply the skew symmetry
 of s(W,X,Y,Z) = (W*X,Y,Z) - X*(W,Y,Z) - (X,Y,Z)*W.
 Recall that skew symmetry means that the function sign
 changes when any two arguments are swapped. This problem
 proves the case for swapping the first two arguments.




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

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

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

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

$\mbox{associator}(\mbox{cx}\cdot \mbox{cx},\mbox{cy},\mbox{cz})\ne \mbox{associator}(\mbox{cx},\mbox{cy},\mbox{cz})\cdot \mbox{cx} + \mbox{cx}\cdot \mbox{associator}(\mbox{cx},\mbox{cy},\mbox{cz})\qquad\mbox{cnf}(\mbox{prove\_skew\_symmetry},\mbox{negated\_conjecture})$

\medskip\textbf{RNG016-6.p} (X+ -Y)*Z = (X*Z) + -(Y*Z)






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

$( x + -y )\cdot z\ne x\cdot z + -y\cdot z\qquad\mbox{cnf}(\mbox{prove\_distributivity},\mbox{negated\_conjecture})$

\medskip\textbf{RNG012-6.p} Product of inverses equal product






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

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

\medskip\textbf{RNG043-2.p} Alternative ring theory (equality) axioms






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

\medskip\textbf{RNG030-7.p} 2*assr(X,X,Y)$\wedge$3 = additive identity






$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

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

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

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

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

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{left\_multiplicative\_zero},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{right\_multiplicative\_zero},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

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

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

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

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

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

$\mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) )\ne 0\qquad\mbox{cnf}(\mbox{prove\_conjecture}_1,\mbox{negated\_conjecture})$

\medskip\textbf{RNG034-1.p} A skew symmetry relation of the associator






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

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

$\mbox{associator}(\mbox{cy},\mbox{cx},\mbox{cz})\ne -\mbox{associator}(\mbox{cx},\mbox{cy},\mbox{cz})\qquad\mbox{cnf}(\mbox{prove\_skew\_symmetry},\mbox{negated\_conjecture})$

\medskip\textbf{RNG027-2.p} Right Moufang identity






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

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

$( y\cdot x )\cdot y = y\cdot ( x\cdot y )\qquad\mbox{cnf}(\mbox{middle\_law},\mbox{axiom})$

$\mbox{associator}(y,x,z) = -\mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{associator\_skew\_symmetry}_1,\mbox{axiom})$

$\mbox{associator}(z,y,x) = -\mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{associator\_skew\_symmetry}_2,\mbox{axiom})$

$\mbox{cz}\cdot ( \mbox{cx}\cdot ( \mbox{cy}\cdot \mbox{cx} ) )\ne ( ( \mbox{cz}\cdot \mbox{cx} )\cdot \mbox{cy} )\cdot \mbox{cx}\qquad\mbox{cnf}(\mbox{prove\_right\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG028-9.p} Left Moufang identity






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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{associator}(x,y\cdot x,z)\ne x\cdot \mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{prove\_left\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG046+1.p} Cauchy-Bouniakowsky-Schwarz inequality 02, 00 expansion






$\forall w_0{:}\;( \mbox{aNaturalNumber}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mNatSort},\mbox{axiom})$

$\mbox{aNaturalNumber}_0(\mbox{sz}_{00})\qquad\mbox{fof}(\mbox{mZeroNat},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aNaturalNumber}_0(w_0) \ \Rightarrow \ ( \mbox{aNaturalNumber}_0(\mbox{szszuzczcdt}_0(w_0))\mbox{ and }\mbox{szszuzczcdt}_0(w_0)\ne \mbox{sz}_{00} ) )\qquad\mbox{fof}(\mbox{mSuccNat},\mbox{axiom})$

$\forall w_0{:}\;( ( \mbox{aNaturalNumber}_0(w_0)\mbox{ and }w_0\ne \mbox{sz}_{00} ) \ \Rightarrow \ \exists w_1{:}\;( \mbox{aNaturalNumber}_0(w_1)\mbox{ and }w_0 = \mbox{szszuzczcdt}_0(w_1) ) )\qquad\mbox{fof}(\mbox{mNatExtr},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aNaturalNumber}_0(w_0)\mbox{ and }\mbox{aNaturalNumber}_0(w_1) ) \ \Rightarrow \ ( \mbox{szszuzczcdt}_0(w_0) = \mbox{szszuzczcdt}_0(w_1) \ \Rightarrow \ w_0 = w_1 ) )\qquad\mbox{fof}(\mbox{mSuccEqu},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aNaturalNumber}_0(w_0)\mbox{ and }\mbox{aNaturalNumber}_0(w_1) ) \ \Rightarrow \ ( \mbox{iLess}_0(w_0,w_1) \ \Rightarrow \ \mbox{\$true} ) )\qquad\mbox{fof}(\mbox{mIHOrd},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aNaturalNumber}_0(w_0) \ \Rightarrow \ \mbox{iLess}_0(w_0,\mbox{szszuzczcdt}_0(w_0)) )\qquad\mbox{fof}(\mbox{mIH},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aScalar}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mScSort},\mbox{axiom})$

$\mbox{aScalar}_0(\mbox{sz0z}_{00})\qquad\mbox{fof}(\mbox{mSZeroSc},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1) ) \ \Rightarrow \ \mbox{aScalar}_0(\mbox{sdtpldt}_0(w_0,w_1)) )\qquad\mbox{fof}(\mbox{mSumSc},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1) ) \ \Rightarrow \ \mbox{aScalar}_0(\mbox{sdtasdt}_0(w_0,w_1)) )\qquad\mbox{fof}(\mbox{mMulSc},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aScalar}_0(w_0) \ \Rightarrow \ \mbox{aScalar}_0(\mbox{smndt}_0(w_0)) )\qquad\mbox{fof}(\mbox{mNegSc},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aScalar}_0(w_0) \ \Rightarrow \ ( \mbox{sdtpldt}_0(w_0,\mbox{sz0z}_{00}) = w_0\mbox{ and }\mbox{sdtpldt}_0(\mbox{sz0z}_{00},w_0) = w_0\mbox{ and }\mbox{sdtasdt}_0(w_0,\mbox{sz0z}_{00}) = \mbox{sz0z}_{00}\mbox{ and }\mbox{sdtasdt}_0(\mbox{sz0z}_{00},w_0) = \mbox{sz0z}_{00}\mbox{ and }\mbox{sdtpldt}_0(w_0,\mbox{smndt}_0(w_0)) = \mbox{sz0z}_{00}\mbox{ and }\mbox{sdtpldt}_0(\mbox{smndt}_0(w_0),w_0) = \mbox{sz0z}_{00}\mbox{ and }\mbox{smndt}_0(\mbox{smndt}_0(w_0)) = w_0\mbox{ and }\mbox{smndt}_0(\mbox{sz0z}_{00}) = \mbox{sz0z}_{00} ) )\qquad\mbox{fof}(\mbox{mScZero},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1)\mbox{ and }\mbox{aScalar}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtpldt}_0(\mbox{sdtpldt}_0(w_0,w_1),w_2) = \mbox{sdtpldt}_0(w_0,\mbox{sdtpldt}_0(w_1,w_2))\mbox{ and }\mbox{sdtpldt}_0(w_0,w_1) = \mbox{sdtpldt}_0(w_1,w_0)\mbox{ and }\mbox{sdtasdt}_0(\mbox{sdtasdt}_0(w_0,w_1),w_2) = \mbox{sdtasdt}_0(w_0,\mbox{sdtasdt}_0(w_1,w_2))\mbox{ and }\mbox{sdtasdt}_0(w_0,w_1) = \mbox{sdtasdt}_0(w_1,w_0) ) )\qquad\mbox{fof}(\mbox{mArith},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1)\mbox{ and }\mbox{aScalar}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtasdt}_0(w_0,\mbox{sdtpldt}_0(w_1,w_2)) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_0,w_1),\mbox{sdtasdt}_0(w_0,w_2))\mbox{ and }\mbox{sdtasdt}_0(\mbox{sdtpldt}_0(w_0,w_1),w_2) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_0,w_2),\mbox{sdtasdt}_0(w_1,w_2)) ) )\qquad\mbox{fof}(\mbox{mDistr},\mbox{axiom})$

$\forall w_0,w_1,w_2,w_3{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1)\mbox{ and }\mbox{aScalar}_0(w_2)\mbox{ and }\mbox{aScalar}_0(w_3) ) \ \Rightarrow \ \mbox{sdtasdt}_0(\mbox{sdtpldt}_0(w_0,w_1),\mbox{sdtpldt}_0(w_2,w_3)) = \mbox{sdtpldt}_0(\mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_0,w_2),\mbox{sdtasdt}_0(w_0,w_3)),\mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_1,w_2),\mbox{sdtasdt}_0(w_1,w_3))) )\qquad\mbox{fof}(\mbox{mDistr}_2,\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aScalar}_0(w_0)\mbox{ and }\mbox{aScalar}_0(w_1) ) \ \Rightarrow \ ( \mbox{sdtasdt}_0(w_0,\mbox{smndt}_0(w_1)) = \mbox{smndt}_0(\mbox{sdtasdt}_0(w_0,w_1))\mbox{ and }\mbox{sdtasdt}_0(\mbox{smndt}_0(w_0),w_1) = \mbox{smndt}_0(\mbox{sdtasdt}_0(w_0,w_1)) ) )\qquad\mbox{fof}(\mbox{mMNeg},\mbox{axiom})$

$\mbox{aScalar}_0(\mbox{xx})\mbox{ and }\mbox{aScalar}_0(\mbox{xy})\qquad\mbox{fof}(\mbox{m\_}_{799},\mbox{hypothesis})$

$\mbox{sdtasdt}_0(\mbox{smndt}_0(\mbox{xx}),\mbox{smndt}_0(\mbox{xy})) = \mbox{sdtasdt}_0(\mbox{xx},\mbox{xy})\qquad\mbox{fof}(\mbox{m\_\_},\mbox{conjecture})$

\medskip\textbf{RNG027-8.p} Right Moufang identity






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

$\mbox{associator}(x,x\cdot y,z)\ne \mbox{associator}(x,y,z)\cdot x\qquad\mbox{cnf}(\mbox{prove\_right\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG040-2.p} Ring property 4






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

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

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

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

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

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

$( x + y{=}u\mbox{ and }y + z{=}v\mbox{ and }u + z{=}w ) \ \Rightarrow \ x + v{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_addition}_1,\mbox{axiom})$

$( x + y{=}u\mbox{ and }y + z{=}v\mbox{ and }x + v{=}w ) \ \Rightarrow \ u + z{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_addition}_2,\mbox{axiom})$

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

$( x\cdot y{=}u\mbox{ and }y\cdot z{=}v\mbox{ and }u\cdot z{=}w ) \ \Rightarrow \ x\cdot v{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_multiplication}_1,\mbox{axiom})$

$( x\cdot y{=}u\mbox{ and }y\cdot z{=}v\mbox{ and }x\cdot v{=}w ) \ \Rightarrow \ u\cdot z{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_multiplication}_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{=}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})$

$a\cdot 1{=}a\qquad\mbox{cnf}(\mbox{right\_multiplicative\_identity},\mbox{hypothesis})$

$1\cdot a{=}a\qquad\mbox{cnf}(\mbox{left\_multiplicative\_identity},\mbox{hypothesis})$

$a\cdot h(a){=}1\mbox{ or }a = 0\qquad\mbox{cnf}(\mbox{clause}_{30},\mbox{hypothesis})$

$h(a)\cdot a{=}1\mbox{ or }a = 0\qquad\mbox{cnf}(\mbox{clause}_{31},\mbox{hypothesis})$

$a\cdot b{=}c \ \Rightarrow \ b\cdot a{=}c\qquad\mbox{cnf}(\mbox{product\_symmetry},\mbox{hypothesis})$

$b + c{=}d\qquad\mbox{cnf}(\mbox{b\_plus\_c},\mbox{negated\_conjecture})$

$d\cdot a{=}0\qquad\mbox{cnf}(\mbox{d\_plus\_a},\mbox{negated\_conjecture})$

$b\cdot a{=}l\qquad\mbox{cnf}(\mbox{b\_plus\_a},\mbox{negated\_conjecture})$

$c\cdot a{=}n\qquad\mbox{cnf}(\mbox{c\_plus\_a},\mbox{negated\_conjecture})$

$\neg\,l + n{=}0\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{RNG004-1.p} X*Y = -X*-Y






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

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

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

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

\medskip\textbf{RNG025-5.p} Middle or Flexible Law






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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{associator}(x,y,z) + \mbox{associator}(x,z,y)\ne 0\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{RNG030-6.p} 2*assr(X,X,Y)$\wedge$3 = additive identity






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

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

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

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

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{left\_multiplicative\_zero},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{right\_multiplicative\_zero},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

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

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

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

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

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

$\mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) ) + \mbox{associator}(x,x,y)\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) )\ne 0\qquad\mbox{cnf}(\mbox{prove\_conjecture}_1,\mbox{negated\_conjecture})$

\medskip\textbf{RNG008-4.p} Boolean rings are commutative

Given a ring in which for all x, x * x = x, prove that for
 all x and y, x * y = y * x.




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

$x\cdot x = x\qquad\mbox{cnf}(\mbox{boolean\_ring},\mbox{hypothesis})$

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

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

\medskip\textbf{RNG023-6.p} Left alternative






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

$\mbox{associator}(x,x,y)\ne 0\qquad\mbox{cnf}(\mbox{prove\_left\_alternative},\mbox{negated\_conjecture})$

\medskip\textbf{RNG011-5.p} In a right alternative ring (((X,X,Y)*X)*(X,X,Y)) = Add Id






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

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

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

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

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$-0 = 0\qquad\mbox{cnf}(\mbox{additive\_inverse\_identity},\mbox{axiom})$

$x + ( -x + y ) = y\qquad\mbox{cnf}(\mbox{property\_of\_inverse\_and\_add},\mbox{axiom})$

$-( x + y ) = -x + -y\qquad\mbox{cnf}(\mbox{distribute\_additive\_inverse},\mbox{axiom})$

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{multiply\_additive\_id}_1,\mbox{axiom})$

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{multiply\_additive\_id}_2,\mbox{axiom})$

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverse},\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{multiply\_additive\_inverse}_1,\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{multiply\_additive\_inverse}_2,\mbox{axiom})$

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

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

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

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

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

$( \mbox{associator}(x,x,y)\cdot x )\cdot \mbox{associator}(x,x,y) = 0\qquad\mbox{cnf}(\mbox{middle\_associator},\mbox{axiom})$

$( \mbox{associator}(a,a,b)\cdot a )\cdot \mbox{associator}(a,a,b)\ne 0\qquad\mbox{cnf}(\mbox{prove\_equality},\mbox{negated\_conjecture})$

\medskip\textbf{RNG027-5.p} Right Moufang identity






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

$\mbox{cz}\cdot ( \mbox{cx}\cdot ( \mbox{cy}\cdot \mbox{cx} ) )\ne ( ( \mbox{cz}\cdot \mbox{cx} )\cdot \mbox{cy} )\cdot \mbox{cx}\qquad\mbox{cnf}(\mbox{prove\_right\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG021-6.p} Third part of the linearised form of the associator

The associator can be expressed in another form called
 a linearised form. There are three clauses to be proved
 to establish the equivalence of the two forms.




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

$\mbox{associator}(u + v,x,y)\ne \mbox{associator}(u,x,y) + \mbox{associator}(v,x,y)\qquad\mbox{cnf}(\mbox{prove\_linearised\_form}_3,\mbox{negated\_conjecture})$

\medskip\textbf{RNG006-3.p} X*(Y+ -Z) = (X*Y) + -(X*Z)






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

$b + -c{=}\mbox{bS\_Ic}\qquad\mbox{cnf}(\mbox{b\_plus\_inverse\_c},\mbox{hypothesis})$

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

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

$\mbox{aPb} + -\mbox{aPc}{=}\mbox{aPb\_S\_IaPc}\qquad\mbox{cnf}(\mbox{aPb\_plus\_IaPc},\mbox{hypothesis})$

$\neg\,a\cdot \mbox{bS\_Ic}{=}\mbox{aPb\_S\_IaPc}\qquad\mbox{cnf}(\mbox{prove\_a\_times\_bS\_Ic\_is\_aPb\_S\_\_IaPc},\mbox{negated\_conjecture})$

\medskip\textbf{RNG018-6.p} (X+Y)* -Z = -(X*Z) + -(Y*Z)






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

$( x + y )\cdot ( -z )\ne -x\cdot z + -y\cdot z\qquad\mbox{cnf}(\mbox{prove\_distributivity},\mbox{negated\_conjecture})$

\medskip\textbf{RNG128-1.p} In commutative semirings with 1+x+x$\wedge$2=x, the operations coincide






$a + ( b + c ) = ( a + b ) + c\qquad\mbox{cnf}(\mbox{sos},\mbox{axiom})$

$a + b = b + a\qquad\mbox{cnf}(\mbox{sos}_{001},\mbox{axiom})$

$a\cdot b = b\cdot a\qquad\mbox{cnf}(\mbox{sos}_{002},\mbox{axiom})$

$a\cdot ( b + c ) = a\cdot b + a\cdot c\qquad\mbox{cnf}(\mbox{sos}_{003},\mbox{axiom})$

$0 + a = a\qquad\mbox{cnf}(\mbox{sos}_{004},\mbox{axiom})$

$a\cdot 1 = a\qquad\mbox{cnf}(\mbox{sos}_{005},\mbox{axiom})$

$1 + ( a + a\cdot a ) = a\qquad\mbox{cnf}(\mbox{sos}_{006},\mbox{axiom})$

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

\medskip\textbf{RNG013-6.p} -X*Y = -(X*Y)






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

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

\medskip\textbf{RNG129-1.p} Separativity in rings






$0 + a = a\qquad\mbox{cnf}(\mbox{sos},\mbox{axiom})$

$a + 0 = a\qquad\mbox{cnf}(\mbox{sos}_{001},\mbox{axiom})$

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

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

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

$( a + b ) + c = a + ( b + c )\qquad\mbox{cnf}(\mbox{sos}_{005},\mbox{axiom})$

$a + b = b + a\qquad\mbox{cnf}(\mbox{sos}_{006},\mbox{axiom})$

$a\cdot 1 = a\qquad\mbox{cnf}(\mbox{sos}_{007},\mbox{axiom})$

$1\cdot a = a\qquad\mbox{cnf}(\mbox{sos}_{008},\mbox{axiom})$

$( a\cdot b )\cdot c = a\cdot ( b\cdot c )\qquad\mbox{cnf}(\mbox{sos}_{009},\mbox{axiom})$

$0\cdot a = 0\qquad\mbox{cnf}(\mbox{sos}_{010},\mbox{axiom})$

$a\cdot 0 = 0\qquad\mbox{cnf}(\mbox{sos}_{011},\mbox{axiom})$

$a\cdot b + a\cdot c = a\cdot ( b + c )\qquad\mbox{cnf}(\mbox{sos}_{012},\mbox{axiom})$

$a\cdot b + c\cdot b = ( a + c )\cdot b\qquad\mbox{cnf}(\mbox{sos}_{013},\mbox{axiom})$

$a\cdot ( a^{-1}\cdot a ) = a\qquad\mbox{cnf}(\mbox{sos}_{014},\mbox{axiom})$

$a^{-1}\cdot ( a\cdot a^{-1} ) = a^{-1}\qquad\mbox{cnf}(\mbox{sos}_{015},\mbox{axiom})$

$a_0 + ( a_1 + ( b_0 + b_1 ) ) = 1\qquad\mbox{cnf}(\mbox{sos}_{016},\mbox{axiom})$

$a_0\cdot a_0 = a_0\qquad\mbox{cnf}(\mbox{sos}_{017},\mbox{axiom})$

$a_1\cdot a_1 = a_1\qquad\mbox{cnf}(\mbox{sos}_{018},\mbox{axiom})$

$b_0\cdot b_0 = b_0\qquad\mbox{cnf}(\mbox{sos}_{019},\mbox{axiom})$

$b_1\cdot b_1 = b_1\qquad\mbox{cnf}(\mbox{sos}_{020},\mbox{axiom})$

$a_0\cdot a_1 = 0\qquad\mbox{cnf}(\mbox{sos}_{021},\mbox{axiom})$

$a_1\cdot a_0 = 0\qquad\mbox{cnf}(\mbox{sos}_{022},\mbox{axiom})$

$a_0\cdot b_0 = 0\qquad\mbox{cnf}(\mbox{sos}_{023},\mbox{axiom})$

$b_0\cdot a_0 = 0\qquad\mbox{cnf}(\mbox{sos}_{024},\mbox{axiom})$

$a_0\cdot b_1 = 0\qquad\mbox{cnf}(\mbox{sos}_{025},\mbox{axiom})$

$b_1\cdot a_0 = 0\qquad\mbox{cnf}(\mbox{sos}_{026},\mbox{axiom})$

$a_1\cdot b_0 = 0\qquad\mbox{cnf}(\mbox{sos}_{027},\mbox{axiom})$

$b_0\cdot a_1 = 0\qquad\mbox{cnf}(\mbox{sos}_{028},\mbox{axiom})$

$a_1\cdot b_1 = 0\qquad\mbox{cnf}(\mbox{sos}_{029},\mbox{axiom})$

$b_1\cdot a_1 = 0\qquad\mbox{cnf}(\mbox{sos}_{030},\mbox{axiom})$

$b_0\cdot b_1 = 0\qquad\mbox{cnf}(\mbox{sos}_{031},\mbox{axiom})$

$b_1\cdot b_0 = 0\qquad\mbox{cnf}(\mbox{sos}_{032},\mbox{axiom})$

$u\cdot u = 1\qquad\mbox{cnf}(\mbox{sos}_{033},\mbox{axiom})$

$u\cdot ( a_0\cdot u ) = a_1\qquad\mbox{cnf}(\mbox{sos}_{034},\mbox{axiom})$

$u\cdot ( b_0\cdot u ) = b_1\qquad\mbox{cnf}(\mbox{sos}_{035},\mbox{axiom})$

$a_0 + a_1 = c\cdot d\qquad\mbox{cnf}(\mbox{sos}_{036},\mbox{axiom})$

$a_1 + b_0 = d\cdot c\qquad\mbox{cnf}(\mbox{sos}_{037},\mbox{axiom})$

$c = ( a_0 + a_1 )\cdot ( c\cdot ( a_1 + b_0 ) )\qquad\mbox{cnf}(\mbox{sos}_{038},\mbox{axiom})$

$d = ( a_1 + b_0 )\cdot ( d\cdot ( a_0 + a_1 ) )\qquad\mbox{cnf}(\mbox{sos}_{039},\mbox{axiom})$

$a_1 + b_0 = e\cdot f\qquad\mbox{cnf}(\mbox{sos}_{040},\mbox{axiom})$

$b_0 + b_1 = f\cdot e\qquad\mbox{cnf}(\mbox{sos}_{041},\mbox{axiom})$

$e = ( a_1 + b_0 )\cdot ( e\cdot ( b_0 + b_1 ) )\qquad\mbox{cnf}(\mbox{sos}_{042},\mbox{axiom})$

$f = ( b_0 + b_1 )\cdot ( f\cdot ( a_1 + b_0 ) )\qquad\mbox{cnf}(\mbox{sos}_{043},\mbox{axiom})$

$a\cdot b = a_0 \ \Rightarrow \ b\cdot a\ne b_0\qquad\mbox{cnf}(\mbox{sos}_{044},\mbox{negated\_conjecture})$

\medskip\textbf{RNG082+1.p} Chinese remainder theorem in a ring 01, 00 expansion






$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mElmSort},\mbox{axiom})$

$\mbox{aElement}_0(\mbox{sz}_{00})\qquad\mbox{fof}(\mbox{mSortsC},\mbox{axiom})$

$\mbox{aElement}_0(\mbox{sz}_{10})\qquad\mbox{fof}(\mbox{mSortsC}_{01},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ \mbox{aElement}_0(\mbox{smndt}_0(w_0)) )\qquad\mbox{fof}(\mbox{mSortsU},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1) ) \ \Rightarrow \ \mbox{aElement}_0(\mbox{sdtpldt}_0(w_0,w_1)) )\qquad\mbox{fof}(\mbox{mSortsB},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1) ) \ \Rightarrow \ \mbox{aElement}_0(\mbox{sdtasdt}_0(w_0,w_1)) )\qquad\mbox{fof}(\mbox{mSortsB}_{02},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1) ) \ \Rightarrow \ \mbox{sdtpldt}_0(w_0,w_1) = \mbox{sdtpldt}_0(w_1,w_0) )\qquad\mbox{fof}(\mbox{mAddComm},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ \mbox{sdtpldt}_0(\mbox{sdtpldt}_0(w_0,w_1),w_2) = \mbox{sdtpldt}_0(w_0,\mbox{sdtpldt}_0(w_1,w_2)) )\qquad\mbox{fof}(\mbox{mAddAsso},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ ( \mbox{sdtpldt}_0(w_0,\mbox{sz}_{00}) = w_0\mbox{ and }w_0 = \mbox{sdtpldt}_0(\mbox{sz}_{00},w_0) ) )\qquad\mbox{fof}(\mbox{mAddZero},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ ( \mbox{sdtpldt}_0(w_0,\mbox{smndt}_0(w_0)) = \mbox{sz}_{00}\mbox{ and }\mbox{sz}_{00} = \mbox{sdtpldt}_0(\mbox{smndt}_0(w_0),w_0) ) )\qquad\mbox{fof}(\mbox{mAddInvr},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1) ) \ \Rightarrow \ \mbox{sdtasdt}_0(w_0,w_1) = \mbox{sdtasdt}_0(w_1,w_0) )\qquad\mbox{fof}(\mbox{mMulComm},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ \mbox{sdtasdt}_0(\mbox{sdtasdt}_0(w_0,w_1),w_2) = \mbox{sdtasdt}_0(w_0,\mbox{sdtasdt}_0(w_1,w_2)) )\qquad\mbox{fof}(\mbox{mMulAsso},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ ( \mbox{sdtasdt}_0(w_0,\mbox{sz}_{10}) = w_0\mbox{ and }w_0 = \mbox{sdtasdt}_0(\mbox{sz}_{10},w_0) ) )\qquad\mbox{fof}(\mbox{mMulUnit},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtasdt}_0(w_0,\mbox{sdtpldt}_0(w_1,w_2)) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_0,w_1),\mbox{sdtasdt}_0(w_0,w_2))\mbox{ and }\mbox{sdtasdt}_0(\mbox{sdtpldt}_0(w_1,w_2),w_0) = \mbox{sdtpldt}_0(\mbox{sdtasdt}_0(w_1,w_0),\mbox{sdtasdt}_0(w_2,w_0)) ) )\qquad\mbox{fof}(\mbox{mAMDistr},\mbox{axiom})$

$\mbox{aElement}_0(\mbox{xx})\qquad\mbox{fof}(\mbox{m\_}_{444},\mbox{hypothesis})$

$\mbox{sdtasdt}_0(\mbox{smndt}_0(\mbox{sz}_{10}),\mbox{xx}) = \mbox{smndt}_0(\mbox{xx})\qquad\mbox{fof}(\mbox{m\_\_},\mbox{conjecture})$

\medskip\textbf{RNG033-9.p} A fairly complex equation with associators

assr(X.Y,Z,W)+assr(X,Y,comm(Z,W)) = X.assr(Y,Z,W)+assr(X,Z,W).Y




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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

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

$\mbox{associator}(x\cdot y,z,w) + \mbox{associator}(x,y,\mbox{commutator}(z,w))\ne x\cdot \mbox{associator}(y,z,w) + \mbox{associator}(x,z,w)\cdot y\qquad\mbox{cnf}(\mbox{prove\_challenge},\mbox{negated\_conjecture})$

\medskip\textbf{RNG035-7.p} If X*X*X*X = X then the ring is commutative

Given a ring in which for all x, x * x * x * x = x, prove
 that for all x and y, x * y = y * x.




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

$x\cdot ( x\cdot ( x\cdot x ) ) = x\qquad\mbox{cnf}(\mbox{x\_fourthed\_is\_x},\mbox{hypothesis})$

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

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

\medskip\textbf{RNG007-4.p} In Boolean rings, X is its own inverse

Given a ring in which for all x, x * x = x, prove that for
 all x, x + x = additive\_identity




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

$x\cdot x = x\qquad\mbox{cnf}(\mbox{boolean\_ring},\mbox{hypothesis})$

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

\medskip\textbf{RNG127+1.p} Proper integral domains






$\forall a{:}\;a + m(a) = n\qquad\mbox{fof}(f_{01},\mbox{axiom})$

$\forall a{:}\;a + n = a\qquad\mbox{fof}(f_{02},\mbox{axiom})$

$\forall a,b,c{:}\;a + ( b + c ) = ( a + b ) + c\qquad\mbox{fof}(f_{03},\mbox{axiom})$

$\forall a,b{:}\;a + b = b + a\qquad\mbox{fof}(f_{04},\mbox{axiom})$

$\forall a{:}\;a\cdot e = a\qquad\mbox{fof}(f_{05},\mbox{axiom})$

$\forall a,b,c{:}\;a\cdot ( b\cdot c ) = ( a\cdot b )\cdot c\qquad\mbox{fof}(f_{06},\mbox{axiom})$

$\forall a,b{:}\;a\cdot b = b\cdot a\qquad\mbox{fof}(f_{07},\mbox{axiom})$

$\forall a,b,c{:}\;a\cdot ( b + c ) = a\cdot b + a\cdot c\qquad\mbox{fof}(f_{08},\mbox{axiom})$

$\forall a,b{:}\;( a\cdot b = n \ \Rightarrow \ ( a = n\mbox{ or }b = n ) )\qquad\mbox{fof}(f_{09},\mbox{axiom})$

$\exists a{:}\;\forall b{:}\;( a\ne n\mbox{ and }a\cdot b\ne e )\qquad\mbox{fof}(f_{10},\mbox{axiom})$

\medskip\textbf{RNG027-7.p} Right Moufang identity






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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{cz}\cdot ( \mbox{cx}\cdot ( \mbox{cy}\cdot \mbox{cx} ) )\ne ( ( \mbox{cz}\cdot \mbox{cx} )\cdot \mbox{cy} )\cdot \mbox{cx}\qquad\mbox{cnf}(\mbox{prove\_right\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG029-3.p} Middle Moufang identity






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

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

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

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

$( y\cdot x )\cdot y = y\cdot ( x\cdot y )\qquad\mbox{cnf}(\mbox{middle\_law},\mbox{axiom})$

$\mbox{associator}(y,x,z) = -\mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{associator\_skew\_symmetry}_1,\mbox{axiom})$

$\mbox{associator}(z,y,x) = -\mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{associator\_skew\_symmetry}_2,\mbox{axiom})$

$( \mbox{cx}\cdot \mbox{cy} )\cdot ( \mbox{cz}\cdot \mbox{cx} )\ne \mbox{cx}\cdot ( ( \mbox{cy}\cdot \mbox{cz} )\cdot \mbox{cx} )\qquad\mbox{cnf}(\mbox{prove\_middle\_law},\mbox{negated\_conjecture})$

\medskip\textbf{RNG033-6.p} A fairly complex equation with associators

assr(X.Y,Z,W)+assr(X,Y,comm(Z,W)) = X.assr(Y,Z,W)+assr(X,Z,W).Y




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

$\mbox{associator}(x\cdot y,z,w) + \mbox{associator}(x,y,\mbox{commutator}(z,w))\ne x\cdot \mbox{associator}(y,z,w) + \mbox{associator}(x,z,w)\cdot y\qquad\mbox{cnf}(\mbox{prove\_challenge},\mbox{negated\_conjecture})$

\medskip\textbf{RNG001-4.p} X.additive\_identity = additive\_identity for any X






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

$( x + y{=}z\mbox{ and }x + w{=}z ) \ \Rightarrow \ y = w\qquad\mbox{cnf}(\mbox{cancellation}_1,\mbox{axiom})$

$( x + y{=}z\mbox{ and }w + y{=}z ) \ \Rightarrow \ x = w\qquad\mbox{cnf}(\mbox{cancellation}_2,\mbox{axiom})$

$\neg\,a\cdot 0{=}0\qquad\mbox{cnf}(\mbox{prove\_a\_times\_additive\_id\_is\_additive\_id},\mbox{negated\_conjecture})$

\medskip\textbf{RNG025-1.p} Middle or Flexible Law






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

$( \mbox{cy}\cdot \mbox{cx} )\cdot \mbox{cy}\ne \mbox{cy}\cdot ( \mbox{cx}\cdot \mbox{cy} )\qquad\mbox{cnf}(\mbox{prove\_middle\_law},\mbox{negated\_conjecture})$

\medskip\textbf{RNG023-7.p} Left alternative






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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{associator}(x,x,y)\ne 0\qquad\mbox{cnf}(\mbox{prove\_left\_alternative},\mbox{negated\_conjecture})$

\medskip\textbf{RNG019-7.p} First part of the linearised form of the associator

The associator can be expressed in another form called
 a linearised form. There are three clauses to be proved
 to establish the equivalence of the two forms.




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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{associator}(x,y,u + v)\ne \mbox{associator}(x,y,u) + \mbox{associator}(x,y,v)\qquad\mbox{cnf}(\mbox{prove\_linearised\_form}_1,\mbox{negated\_conjecture})$

\medskip\textbf{RNG039-1.p} Ring property 2






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

$a + ( a + b ){=}b\qquad\mbox{cnf}(\mbox{absorbtion}_1,\mbox{axiom})$

$( a + b ) + b{=}a\qquad\mbox{cnf}(\mbox{absorbtion}_2,\mbox{axiom})$

$a + a{=}0\qquad\mbox{cnf}(\mbox{clause}_{32},\mbox{axiom})$

$a + 0 = a\qquad\mbox{cnf}(\mbox{clause}_{33},\mbox{axiom})$

$a + a = 0\qquad\mbox{cnf}(\mbox{clause}_{34},\mbox{axiom})$

$a\cdot a = a\qquad\mbox{cnf}(\mbox{clause}_{35},\mbox{axiom})$

$a\cdot b = c\qquad\mbox{cnf}(\mbox{clause}_{36},\mbox{axiom})$

$b\cdot a = d\qquad\mbox{cnf}(\mbox{clause}_{37},\mbox{axiom})$

$a + b{=}b + a\qquad\mbox{cnf}(\mbox{clause}_{38},\mbox{axiom})$

$a\cdot c{=}c\qquad\mbox{cnf}(\mbox{clause}_{39},\mbox{axiom})$

$b\cdot d{=}d\qquad\mbox{cnf}(\mbox{clause}_{40},\mbox{axiom})$

$c\cdot b{=}c\qquad\mbox{cnf}(\mbox{clause}_{41},\mbox{axiom})$

$d\cdot a{=}d\qquad\mbox{cnf}(\mbox{clause}_{42},\mbox{axiom})$

$a\cdot ( a\cdot b ){=}a\cdot b\qquad\mbox{cnf}(\mbox{clause}_{43},\mbox{axiom})$

$a\cdot ( b\cdot a ){=}b\cdot a\qquad\mbox{cnf}(\mbox{clause}_{44},\mbox{axiom})$

$a\cdot b{=}c\cdot b\qquad\mbox{cnf}(\mbox{clause}_{45},\mbox{axiom})$

$a\cdot ( b\cdot c ){=}c\qquad\mbox{cnf}(\mbox{clause}_{46},\mbox{axiom})$

$b\cdot ( a\cdot a ){=}d\cdot a\qquad\mbox{cnf}(\mbox{clause}_{47},\mbox{axiom})$

$b\cdot a{=}d\cdot a\qquad\mbox{cnf}(\mbox{clause}_{48},\mbox{axiom})$

$b\cdot ( a\cdot d ){=}d\qquad\mbox{cnf}(\mbox{clause}_{49},\mbox{axiom})$

$b\cdot c{=}d\cdot b\qquad\mbox{cnf}(\mbox{clause}_{50},\mbox{axiom})$

$a\cdot d{=}c\cdot a\qquad\mbox{cnf}(\mbox{clause}_{51},\mbox{axiom})$

$( a\cdot b )\cdot b{=}a\cdot b\qquad\mbox{cnf}(\mbox{clause}_{52},\mbox{axiom})$

$( a\cdot a )\cdot b{=}a\cdot c\qquad\mbox{cnf}(\mbox{clause}_{53},\mbox{axiom})$

$a\cdot b{=}a\cdot c\qquad\mbox{cnf}(\mbox{clause}_{54},\mbox{axiom})$

$( c\cdot a )\cdot b{=}c\qquad\mbox{cnf}(\mbox{clause}_{55},\mbox{axiom})$

$d\cdot b{=}b\cdot c\qquad\mbox{cnf}(\mbox{clause}_{56},\mbox{axiom})$

$( a\cdot b )\cdot a{=}a\cdot d\qquad\mbox{cnf}(\mbox{clause}_{57},\mbox{axiom})$

$b\cdot a{=}b\cdot d\qquad\mbox{cnf}(\mbox{clause}_{58},\mbox{axiom})$

$( d\cdot b )\cdot a{=}d\qquad\mbox{cnf}(\mbox{clause}_{59},\mbox{axiom})$

$c\cdot a{=}a\cdot d\qquad\mbox{cnf}(\mbox{clause}_{60},\mbox{axiom})$

$a\cdot ( b + a ){=}c + a\qquad\mbox{cnf}(\mbox{clause}_{63},\mbox{axiom})$

$a\cdot ( a + b ){=}a + c\qquad\mbox{cnf}(\mbox{clause}_{64},\mbox{axiom})$

$b\cdot ( a + b ){=}d + b\qquad\mbox{cnf}(\mbox{clause}_{65},\mbox{axiom})$

$b\cdot ( b + a ){=}b + d\qquad\mbox{cnf}(\mbox{clause}_{66},\mbox{axiom})$

$( a + b )\cdot b{=}c + b\qquad\mbox{cnf}(\mbox{clause}_{67},\mbox{axiom})$

$( b + a )\cdot b{=}b + c\qquad\mbox{cnf}(\mbox{clause}_{68},\mbox{axiom})$

$( b + a )\cdot a{=}d + a\qquad\mbox{cnf}(\mbox{clause}_{69},\mbox{axiom})$

$( a + b )\cdot a{=}a + d\qquad\mbox{cnf}(\mbox{clause}_{70},\mbox{axiom})$

$a\cdot a{=}a\qquad\mbox{cnf}(\mbox{clause}_{71},\mbox{axiom})$

$a\cdot b{=}c\qquad\mbox{cnf}(\mbox{a\_times\_b},\mbox{negated\_conjecture})$

$b\cdot a{=}d\qquad\mbox{cnf}(\mbox{b\_times\_a},\mbox{negated\_conjecture})$

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

\medskip\textbf{RNG008-2.p} Boolean rings are commutative

Given a ring in which for all x, x * x = x, prove that for
 all x and y, x * y = y * x.




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

$( x + y{=}z\mbox{ and }x + w{=}z ) \ \Rightarrow \ y = w\qquad\mbox{cnf}(\mbox{cancellation}_1,\mbox{axiom})$

$( x + y{=}z\mbox{ and }w + y{=}z ) \ \Rightarrow \ x = w\qquad\mbox{cnf}(\mbox{cancellation}_2,\mbox{axiom})$

$x\cdot x{=}x\qquad\mbox{cnf}(\mbox{x\_squared\_is\_x},\mbox{hypothesis})$

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

$\neg\,b\cdot a{=}c\qquad\mbox{cnf}(\mbox{prove\_b\_times\_a\_is\_c},\mbox{negated\_conjecture})$

\medskip\textbf{RNG028-2.p} Left Moufang identity






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

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

$( y\cdot x )\cdot y = y\cdot ( x\cdot y )\qquad\mbox{cnf}(\mbox{middle\_law},\mbox{axiom})$

$\mbox{associator}(y,x,z) = -\mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{associator\_skew\_symmetry}_1,\mbox{axiom})$

$\mbox{associator}(z,y,x) = -\mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{associator\_skew\_symmetry}_2,\mbox{axiom})$

$( \mbox{cx}\cdot ( \mbox{cy}\cdot \mbox{cx} ) )\cdot \mbox{cz}\ne \mbox{cx}\cdot ( \mbox{cy}\cdot ( \mbox{cx}\cdot \mbox{cz} ) )\qquad\mbox{cnf}(\mbox{prove\_left\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG043-1.p} Alternative ring theory (equality) axioms






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

\medskip\textbf{RNG025-6.p} Middle or Flexible Law






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

$\mbox{associator}(x,y,x)\ne 0\qquad\mbox{cnf}(\mbox{prove\_flexible\_law},\mbox{negated\_conjecture})$

\medskip\textbf{RNG033-8.p} A fairly complex equation with associators

assr(X.Y,Z,W)+assr(X,Y,comm(Z,W)) = X.assr(Y,Z,W)+assr(X,Z,W).Y




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

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

$\mbox{associator}(x\cdot y,z,w) + \mbox{associator}(x,y,\mbox{commutator}(z,w))\ne x\cdot \mbox{associator}(y,z,w) + \mbox{associator}(x,z,w)\cdot y\qquad\mbox{cnf}(\mbox{prove\_challenge},\mbox{negated\_conjecture})$

\medskip\textbf{RNG025-8.p} Middle or Flexible Law






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

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

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

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

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{left\_multiplicative\_zero},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{right\_multiplicative\_zero},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

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

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

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

$( x\cdot x )\cdot y = x\cdot ( x\cdot y )\qquad\mbox{cnf}(\mbox{left\_alternative},\mbox{axiom})$

$\mbox{associator}(x,y,u + v) = \mbox{associator}(x,y,u) + \mbox{associator}(x,y,v)\qquad\mbox{cnf}(\mbox{linearised\_associator}_1,\mbox{axiom})$

$\mbox{associator}(x,u + v,y) = \mbox{associator}(x,u,y) + \mbox{associator}(x,v,y)\qquad\mbox{cnf}(\mbox{linearised\_associator}_2,\mbox{axiom})$

$\mbox{associator}(u + v,x,y) = \mbox{associator}(u,x,y) + \mbox{associator}(v,x,y)\qquad\mbox{cnf}(\mbox{linearised\_associator}_3,\mbox{axiom})$

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

$\mbox{associator}(a,b,c) + \mbox{associator}(a,c,b)\ne 0\qquad\mbox{cnf}(\mbox{prove\_flexible\_law},\mbox{negated\_conjecture})$

\medskip\textbf{RNG028-8.p} Left Moufang identity






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

$\mbox{associator}(x,y\cdot x,z)\ne x\cdot \mbox{associator}(x,y,z)\qquad\mbox{cnf}(\mbox{prove\_left\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG042-2.p} Ring theory (equality) axioms






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

\medskip\textbf{RNG027-1.p} Right Moufang identity






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

$\mbox{cz}\cdot ( \mbox{cx}\cdot ( \mbox{cy}\cdot \mbox{cx} ) )\ne ( ( \mbox{cz}\cdot \mbox{cx} )\cdot \mbox{cy} )\cdot \mbox{cx}\qquad\mbox{cnf}(\mbox{prove\_right\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG010-6.p} Skew symmetry of the auxilliary function

The three Moufang identities imply the skew symmetry
 of s(W,X,Y,Z) = (W*X,Y,Z) - X*(W,Y,Z) - (X,Y,Z)*W.
 Recall that skew symmetry means that the function sign
 changes when any two arguments are swapped. This problem
 proves the case for swapping the first two arguments.




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

$s(w,x,y,z) = ( \mbox{associator}(w\cdot x,y,z) + -x\cdot \mbox{associator}(w,y,z) ) + -\mbox{associator}(x,y,z)\cdot w\qquad\mbox{cnf}(\mbox{defines\_s},\mbox{axiom})$

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

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

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

$s(a,b,c,d)\ne -s(b,a,c,d)\qquad\mbox{cnf}(\mbox{prove\_skew\_symmetry},\mbox{negated\_conjecture})$

\medskip\textbf{RNG024-7.p} Right alternative






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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{associator}(x,y,y)\ne 0\qquad\mbox{cnf}(\mbox{prove\_right\_alternative},\mbox{negated\_conjecture})$

\medskip\textbf{RNG008-1.p} Boolean rings are commutative

Given a ring in which for all x, x * x = x, prove that for
 all x and y, x * y = y * x.




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

$x\cdot x{=}x\qquad\mbox{cnf}(\mbox{x\_squared\_is\_x},\mbox{hypothesis})$

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

$\neg\,b\cdot a{=}c\qquad\mbox{cnf}(\mbox{prove\_b\_times\_a\_is\_c},\mbox{negated\_conjecture})$

\medskip\textbf{RNG008-5.p} Boolean rings are commutative

Given a ring in which for all x, x * x = x, prove that for
 all x and y, x * y = y * x.




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

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

$-( -x ) + 0{=}x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$x\cdot 0{=}0\qquad\mbox{cnf}(\mbox{multiply\_additive\_id}_1,\mbox{axiom})$

$0\cdot x{=}0\qquad\mbox{cnf}(\mbox{multiply\_additive\_id}_2,\mbox{axiom})$

$-x + -y{=}-( x + y )\qquad\mbox{cnf}(\mbox{distribute\_additive\_inverse},\mbox{axiom})$

$x\cdot ( -y ){=}-x\cdot y\qquad\mbox{cnf}(\mbox{multiply\_additive\_inverse},\mbox{axiom})$

$x\cdot x{=}x\qquad\mbox{cnf}(\mbox{x\_squared\_is\_x},\mbox{hypothesis})$

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

$\neg\,b\cdot a{=}c\qquad\mbox{cnf}(\mbox{prove\_b\_times\_a\_is\_c},\mbox{negated\_conjecture})$

\medskip\textbf{RNG001-1.p} X.additive\_identity = additive\_identity for any X






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

$\neg\,a\cdot 0{=}0\qquad\mbox{cnf}(\mbox{prove\_a\_times\_0\_is}_0,\mbox{negated\_conjecture})$

\medskip\textbf{RNG017-6.p} -X*(Y+Z) = -(X*Y) + -(X*Z)






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

$( -x )\cdot ( y + z )\ne -x\cdot y + -x\cdot z\qquad\mbox{cnf}(\mbox{prove\_distributivity},\mbox{negated\_conjecture})$

\medskip\textbf{RNG031-6.p} (W*W)*X*(W*W) = additive identity






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

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

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

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

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{left\_multiplicative\_zero},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{right\_multiplicative\_zero},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

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

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

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

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

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

$( ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) )\cdot x )\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) )\ne 0\qquad\mbox{cnf}(\mbox{prove\_conjecture}_2,\mbox{negated\_conjecture})$

\medskip\textbf{RNG025-4.p} Middle or Flexible Law






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

$\mbox{associator}(x,y,z) + \mbox{associator}(x,z,y)\ne 0\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{RNG007-1.p} In Boolean rings, X is its own inverse

Given a ring in which for all x, x * x = x, prove that for
 all x, x + x = additive\_identity




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

$x\cdot x{=}x\qquad\mbox{cnf}(\mbox{x\_squared\_is\_x},\mbox{hypothesis})$

$\neg\,a + a{=}0\qquad\mbox{cnf}(\mbox{prove\_a\_plus\_a\_is\_id},\mbox{negated\_conjecture})$

\medskip\textbf{RNG031-7.p} (W*W)*X*(W*W) = additive identity






$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

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

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

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

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

$0\cdot x = 0\qquad\mbox{cnf}(\mbox{left\_multiplicative\_zero},\mbox{axiom})$

$x\cdot 0 = 0\qquad\mbox{cnf}(\mbox{right\_multiplicative\_zero},\mbox{axiom})$

$-x + x = 0\qquad\mbox{cnf}(\mbox{left\_additive\_inverse},\mbox{axiom})$

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

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

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

$-( -x ) = x\qquad\mbox{cnf}(\mbox{additive\_inverse\_additive\_inverse},\mbox{axiom})$

$( x\cdot y )\cdot y = x\cdot ( y\cdot y )\qquad\mbox{cnf}(\mbox{right\_alternative},\mbox{axiom})$

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

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

$( ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) )\cdot x )\cdot ( \mbox{associator}(x,x,y)\cdot \mbox{associator}(x,x,y) )\ne 0\qquad\mbox{cnf}(\mbox{prove\_conjecture}_2,\mbox{negated\_conjecture})$

\medskip\textbf{RNG009-5.p} If X*X*X = X then the ring is commutative

Given a ring in which for all x, x * x * x = x, prove that
 for all x and y, x * y = y * x.




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

$x + -x = 0\qquad\mbox{cnf}(\mbox{right\_additive\_inverse},\mbox{axiom})$

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

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

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

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

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

$x\cdot ( x\cdot x ) = x\qquad\mbox{cnf}(\mbox{x\_cubed\_is\_x},\mbox{hypothesis})$

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

\medskip\textbf{RNG024-6.p} Right alternative






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

$\mbox{associator}(x,y,y)\ne 0\qquad\mbox{cnf}(\mbox{prove\_right\_alternative},\mbox{negated\_conjecture})$

\medskip\textbf{RNG025-7.p} Middle or Flexible Law






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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{associator}(x,y,x)\ne 0\qquad\mbox{cnf}(\mbox{prove\_flexible\_law},\mbox{negated\_conjecture})$

\medskip\textbf{RNG014-6.p} -X*Y = -(X*Y)






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

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

\medskip\textbf{RNG037-1.p} (X* -Y) + (X*Y) = additive\_identity






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

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

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

$\neg\,c + d{=}0\qquad\mbox{cnf}(\mbox{prove\_sum\_is\_additive\_identity},\mbox{negated\_conjecture})$

\medskip\textbf{RNG001-2.p} X.additive\_identity = additive\_identity for any X






$( a{=}b\mbox{ and }c + d{=}a ) \ \Rightarrow \ c + d{=}b\qquad\mbox{cnf}(\mbox{sum\_substitution}_3,\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})$

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

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

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

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

$( x + y{=}u\mbox{ and }y + z{=}v\mbox{ and }u + z{=}w ) \ \Rightarrow \ x + v{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_addition}_1,\mbox{axiom})$

$( x + y{=}u\mbox{ and }y + z{=}v\mbox{ and }x + v{=}w ) \ \Rightarrow \ u + z{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_addition}_2,\mbox{axiom})$

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

$( x\cdot y{=}u\mbox{ and }y\cdot z{=}v\mbox{ and }u\cdot z{=}w ) \ \Rightarrow \ x\cdot v{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_multiplication}_1,\mbox{axiom})$

$( x\cdot y{=}u\mbox{ and }y\cdot z{=}v\mbox{ and }x\cdot v{=}w ) \ \Rightarrow \ u\cdot z{=}w\qquad\mbox{cnf}(\mbox{associativity\_of\_multiplication}_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{=}u\mbox{ and }x + y{=}v ) \ \Rightarrow \ u{=}v\qquad\mbox{cnf}(\mbox{addition\_is\_well\_defined},\mbox{axiom})$

$\neg\,a\cdot 0{=}0\qquad\mbox{cnf}(\mbox{theorem},\mbox{negated\_conjecture})$

\medskip\textbf{RNG029-7.p} Middle Moufang identity






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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

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

\medskip\textbf{RNG038-1.p} Ring property 1






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

$x = 0 \ \Rightarrow \ x\cdot h(x,y){=}y\qquad\mbox{cnf}(\mbox{some\_property},\mbox{hypothesis})$

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

$a\ne 0\qquad\mbox{cnf}(\mbox{a\_not\_additive\_identity},\mbox{negated\_conjecture})$

$b\ne 0\qquad\mbox{cnf}(\mbox{prove\_b\_is\_additive\_identity},\mbox{negated\_conjecture})$

\medskip\textbf{RNG020-7.p} Second part of the linearised form of the associator

The associator can be expressed in another form called
 a linearised form. There are three clauses to be proved
 to establish the equivalence of the two forms.




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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$\mbox{associator}(x,u + v,y)\ne \mbox{associator}(x,u,y) + \mbox{associator}(x,v,y)\qquad\mbox{cnf}(\mbox{prove\_linearised\_form}_2,\mbox{negated\_conjecture})$

\medskip\textbf{RNG040-1.p} Ring property 4






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

$a\cdot 1{=}a\qquad\mbox{cnf}(\mbox{right\_multiplicative\_identity},\mbox{hypothesis})$

$1\cdot a{=}a\qquad\mbox{cnf}(\mbox{left\_multiplicative\_identity},\mbox{hypothesis})$

$a\cdot h(a){=}1\mbox{ or }a = 0\qquad\mbox{cnf}(\mbox{clause}_{30},\mbox{hypothesis})$

$h(a)\cdot a{=}1\mbox{ or }a = 0\qquad\mbox{cnf}(\mbox{clause}_{31},\mbox{hypothesis})$

$a\cdot b{=}c \ \Rightarrow \ b\cdot a{=}c\qquad\mbox{cnf}(\mbox{product\_symmetry},\mbox{hypothesis})$

$b + c{=}d\qquad\mbox{cnf}(\mbox{b\_plus\_c},\mbox{negated\_conjecture})$

$d\cdot a{=}0\qquad\mbox{cnf}(\mbox{d\_plus\_a},\mbox{negated\_conjecture})$

$b\cdot a{=}l\qquad\mbox{cnf}(\mbox{b\_plus\_a},\mbox{negated\_conjecture})$

$c\cdot a{=}n\qquad\mbox{cnf}(\mbox{c\_plus\_a},\mbox{negated\_conjecture})$

$\neg\,l + n{=}0\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{RNG028-7.p} Left Moufang identity






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

$( -x )\cdot ( -y ) = x\cdot y\qquad\mbox{cnf}(\mbox{product\_of\_inverses},\mbox{axiom})$

$( -x )\cdot y = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_1,\mbox{axiom})$

$x\cdot ( -y ) = -x\cdot y\qquad\mbox{cnf}(\mbox{inverse\_product}_2,\mbox{axiom})$

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

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

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

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

$( \mbox{cx}\cdot ( \mbox{cy}\cdot \mbox{cx} ) )\cdot \mbox{cz}\ne \mbox{cx}\cdot ( \mbox{cy}\cdot ( \mbox{cx}\cdot \mbox{cz} ) )\qquad\mbox{cnf}(\mbox{prove\_left\_moufang},\mbox{negated\_conjecture})$

\medskip\textbf{RNG019-6.p} First part of the linearised form of the associator

The associator can be expressed in another form called
 a linearised form. There are three clauses to be proved
 to establish the equivalence of the two forms.




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

$\mbox{associator}(x,y,u + v)\ne \mbox{associator}(x,y,u) + \mbox{associator}(x,y,v)\qquad\mbox{cnf}(\mbox{prove\_linearised\_form}_1,\mbox{negated\_conjecture})$

\medskip\textbf{RNG029-5.p} Middle Moufang identity






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

$( \mbox{cx}\cdot \mbox{cy} )\cdot ( \mbox{cz}\cdot \mbox{cx} )\ne \mbox{cx}\cdot ( ( \mbox{cy}\cdot \mbox{cz} )\cdot \mbox{cx} )\qquad\mbox{cnf}(\mbox{prove\_middle\_law},\mbox{negated\_conjecture})$

\medskip
\end{document}