proof.tex

\documentclass[a4]{article}

% ILF_STYLE 1.4 (03/25/97)
  \newlength{\ilfformulalength}\setlength{\ilfformulalength}{\textwidth}
  \addtolength{\ilfformulalength}{-7em}
  \ifx\mathindent\undefined
    \newcommand{\ilftformel}[1]{\begin{equation}%
\parbox{\ilfformulalength}{\centering #1}\end{equation}}
  \else
    \addtolength{\ilfformulalength}{-\mathindent}
    \newcommand{\ilftformel}[1]{\begin{equation}%
\parbox{\ilfformulalength}{#1}\end{equation}}
\fi
  \newcommand{\ilfformula}[1]{\ilftformel{$ #1 $}}
  \newenvironment{ilfproof}[1]{%
Proof\/\footnote{#1}.}{\begin{quote}\raggedleft q.e.d.\end{quote}}
  \newenvironment{ilf_cases}{%
\renewcommand{\labelenumi}{Case \arabic{enumi}.}\begin{enumerate}}%
{\end{enumerate}}
  \newcommand{\ilfUpCase}[1]{\ifmmode#1\else\uppercase{#1}\fi}
  \newcommand{\ilftext}[1]{\ifmmode$#1$\else#1\fi}
  \newcounter{ilflistdepth}\setcounter{ilflistdepth}{0}
  \newcounter{ilflistolddepth}
  \newcounter{ilflistmaxdepth}\setcounter{ilflistmaxdepth}{0}
  \newlength{\ilflistmargin}\settowidth{\ilflistmargin}{1.\ }
  \newcommand\ilflistempty{}
  \newcommand\ilflistconstlabel{}
  \def\ilflistlabeli{}
  \def\ilflistsetlabel#1#2{\ifnum#2=0\else
\ilflistsetlabelA{\romannumeral#1}{\romannumeral#2}\fi}
  \def\ilflistsetlabelA#1#2{\expandafter\xdef\csname ilflistlabel#1\endcsname{%
\csname ilflistlabel#2\endcsname\arabic{ilflist#2}.\ }}
  \def\ilflistlabel#1{\ilflistconstlabel%
\csname ilflistlabel#1\endcsname\arabic{ilflist#1}.\ }
\expandafter\def\csname p@ilflisti\endcsname{}
  \def\ilflistsetpa#1#2{\ifnum#2=0\else
\ilflistsetpaA{\romannumeral#1}{\romannumeral#2}\fi}
  \def\ilflistsetpaA#1#2{\expandafter\xdef\csname p@ilflist#1\endcsname{%
\csname p@ilflist#2\endcsname\arabic{ilflist#2}.}}
  \newenvironment{ilflist}[1]{\par\vspace{\topsep}\parskip\parsep%
\advance\leftskip by \ilflistmargin%
\ifnum\theilflistdepth=0\advance\leftskip by \ilflistmargin\fi%
\renewcommand\ilflistconstlabel{#1}
\ifx\ilflistconstlabel\ilflistempty\else\renewcommand\ilflistconstlabel{#1\ }\fi
\setcounter{ilflistolddepth}{\theilflistdepth}
\addtocounter{ilflistdepth}{1}%
\ifnum\theilflistdepth >\theilflistmaxdepth\relax%
\newcounter{ilflist\romannumeral\theilflistdepth}%
\setcounter{ilflistmaxdepth}{\theilflistdepth}\fi%
\setcounter{ilflist\romannumeral\theilflistdepth}{0}%
\ilflistsetpa{\theilflistdepth}{\theilflistolddepth}%
\ilflistsetlabel{\theilflistdepth}{\theilflistolddepth}}%
{\par\vspace{\topsep}%
\addtocounter{ilflistdepth}{-1}\advance\leftskip by -\ilflistmargin%
\ifnum\theilflistdepth=0\advance\leftskip by -\ilflistmargin\fi}
  \newcommand{\ilfitem}{\par\vspace{\itemsep}%
\hspace*{-\ilflistmargin}\hspace*{-\parindent}%
\refstepcounter{ilflist\romannumeral\theilflistdepth}%
\ilflistlabel{\romannumeral\theilflistdepth}\ignorespaces}
  \newtheorem{axiom}{Axiom}[section]
  \newtheorem{sysinfo}{System Information}
  \newtheorem{conjecture}{Conjecture}[section]
  \newtheorem{theorem}{Theorem}[section]
  \newtheorem{lemma}{Lemma}[section]
% END ILF_STYLE

\begin{document}

\title{Joao's Proof\thanks{\fussy This manuscript was generated by ILF.
The development of ILF was supported by the Deutsche Forschungsgemeinschaft.
For information on ILF contact
ilf--serv--request@ma\-the\-ma\-tik.hu-ber\-lin.de.}}
\author{Prover 9 and ILF}
\maketitle

\expandafter\ifx\csname Axiom\endcsname\relax%
\newtheorem{Axiom}{Axiom}[section]\fi
\begin{Axiom}[{$ $3-index free$ $}]
$ X_{1} \cdot  X_{1} \cdot  (X_{1} \cdot  X_{1}) = X_{1} -> X_{1} \cdot  X_{1} = X_{1} $.
\end{Axiom}
\begin{Axiom}[{$ $\ilfUpCase{a}ssociativity$ $}]
$ X_{1} \cdot  X_{2} \cdot  X_{3} = X_{1} \cdot  (X_{2} \cdot  X_{3}) $.
\end{Axiom}
\begin{Axiom}[{$ $\ilfUpCase{r}ight identitity$ $}]
$ X_{1} \cdot  0 = X_{1} $.
\end{Axiom}
\begin{Axiom}[{$ $\ilfUpCase{r}ight inverse$ $}]
$ X_{1} \cdot  X_{1} ^{\prime}  = 0 $.
\end{Axiom}
\begin{Axiom}[{$ $\ilfUpCase{l}eft inverse$ $}]
$ X_{1} ^{\prime}  \cdot  X_{1} = 0 $.
\end{Axiom}
\begin{Axiom}[{$ $\ilfUpCase{l}eft identity$ $}]
$ 0 \cdot  X_{1} = X_{1} $.
\end{Axiom}
\begin{Axiom}[{$ $\ilfUpCase{i}nvolution$ $}]
$ X_{1} ^{\prime}  ^{\prime}  = X_{1} $.
\end{Axiom}
\begin{Axiom}[{$ $\ilfUpCase{a}nti-morphism$ $}]
$ (X_{1} \cdot  X_{2}) ^{\prime}  = X_{2} ^{\prime}  \cdot  X_{1} ^{\prime}  $.
\end{Axiom}
\begin{Axiom}[{$ $2-commutativity$ $}]
$ X_{1} \cdot  X_{2} \cdot  (X_{1} \cdot  X_{2}) = X_{2} \cdot  X_{2} \cdot  (X_{1} \cdot  X_{1}) $.
\end{Axiom}
\begin{Axiom}[{$ $\ilfUpCase{c}ubes commute$ $}]
$ X_{1} \cdot  X_{1} \cdot  X_{1} \cdot  X_{2} = X_{2} \cdot  (X_{1} \cdot  X_{1} \cdot  X_{1}) $.
\end{Axiom}
\expandafter\ifx\csname Lemma\endcsname\relax%
\newtheorem{Lemma}{Lemma}[section]\fi
\begin{Lemma}\label{[sub(1, 1), 15]}
$ X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  X_{2})) = X_{2} \cdot  (X_{2} \cdot  (X_{1} \cdot  X_{1})) $.
\end{Lemma}

\begin{ilfproof}{$ ilf $} Because of $ $associativity$ $ and by $ $2-commutativity$ $ $ X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  X_{2})) = X_{2} \cdot  (X_{2} \cdot  (X_{1} \cdot  X_{1})). $


\end{ilfproof}
\begin{Lemma}\label{[sub(1, 1), 21]}
$ X_{1} \cdot  (X_{1} ^{\prime}  \cdot  X_{2}) = X_{2} $.
\end{Lemma}

\begin{ilfproof}{$ ilf $} We  show directly that $ X_{1} \cdot  (X_{1} ^{\prime}  \cdot  X_{2}) = X_{2}. $
Because of $ $associativity$ $,  $ $left identity$ $, and by $ $right inverse$ $ $ X_{1} \cdot  (X_{1} ^{\prime}  \cdot  X_{2}) = X_{2}. $
Thus we have completed the proof of Lemma \ref{[sub(1, 1), 21]}.



\end{ilfproof}
\begin{Lemma}\label{[sub(1, 1), 22]}
$ X_{1} ^{\prime}  \cdot  (X_{1} \cdot  X_{2}) = X_{2} $.
\end{Lemma}

\begin{ilfproof}{$ ilf $} We  show directly that $ X_{1} ^{\prime}  \cdot  (X_{1} \cdot  X_{2}) = X_{2}. $
Because of $ $associativity$ $,  $ $left identity$ $, and by $ $left inverse$ $ $ X_{1} ^{\prime}  \cdot  (X_{1} \cdot  X_{2}) = X_{2}. $
Thus we have completed the proof of Lemma \ref{[sub(1, 1), 22]}.



\end{ilfproof}
\begin{Lemma}\label{[sub(1, 1), 24]}
$ X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{2} \cdot  X_{3}))) = X_{2} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{1} \cdot  X_{3}))) $.
\end{Lemma}

\begin{ilfproof}{$ ilf $} By $ $associativity$ $ and by Lemma \ref{[sub(1, 1), 15]} $ X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{2} \cdot  X_{3}))) = X_{2} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{1} \cdot  X_{3}))). $


