\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{LDA001-0.ax} Embedding algebra

LD-algebras are related to large cardinals. Under a very
 strong large cardinal assumption, the free-monogenic
 LD-algebra can be represented by an algebra of elementary
 embeddings. Theorems about this algebra can be proved from
 a small number of properties, suggesting the definition
 of an embedding algebra.




$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$a(x,a(y,z)) = a(f(x,y),a(x,z))\qquad\mbox{cnf}(\mbox{a1a},\mbox{axiom})$

$\mbox{critical\_point}(f(u,v)) = a(u,\mbox{critical\_point}(v))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

$\neg\,\mbox{less}(x,x)\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$\mbox{less}(x,y)\mbox{ or }\mbox{less}(y,x)\mbox{ or }x = y\qquad\mbox{cnf}(b_2,\mbox{axiom})$

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

$\mbox{less}(x,y) \ \Rightarrow \ \mbox{less}(a(u,x),a(u,y))\qquad\mbox{cnf}(b_4,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u)) \ \Rightarrow \ a(u,x) = x\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u))\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_3,\mbox{axiom})$

\medskip\textbf{LDA041-1.p} Embedding algebra






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

\medskip\textbf{LDA010-1.p} Let g = cr(t). Show that stts(sttt)(stts)g $<$ stt(sg)






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

$\mbox{st} = f(s,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{stt} = f(\mbox{st},t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{sttt} = f(\mbox{stt},t)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{stts} = f(\mbox{stt},s)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{sts} = f(\mbox{st},s)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{st\_ts} = f(\mbox{st},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$\mbox{less}(k,\mbox{sk})\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{hypothesis})$

$\neg\,\mbox{less}(f(f(f(\mbox{stts},\mbox{sttt}),\mbox{stts}),k),f(\mbox{stt},\mbox{sk}))\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA007-1.p} Let g = cr(t). Show that t(tsg) = tt(ts)(tg)






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

$\mbox{tt} = f(t,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{st} = f(s,t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{tt\_ts} = f(\mbox{tt},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{tk} = f(t,k)\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{tsk} = f(\mbox{ts},k)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{ttk} = f(\mbox{tt},k)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$f(t,\mbox{tsk})\ne f(\mbox{tt\_ts},\mbox{tk})\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA001-1.p} Verify 3*2*U = UUU, where U = 2*2






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$n_2 = f(n_1,n_1)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$n_3 = f(n_2,n_1)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$u = f(n_2,n_2)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$f(f(n_3,n_2),u)\ne f(f(u,u),u)\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA013-1.p} Let g = cr(t). Show that aag $\leq$ ag, t=a

This is the base step of an induction proof.




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

$k = \mbox{critical\_point}(\mbox{aconst})\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{aa} = f(\mbox{aconst},\mbox{aconst})\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{aak} = f(\mbox{aa},k)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{ak} = f(\mbox{aconst},k)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{less}(\mbox{ak},\mbox{aak})\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA010-2.p} Let g = cr(t). Show that stts(sttt)(stts)g $<$ stt(sg)






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$a(x,a(y,z)) = a(f(x,y),a(x,z))\qquad\mbox{cnf}(\mbox{a1a},\mbox{axiom})$

$\mbox{critical\_point}(f(u,v)) = a(u,\mbox{critical\_point}(v))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

$\neg\,\mbox{less}(x,x)\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$\mbox{less}(x,y) \ \Rightarrow \ \mbox{less}(a(u,x),a(u,y))\qquad\mbox{cnf}(b_4,\mbox{axiom})$

$x = a(u,x)\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u)) \ \Rightarrow \ a(u,x) = x\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u))\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$a(u,x) = x \ \Rightarrow \ a(f(v,u),x) = x\qquad\mbox{cnf}(d_2,\mbox{axiom})$

$\mbox{stt} = f(\mbox{st},t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{sttt} = f(\mbox{stt},t)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{stts} = f(\mbox{stt},s)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{sts} = f(\mbox{st},s)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{st\_ts} = f(\mbox{st},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$\mbox{less}(k,\mbox{sk})\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{hypothesis})$

$\neg\,\mbox{less}(f(f(f(\mbox{stts},\mbox{sttt}),\mbox{stts}),k),f(\mbox{stt},\mbox{sk}))\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA023-1.p} Identity 11 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA037-1.p} Identity 34 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA006-2.p} Let g = cr(t). Show that tsg is not in the range of t

Showing that tsg is not in the range of t is the same as
 showing that tsg $<$$>$ ta for any a.




$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$a(x,a(y,z)) = a(f(x,y),a(x,z))\qquad\mbox{cnf}(\mbox{a1a},\mbox{axiom})$

