3a done. 3b partially

1 files changed, 38 insertions, 3 deletions

diff --git a/part2.tex b/part2.tex
index 50296f2..6959fd3 100644
--- a/part2.tex
+++ b/part2.tex
@@ -1,16 +1,16 @@
 \documentclass[12pt]{article}
 \usepackage{a4wide}
 \usepackage{latexsym}
-\usepackage{amssymb}
+\usepackage{amsmath, amssymb}
 \usepackage{epic}
 \usepackage{graphicx}
 \usepackage{gensymb}
 \usepackage[table]{xcolor}
 \usepackage{listings}
 \usepackage{tikz}
-\usepackage{amsmath}
 \usepackage{hyperref}
 \usepackage{float}
+\usepackage{enumitem}
 %\pagestyle{empty}
 \newcommand{\tr}{\mbox{\sf true}}
 \newcommand{\fa}{\mbox{\sf false}}
@@ -317,9 +317,44 @@ the smallest finite group for which it does not hold.
 
 \subsection*{Solution:}
 \subsubsection*{(a)}
+Using prover9, we found that $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ indeed rewrites to $a(p, q)$.
 
-\subsubsection*{(b)}
+We want to prove that
+\begin{enumerate}
+  \item \label{itm:logic_a_1} $\forall p \forall q : a(p, a(q, a(p, a(q, a(p, a(q, p)))))) = a(p, q)$
+\end{enumerate}
+Using the assumptions
+\begin{enumerate}[resume]
+  \item \label{itm:logic_a_2} $a(x, x) = x$
+  \item \label{itm:logic_a_3} $a(x, y) = a(y, x)$
+  \item \label{itm:logic_a_4} $a(x, a(y, z)) = a(a(x, y), z)$
+\end{enumerate}
+We do this by finding a counterexample
+\begin{enumerate}[resume]
+  \item \label{itm:logic_a_5} $\exists c1, c2 : a(c1, a(c2, a(c1, a(c2, a(c1, a(c2, c1)))))) \neq a(c1, c2)$
+\end{enumerate}
+First, apply \ref{itm:logic_a_3} to \ref{itm:logic_a_5}
+\begin{enumerate}[resume]
+  \item \label{itm:logic_a_6} $\exists c1, c2 : a(c1, a(c2, a(c1, a(c2, a(c1, a(c1, c2)))))) \neq a(c1, c2)$
+\end{enumerate}
+Then, apply \ref{itm:logic_a_2} to \ref{itm:logic_a_4}, where $x \gets x, y \gets x, z \gets y$
+\begin{enumerate}[resume]
+  \item \label{itm:logic_a_7} $a(x, a(x, y)) = a(x, y)$
+\end{enumerate}
+On \ref{itm:logic_a_7}, we can then apply \ref{itm:logic_a_3} twice
+\begin{enumerate}[resume]
+  \item \label{itm:logic_a_8} $a(x, a(y, x)) = a(y, x)$
+\end{enumerate}
+Finally, we can recursively apply \ref{itm:logic_a_7} and \ref{itm:logic_a_8} to \ref{itm:logic_a_6}, where $c1 \gets x$ and $c2 \gets y$
+\begin{enumerate}[resume]
+  \item \label{itm:logic_a_9} $a(x, a(y, a(x, a(y, a(x, a(y, x)))))) \neq a(x, a(y, a(x, a(y, a(x, a(y, x))))))$
+\end{enumerate}
+which evaluates to $FALSE$.
+\\
+This proves that $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ indeed rewrites to $a(p, q)$.
 
+\subsubsection*{(b)}
+The first 3 properties hold for every group. The fourth property does not hold for all groups though.
 
 \section*{Problem: }
 Give a precise description of a non-trivial problem of your own choice, and