\end{ilfproof}
\begin{Lemma}\label{[sub(1, 1), 27]}
$ X_{1} \cdot  (X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  X_{1} ^{\prime} ))) = X_{2} \cdot  (X_{1} \cdot  X_{2}) $.
\end{Lemma}

\begin{ilfproof}{$ ilf $} Hence by $ $right identitity$ $ and by $ $right inverse$ $ $ X_{1} \cdot  (X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  X_{1} ^{\prime} ))) = X_{2} \cdot  (X_{1} \cdot  X_{2}). $


\end{ilfproof}
\begin{Lemma}\label{[sub(1, 1), 33]}
$ X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{1} \cdot  X_{2})) = X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  X_{1} ^{\prime} )) $.
\end{Lemma}

\begin{ilfproof}{$ ilf $} Hence by Lemma \ref{[sub(1, 1), 22]} $ X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{1} \cdot  X_{2})) = X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  X_{1} ^{\prime} )). $


\end{ilfproof}
\begin{Lemma}\label{[sub(1, 1), 34]}
$ X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{2} \cdot  X_{3}))) = X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  (X_{1} ^{\prime}  \cdot  X_{3}))) $.
\end{Lemma}

\begin{ilfproof}{$ ilf $} Hence by $ $associativity$ $ $ X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{2} \cdot  X_{3}))) = X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  (X_{1} ^{\prime}  \cdot  X_{3}))). $