$\mbox{critical\_point}(f(u,v)) = a(u,\mbox{critical\_point}(v))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

$\neg\,\mbox{less}(x,x)\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$\mbox{less}(x,y) \ \Rightarrow \ \mbox{less}(a(u,x),a(u,y))\qquad\mbox{cnf}(b_4,\mbox{axiom})$

$x = a(u,x)\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u)) \ \Rightarrow \ a(u,x) = x\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u))\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$a(u,x) = x \ \Rightarrow \ a(f(v,u),x) = x\qquad\mbox{cnf}(d_2,\mbox{axiom})$

$\mbox{tt} = f(t,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{st} = f(s,t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{tk} = f(t,k)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$\mbox{tsk} = f(\mbox{ts},k)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{tsk} = f(t,\mbox{skolem})\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA005-2.p} Let g=cr(t). Show that tt(tsg) $<$ t(tsg) (for any s)






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$a(x,a(y,z)) = a(f(x,y),a(x,z))\qquad\mbox{cnf}(\mbox{a1a},\mbox{axiom})$

$\mbox{critical\_point}(f(u,v)) = a(u,\mbox{critical\_point}(v))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

$\neg\,\mbox{less}(x,x)\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$\mbox{less}(x,y) \ \Rightarrow \ \mbox{less}(a(u,x),a(u,y))\qquad\mbox{cnf}(b_4,\mbox{axiom})$

$x = a(u,x)\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u)) \ \Rightarrow \ a(u,x) = x\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u))\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$a(u,x) = x \ \Rightarrow \ a(f(v,u),x) = x\qquad\mbox{cnf}(d_2,\mbox{axiom})$

$\mbox{tt} = f(t,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{st} = f(s,t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{tk} = f(t,k)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$\mbox{tsk} = f(\mbox{ts},k)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\neg\,\mbox{less}(f(\mbox{tt},\mbox{tsk}),f(t,\mbox{tsk}))\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA036-1.p} Identity 33 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA006-1.p} Let g = cr(t). Show that tsg is not in the range of t

Showing that tsg is not in the range of t is the same as
 showing that tsg $<$$>$ ta for any a.




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

$\mbox{tt} = f(t,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{st} = f(s,t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{tk} = f(t,k)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$\mbox{tsk} = f(\mbox{ts},k)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{tsk} = f(t,\mbox{skolem})\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA012-2.p} Let g = cr(t). Show that stts(sttt)g = g






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$a(x,a(y,z)) = a(f(x,y),a(x,z))\qquad\mbox{cnf}(\mbox{a1a},\mbox{axiom})$

$\mbox{critical\_point}(f(u,v)) = a(u,\mbox{critical\_point}(v))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

$\neg\,\mbox{less}(x,x)\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$\mbox{less}(x,y) \ \Rightarrow \ \mbox{less}(a(u,x),a(u,y))\qquad\mbox{cnf}(b_4,\mbox{axiom})$

$x = a(u,x)\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u)) \ \Rightarrow \ a(u,x) = x\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u))\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$a(u,x) = x \ \Rightarrow \ a(f(v,u),x) = x\qquad\mbox{cnf}(d_2,\mbox{axiom})$

$\mbox{stt} = f(\mbox{st},t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{sttt} = f(\mbox{stt},t)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{stts} = f(\mbox{stt},s)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{sts} = f(\mbox{st},s)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{st\_ts} = f(\mbox{st},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$\mbox{less}(k,\mbox{sk})\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{hypothesis})$

$f(f(\mbox{stts},\mbox{sttt}),k)\ne k\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA040-1.p} Identity yy in the equational theory of group conjugation






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

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

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

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

\medskip\textbf{LDA026-1.p} Identity 14 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA011-2.p} Let g = cr(t). Show that stts(sttt)(stts)stts(sttt)g $<$ stt(sg)






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$a(x,a(y,z)) = a(f(x,y),a(x,z))\qquad\mbox{cnf}(\mbox{a1a},\mbox{axiom})$

$\mbox{critical\_point}(f(u,v)) = a(u,\mbox{critical\_point}(v))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

$\neg\,\mbox{less}(x,x)\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$\mbox{less}(x,y) \ \Rightarrow \ \mbox{less}(a(u,x),a(u,y))\qquad\mbox{cnf}(b_4,\mbox{axiom})$

$x = a(u,x)\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u)) \ \Rightarrow \ a(u,x) = x\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u))\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$a(u,x) = x \ \Rightarrow \ a(f(v,u),x) = x\qquad\mbox{cnf}(d_2,\mbox{axiom})$