\end{ilfproof}
\begin{Lemma}\label{[sub(1, 1), 36]}
$ X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  (X_{1} ^{\prime}  \cdot  X_{2} ^{\prime} ))) = X_{1} ^{\prime}  \cdot  (X_{2} \cdot  X_{1}) $.
\end{Lemma}

\begin{ilfproof}{$ ilf $} Hence by $ $right identitity$ $ and by $ $right inverse$ $ $ X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  (X_{1} ^{\prime}  \cdot  X_{2} ^{\prime} ))) = X_{1} ^{\prime}  \cdot  (X_{2} \cdot  X_{1}). $


\end{ilfproof}
\begin{Lemma}\label{[sub(1, 1), 37]}
$ X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{1} \cdot  X_{2} ^{\prime} ))) = X_{2} ^{\prime}  \cdot  (X_{1} \cdot  X_{2}) $.
\end{Lemma}

\begin{ilfproof}{$ ilf $} We  show directly that $ X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{1} \cdot  X_{2} ^{\prime} ))) = X_{2} ^{\prime}  \cdot  (X_{1} \cdot  X_{2}). $
By $ $associativity$ $, $ $right identitity$ $, $ $right inverse$ $, $ $involution$ $, $ $anti-morphism$ $,  Lemma \ref{[sub(1, 1), 21]}, and by Lemma \ref{[sub(1, 1), 36]} $ X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{1} \cdot  X_{2} ^{\prime} ))) = X_{2} ^{\prime}  \cdot  (X_{1} \cdot  X_{2}). $
Thus we have completed the proof of Lemma \ref{[sub(1, 1), 37]}.



\end{ilfproof}
\expandafter\ifx\csname Theorem\endcsname\relax%
\newtheorem{Theorem}{Theorem}[section]\fi
\begin{Theorem}\label{[sub(1, 1), theorem]}
$ $\ilfUpCase{f}or all $X_{1}$, X_{2}$ $X_{2} \cdot  X_{1} = X_{1} \cdot  X_{2} $.
\end{Theorem}

\begin{ilfproof}{$ otter $ and $ ilf $} We  show directly that 
\ilfformula{\label{[sub(1, 1), 53]}
X_{1} \cdot  X_{2} = X_{2} \cdot  X_{1}.
}

Because of $ $associativity$ $ and by $ $cubes commute$ $ $ X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  X_{2})) = X_{2} \cdot  (X_{2} \cdot  (X_{2} \cdot  X_{1})). $
Hence by Lemma \ref{[sub(1, 1), 21]} $ X_{1} \cdot  (X_{2} \cdot  (X_{1} ^{\prime}  \cdot  (X_{1} ^{\prime}  \cdot  X_{1} ^{\prime} ))) = X_{1} ^{\prime}  \cdot  (X_{1} ^{\prime}  \cdot  X_{2}). $
Now by $ $associativity$ $ and by Lemma \ref{[sub(1, 1), 21]} $ X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{1} \cdot  X_{1}))) = X_{1} \cdot  (X_{1} \cdot  X_{2}). $
Therefore by $ $associativity$ $, $ $involution$ $,  Lemma \ref{[sub(1, 1), 21]}, and by Lemma \ref{[sub(1, 1), 37]} 
\ilfformula{\label{[hdl4, hdl21]}
X_{1} ^{\prime}  \cdot  (X_{2} ^{\prime}  \cdot  (X_{1} \cdot  X_{2})) = X_{1} \cdot  (X_{2} \cdot  (X_{1} ^{\prime}  \cdot  X_{2} ^{\prime} )).
}

By $ $involution$ $,  Lemma \ref{[sub(1, 1), 21]}, and by Lemma \ref{[sub(1, 1), 27]} $ X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{2} \cdot  X_{1})) = X_{1} \cdot  (X_{2} \cdot  (X_{1} ^{\prime}  \cdot  X_{2})). $
Hence by $ $involution$ $ and by Lemma \ref{[sub(1, 1), 37]} 
\ilfformula{\label{[hdl4, hdl19]}
X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{2} ^{\prime}  \cdot  X_{1}))) = X_{2} \cdot  (X_{1} \cdot  X_{2} ^{\prime} ).
}

By Lemma \ref{[sub(1, 1), 21]} and by Lemma \ref{[sub(1, 1), 24]} 
\ilfformula{\label{[hdl4, hdl18]}
X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{2} \cdot  (X_{1} ^{\prime}  \cdot  X_{3})))) = X_{2} \cdot  (X_{2} \cdot  (X_{1} \cdot  X_{3})).
}

Because of $ $associativity$ $ and by $ $3-index free$ $ $ X_{1} \cdot  (X_{1} \cdot  (X_{1} \cdot  X_{1})) = X_{1} \rightarrow X_{1} \cdot  X_{1} = X_{1}. $
Hence by $ $associativity$ $ and by Lemma \ref{[sub(1, 1), 24]} $ X_{1} \cdot  (X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{1} \cdot  (X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{1} \cdot  (X_{1} \cdot  (X_{2} \cdot  X_{2})))))))))) = X_{1} \cdot  (X_{1} \cdot  X_{2}) \rightarrow X_{1} \cdot  (X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{1} \cdot  X_{2})))) = X_{1} \cdot  (X_{1} \cdot  X_{2}). $
Hence by (\ref{[hdl4, hdl18]}), (\ref{[hdl4, hdl19]}), (\ref{[hdl4, hdl21]}), $ $associativity$ $, $ $right identitity$ $, $ $left inverse$ $, Lemma \ref{[sub(1, 1), 21]}, Lemma \ref{[sub(1, 1), 22]},  Lemma \ref{[sub(1, 1), 34]}, and by Lemma \ref{[sub(1, 1), 37]} 
\ilfformula{\label{[hdl4, hdl15]}
X_{1} ^{\prime}  \cdot  (X_{2} \cdot  (X_{1} \cdot  X_{2} ^{\prime} )) = X_{1} \cdot  (X_{2} \cdot  (X_{1} ^{\prime}  \cdot  X_{2} ^{\prime} )).
}