$\mbox{stt} = f(\mbox{st},t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{sttt} = f(\mbox{stt},t)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{stts} = f(\mbox{stt},s)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{sts} = f(\mbox{st},s)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{st\_ts} = f(\mbox{st},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$\mbox{less}(k,\mbox{sk})\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{hypothesis})$

$\neg\,\mbox{less}(f(f(f(\mbox{stts},\mbox{sttt}),\mbox{stts}),f(f(\mbox{stts},\mbox{sttt}),k)),f(\mbox{stt},\mbox{sk}))\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA009-2.p} Let g = cr(t). If g $<$ sg, then st(ts)g $<$ stt(sg)






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$a(x,a(y,z)) = a(f(x,y),a(x,z))\qquad\mbox{cnf}(\mbox{a1a},\mbox{axiom})$

$\mbox{critical\_point}(f(u,v)) = a(u,\mbox{critical\_point}(v))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

$\neg\,\mbox{less}(x,x)\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$\mbox{less}(x,y) \ \Rightarrow \ \mbox{less}(a(u,x),a(u,y))\qquad\mbox{cnf}(b_4,\mbox{axiom})$

$x = a(u,x)\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u)) \ \Rightarrow \ a(u,x) = x\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u))\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$a(u,x) = x \ \Rightarrow \ a(f(v,u),x) = x\qquad\mbox{cnf}(d_2,\mbox{axiom})$

$\mbox{stt} = f(\mbox{st},t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{sttt} = f(\mbox{stt},t)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{stts} = f(\mbox{stt},s)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{sts} = f(\mbox{st},s)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{st\_ts} = f(\mbox{st},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$\mbox{less}(k,\mbox{sk})\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{hypothesis})$

$\neg\,\mbox{less}(f(\mbox{st\_ts},k),f(\mbox{stt},\mbox{sk}))\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA016-1.p} Identity 01 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA017-1.p} Identity 03 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA034-1.p} Identity 30 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA008-1.p} Let g = cr(t) = cr(T). If Ta $<$ Tsg, then ta $<$ tsg






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

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{bts} = f(\mbox{bt},s)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{ta} = f(t,\mbox{aconst})\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{bta} = f(\mbox{bt},\mbox{aconst})\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{critical\_point}(\mbox{bt}) = k\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{tsk} = f(\mbox{ts},k)\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$\mbox{btsk} = f(\mbox{bts},k)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{less}(\mbox{bta},\mbox{btsk})\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\neg\,\mbox{less}(\mbox{ta},\mbox{tsk})\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA007-2.p} Let g = cr(t). Show that t(tsg) = tt(ts)(tg)






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$a(x,a(y,z)) = a(f(x,y),a(x,z))\qquad\mbox{cnf}(\mbox{a1a},\mbox{axiom})$

$\mbox{critical\_point}(f(u,v)) = a(u,\mbox{critical\_point}(v))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

$\neg\,\mbox{less}(x,x)\qquad\mbox{cnf}(b_1,\mbox{axiom})$

$\mbox{less}(x,y) \ \Rightarrow \ \mbox{less}(a(u,x),a(u,y))\qquad\mbox{cnf}(b_4,\mbox{axiom})$

$x = a(u,x)\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u)) \ \Rightarrow \ a(u,x) = x\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u))\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$a(u,x) = x \ \Rightarrow \ a(f(v,u),x) = x\qquad\mbox{cnf}(d_2,\mbox{axiom})$

$\mbox{tt} = f(t,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{st} = f(s,t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{tt\_ts} = f(\mbox{tt},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{tk} = f(t,k)\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{tsk} = f(\mbox{ts},k)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{ttk} = f(\mbox{tt},k)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$f(t,\mbox{tsk})\ne f(\mbox{tt\_ts},\mbox{tk})\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA022-1.p} Identity 10 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA021-1.p} Identity 08 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA027-1.p} Identity 17 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA020-1.p} Identity 07 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA018-1.p} Identity 04 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA038-1.p} Identity 35 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA005-1.p} Let g=cr(t). Show that tt(tsg) $<$ t(tsg) (for any s)






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