By $ $involution$ $, Lemma \ref{[sub(1, 1), 22]}, Lemma \ref{[sub(1, 1), 33]},  Lemma \ref{[sub(1, 1), 34]}, and by Lemma \ref{[sub(1, 1), 37]} $ X_{1} \cdot  (X_{2} ^{\prime}  \cdot  (X_{1} \cdot  (X_{2} \cdot  X_{1} ^{\prime} ))) = X_{2} ^{\prime}  \cdot  (X_{1} \cdot  X_{2}). $
By (\ref{[hdl4, hdl21]}), $ $associativity$ $, $ $involution$ $, $ $anti-morphism$ $, Lemma \ref{[sub(1, 1), 21]}, Lemma \ref{[sub(1, 1), 22]}, Lemma \ref{[sub(1, 1), 27]},  Lemma \ref{[sub(1, 1), 33]}, and by Lemma \ref{[sub(1, 1), 37]} 
\ilfformula{\label{[hdl4, hdl13]}
X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{2} ^{\prime}  \cdot  X_{1} ^{\prime} ))) = X_{2} \cdot  (X_{1} \cdot  X_{2} ^{\prime} ).
}

Therefore by (\ref{[hdl4, hdl15]}) 
\ilfformula{\label{[hdl4, hdl12]}
X_{1} ^{\prime}  \cdot  (X_{2} \cdot  X_{1}) = X_{1} \cdot  (X_{2} \cdot  X_{1} ^{\prime} ).
}

By $ $right identitity$ $,  $ $right inverse$ $, and by Lemma \ref{[sub(1, 1), 24]} $ X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{2} \cdot  X_{1} ^{\prime} ))) = X_{2} \cdot  (X_{2} \cdot  X_{1}). $
Hence by (\ref{[hdl4, hdl13]}), (\ref{[hdl4, hdl18]}),  $ $involution$ $, and by Lemma \ref{[sub(1, 1), 21]} $ X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  X_{1})) = X_{2} \cdot  (X_{1} \cdot  (X_{1} \cdot  X_{2})). $
Hence by (\ref{[hdl4, hdl18]}), $ $associativity$ $, $ $right identitity$ $, $ $left inverse$ $, Lemma \ref{[sub(1, 1), 21]},  Lemma \ref{[sub(1, 1), 22]}, and by Lemma \ref{[sub(1, 1), 36]} $ X_{1} \cdot  (X_{2} \cdot  (X_{1} ^{\prime}  \cdot  (X_{1} ^{\prime}  \cdot  (X_{2} \cdot  X_{1})))) = X_{2} \cdot  X_{2}. $
Hence by (\ref{[hdl4, hdl12]}) and by Lemma \ref{[sub(1, 1), 22]} $ X_{1} \cdot  (X_{2} \cdot  (X_{2} \cdot  X_{1} ^{\prime} )) = X_{2} \cdot  X_{2}. $
Hence by (\ref{[hdl4, hdl12]}),  Lemma \ref{[sub(1, 1), 22]}, and by Lemma \ref{[sub(1, 1), 37]} 
\ilfformula{\label{[hdl4, hdl7]}
X_{1} \cdot  (X_{2} \cdot  X_{1} ^{\prime} ) = X_{2}.
}

By (\ref{[hdl4, hdl18]}), $ $involution$ $,  Lemma \ref{[sub(1, 1), 21]}, and by Lemma \ref{[sub(1, 1), 36]} $ X_{1} \cdot  (X_{2} \cdot  (X_{1} \cdot  (X_{2} ^{\prime}  \cdot  (X_{1} ^{\prime}  \cdot  X_{2})))) = X_{2} \cdot  X_{1}. $
Hence by (\ref{[hdl4, hdl12]}) and by (\ref{[hdl4, hdl13]}) $ X_{1} \cdot  (X_{1} \cdot  (X_{2} \cdot  X_{1} ^{\prime} )) = X_{2} \cdot  X_{1}. $
Hence by (\ref{[hdl4, hdl7]}) $ X_{1} \cdot  X_{2} = X_{2} \cdot  X_{1}. $
Thus we have completed the proof of (\ref{[sub(1, 1), 53]}).



\end{ilfproof}

\end{document}