$\mbox{tt} = f(t,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{st} = f(s,t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{tk} = f(t,k)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$\mbox{tsk} = f(\mbox{ts},k)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\neg\,\mbox{less}(f(\mbox{tt},\mbox{tsk}),f(t,\mbox{tsk}))\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA035-1.p} Identity 32 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA007-3.p} Let g = cr(t). Show that t(tsg) = tt(ts)(tg)






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$\mbox{tt} = f(t,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{tt\_ts} = f(\mbox{tt},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{tk} = f(t,k)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{tsk} = f(\mbox{ts},k)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$f(t,\mbox{tsk})\ne f(\mbox{tt\_ts},\mbox{tk})\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA031-1.p} Identity 25 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA002-1.p} Verify 3*2(U2)(UU(UU)) = U1(U3)(UU(UU))






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$n_2 = f(n_1,n_1)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$n_3 = f(n_2,n_1)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$u = f(n_2,n_2)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$u_1 = f(u,n_1)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$u_2 = f(u,n_2)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$u_3 = f(u,n_3)\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$\mbox{uu} = f(u,u)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$a = f(f(n_3,n_2),u_2)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$b = f(u_1,u_3)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$v = f(\mbox{uu},\mbox{uu})\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{axiom})$

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

\medskip\textbf{LDA024-1.p} Identity 12 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA033-1.p} Identity 29 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA004-1.p} Show that 3*2(U2) is a left segment of U1(U3)






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$\mbox{left}(x,f(x,y))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

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

$n_2 = f(n_1,n_1)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$n_3 = f(n_2,n_1)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$u = f(n_2,n_2)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$u_1 = f(u,n_1)\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$u_2 = f(u,n_2)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$u_3 = f(u,n_3)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$a = f(f(n_3,n_2),u_2)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$b = f(u_1,u_3)\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{axiom})$

$\neg\,\mbox{left}(a,b)\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA039-1.p} Identity xx in the equational theory of group conjugation






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

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

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

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

\medskip\textbf{LDA015-1.p} Identity 00 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA025-1.p} Identity 13 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA009-1.p} Let g = cr(t). If g $<$ sg, then st(ts)g $<$ stt(sg)






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

$\mbox{st} = f(s,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{stt} = f(\mbox{st},t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{sttt} = f(\mbox{stt},t)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{stts} = f(\mbox{stt},s)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{sts} = f(\mbox{st},s)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{st\_ts} = f(\mbox{st},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$\mbox{less}(k,\mbox{sk})\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{hypothesis})$

$\neg\,\mbox{less}(f(\mbox{st\_ts},k),f(\mbox{stt},\mbox{sk}))\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA019-1.p} Identity 06 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA030-1.p} Identity 24 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA014-1.p} Let g = cr(t). Show that aag $\leq$ ag, t=a

This is the induction step of an induction proof.




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

$k = \mbox{critical\_point}(\mbox{aconst})\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{aa} = f(\mbox{aconst},\mbox{aconst})\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{aak} = f(\mbox{aa},k)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{ak} = f(\mbox{aconst},k)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{crit\_u} = \mbox{critical\_point}(u)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{aacrit\_u} = f(\mbox{aa},\mbox{crit\_u})\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{acrit\_u} = f(\mbox{aconst},\mbox{crit\_u})\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$\mbox{crit\_v} = \mbox{critical\_point}(v)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{aacrit\_v} = f(\mbox{aa},\mbox{crit\_v})\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{acrit\_v} = f(\mbox{aconst},\mbox{crit\_v})\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$\mbox{uv} = f(u,v)\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{axiom})$

$\mbox{crit\_uv} = \mbox{critical\_point}(\mbox{uv})\qquad\mbox{cnf}(\mbox{clause}_{12},\mbox{axiom})$

$\mbox{aacrit\_uv} = f(\mbox{aa},\mbox{crit\_uv})\qquad\mbox{cnf}(\mbox{clause}_{13},\mbox{axiom})$

$\mbox{acrit\_uv} = f(\mbox{aconst},\mbox{crit\_uv})\qquad\mbox{cnf}(\mbox{clause}_{14},\mbox{axiom})$

$\neg\,\mbox{less}(\mbox{acrit\_u},\mbox{aacrit\_u})\qquad\mbox{cnf}(\mbox{true\_for\_u},\mbox{hypothesis})$

$\neg\,\mbox{less}(\mbox{acrit\_v},\mbox{aacrit\_v})\qquad\mbox{cnf}(\mbox{true\_for\_v},\mbox{hypothesis})$

$\mbox{less}(\mbox{acrit\_uv},\mbox{aacrit\_uv})\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA028-1.p} Identity 19 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA012-1.p} Let g = cr(t). Show that stts(sttt)g = g






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

$\mbox{st} = f(s,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{stt} = f(\mbox{st},t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{sttt} = f(\mbox{stt},t)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{stts} = f(\mbox{stt},s)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{sts} = f(\mbox{st},s)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{st\_ts} = f(\mbox{st},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$\mbox{less}(k,\mbox{sk})\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{hypothesis})$

$f(f(\mbox{stts},\mbox{sttt}),k)\ne k\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA029-1.p} Identity 21 in the equational theory of group conjugation






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

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

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

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

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

\medskip\textbf{LDA008-2.p} Let g = cr(t) = cr(T). If Ta $<$ Tsg, then ta $<$ tsg






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$a(x,a(y,z)) = a(f(x,y),a(x,z))\qquad\mbox{cnf}(\mbox{a1a},\mbox{axiom})$

$\mbox{critical\_point}(f(u,v)) = a(u,\mbox{critical\_point}(v))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

$\neg\,\mbox{less}(x,x)\qquad\mbox{cnf}(b_1,\mbox{axiom})$

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

$\mbox{less}(x,y) \ \Rightarrow \ \mbox{less}(a(u,x),a(u,y))\qquad\mbox{cnf}(b_4,\mbox{axiom})$

$x = a(u,x)\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_1,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u)) \ \Rightarrow \ a(u,x) = x\qquad\mbox{cnf}(c_2,\mbox{axiom})$

$\mbox{less}(x,\mbox{critical\_point}(u))\mbox{ or }\mbox{less}(x,a(u,x))\qquad\mbox{cnf}(c_3,\mbox{axiom})$

$a(u,x) = x \ \Rightarrow \ a(f(v,u),x) = x\qquad\mbox{cnf}(d_2,\mbox{axiom})$

$\mbox{bts} = f(\mbox{bt},s)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{ta} = f(t,\mbox{aconst})\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{bta} = f(\mbox{bt},\mbox{aconst})\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{critical\_point}(\mbox{bt}) = k\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{tsk} = f(\mbox{ts},k)\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$\mbox{btsk} = f(\mbox{bts},k)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{less}(\mbox{bta},\mbox{btsk})\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\neg\,\mbox{less}(\mbox{ta},\mbox{tsk})\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA011-1.p} Let g = cr(t). Show that stts(sttt)(stts)stts(sttt)g $<$ stt(sg)






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

$\mbox{st} = f(s,t)\qquad\mbox{cnf}(\mbox{clause}_1,\mbox{axiom})$

$\mbox{stt} = f(\mbox{st},t)\qquad\mbox{cnf}(\mbox{clause}_2,\mbox{axiom})$

$\mbox{sttt} = f(\mbox{stt},t)\qquad\mbox{cnf}(\mbox{clause}_3,\mbox{axiom})$

$\mbox{stts} = f(\mbox{stt},s)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$\mbox{ts} = f(t,s)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$\mbox{sts} = f(\mbox{st},s)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\mbox{st\_ts} = f(\mbox{st},\mbox{ts})\qquad\mbox{cnf}(\mbox{clause}_7,\mbox{axiom})$

$k = \mbox{critical\_point}(t)\qquad\mbox{cnf}(\mbox{clause}_8,\mbox{axiom})$

$\mbox{sk} = f(s,k)\qquad\mbox{cnf}(\mbox{clause}_9,\mbox{axiom})$

$\mbox{stk} = f(\mbox{st},k)\qquad\mbox{cnf}(\mbox{clause}_{10},\mbox{axiom})$

$\mbox{less}(k,\mbox{sk})\qquad\mbox{cnf}(\mbox{clause}_{11},\mbox{hypothesis})$

$\neg\,\mbox{less}(f(f(f(\mbox{stts},\mbox{sttt}),\mbox{stts}),f(f(\mbox{stts},\mbox{sttt}),k)),f(\mbox{stt},\mbox{sk}))\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA003-1.p} Show that 3 is a left segment of U = 2*2






$f(x,f(y,z)) = f(f(x,y),f(x,z))\qquad\mbox{cnf}(a_1,\mbox{axiom})$

$\mbox{left}(x,f(x,y))\qquad\mbox{cnf}(a_2,\mbox{axiom})$

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

$n_2 = f(n_1,n_1)\qquad\mbox{cnf}(\mbox{clause}_4,\mbox{axiom})$

$n_3 = f(n_2,n_1)\qquad\mbox{cnf}(\mbox{clause}_5,\mbox{axiom})$

$u = f(n_2,n_2)\qquad\mbox{cnf}(\mbox{clause}_6,\mbox{axiom})$

$\neg\,\mbox{left}(n_3,u)\qquad\mbox{cnf}(\mbox{prove\_equation},\mbox{negated\_conjecture})$

\medskip\textbf{LDA032-1.p} Identity 26 in the equational theory of group conjugation






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

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

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

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

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

\medskip
\end{document}