part 3 done

1 files changed, 131 insertions, 6 deletions

diff --git a/part2.tex b/part2.tex
index 6959fd3..e6b11e9 100644
--- a/part2.tex
+++ b/part2.tex
@@ -317,8 +317,6 @@ 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)$.
-
 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)$
@@ -345,16 +343,143 @@ 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$
+Finally, we can recursively apply \ref{itm:logic_a_3}, \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$.
+which evaluates to $FALSE$.\\
+Therefore, we found that no counterexample exists, which proves that $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ indeed rewrites to $a(p, q)$.
 \\
-This proves that $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ indeed rewrites to $a(p, q)$.
+We derived this proof with \textit{prover9}, using the following input:
+\begin{lstlisting}
+formulas(sos).
+	a(x,x)=x.
+	a(x,y)=a(y,x).
+	a(x,a(y,z))=a(a(x,y),z).
+end_of_list.
+
+formulas(goals).
+	all p all q (a(p,a(q,a(p,a(q,a(p,a(q,p))))))=a(p,q)).
+end_of_list.
+\end{lstlisting}
 
 \subsubsection*{(b)}
-The first 3 properties hold for every group. The fourth property does not hold for all groups though.
+We want to prove 4 things:
+\begin{enumerate}
+  \item \label{itm:logic_b_1} $\forall x : I * x = x$
+  \item \label{itm:logic_b_2} $\forall x : inv(inv(x)) = x$
+  \item \label{itm:logic_b_3} $\forall x : inv(x) * x = I$
+  \item \label{itm:logic_b_4} $\forall x \forall y : x * y = y * x$
+\end{enumerate}
+Using the assumptions
+\begin{enumerate}[resume]
+ \item \label{itm:logic_b_5} $x * (y * z) = (x * y) * z$
+ \item \label{itm:logic_b_6} $x * I = x$
+ \item \label{itm:logic_b_7} $x * inv(x) = I$
+\end{enumerate}
+
+To prove \ref{itm:logic_b_1}, \ref{itm:logic_b_2}, \ref{itm:logic_b_3} and \ref{itm:logic_b_4}, we created the following input:
+\begin{lstlisting}
+formulas(sos).
+	(x*(y*z)=(x*y)*z).
+	(x*I=x).
+	(x*inv(x)=I).
+end_of_list.
+
+formulas(goals).
+	all x (I*x=x).
+	all x (inv(inv(x))=x).
+	all x (inv(x)*x=I).
+	all x all y (x*y=y*x).
+end_of_list.
+\end{lstlisting}
+
+Running this input through \textit{prover9} generated the following proofs for \ref{itm:logic_b_1}, \ref{itm:logic_b_2} and \ref{itm:logic_b_3} respectively:
+\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_1}]
+1 (all x I * x = x) # label(non_clause) # label(goal).  [goal].
+5 x * (y * z) = (x * y) * z.  [assumption].
+6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
+7 x * I = x.  [assumption].
+8 x * inv(x) = I.  [assumption].
+9 I * c1 != c1.  [deny(1)].
+13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
+14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
+19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
+21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
+22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
+23 $F.  [resolve(22,a,9,a)].
+\end{lstlisting}
+
+\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_2}]
+2 (all x inv(inv(x)) = x) # label(non_clause) # label(goal).  [goal].
+5 x * (y * z) = (x * y) * z.  [assumption].
+6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
+7 x * I = x.  [assumption].
+8 x * inv(x) = I.  [assumption].
+10 inv(inv(c2)) != c2.  [deny(2)].
+13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
+14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
+19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
+21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
+22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
+26 x * (inv(x) * y) = y.  [back_rewrite(14),rewrite([22(5)])].
+30 inv(inv(x)) = x.  [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)].
+31 $F.  [resolve(30,a,10,a)].
+\end{lstlisting}
+
+\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_3}]
+3 (all x inv(x) * x = I) # label(non_clause) # label(goal).  [goal].
+5 x * (y * z) = (x * y) * z.  [assumption].
+6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
+7 x * I = x.  [assumption].
+8 x * inv(x) = I.  [assumption].
+11 inv(c3) * c3 != I.  [deny(3)].
+13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
+14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
+19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
+21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
+22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
+26 x * (inv(x) * y) = y.  [back_rewrite(14),rewrite([22(5)])].
+30 inv(inv(x)) = x.  [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)].
+34 inv(x) * x = I.  [para(30(a,1),8(a,1,2))].
+35 $F.  [resolve(34,a,11,a)].
+\end{lstlisting}
+
+\textit{prover9} was not able to prover that $x * y = y * x$ holds for all finite groups. Therefor, we ran \ref{itm:logic_b_4} through \textit{mace4} to find the smallest group $G(I, *, inv)$ for which $x * y \neq y * x$.
+The following input was used:
+\begin{verbatim}
+formulas(sos).
+	(x*(y*z)=(x*y)*z).
+	(x*I=x).
+	(x*inv(x)=I).
+end_of_list.
+
+formulas(goals).
+	all x all y (x*y=y*x).
+end_of_list.
+\end{verbatim}
+After running this input through \textit{mace4}, we retrieved the following finite group $G(I, *, inv)$:
+\begin{verbatim}
+ I: 0
+ 
+ *:    | 0 1 2 3 4 5
+     --*-------------
+     0 | 0 1 2 3 4 5 
+     1 | 1 0 3 2 5 4
+     2 | 2 4 0 5 1 3
+     3 | 3 5 1 4 0 2
+     4 | 4 2 5 0 3 1
+     5 | 5 3 4 1 2 0
+ 
+ inv: 0 -> 0 
+      1 -> 1
+      2 -> 2
+      3 -> 3
+      4 -> 4
+      5 -> 5
+\end{verbatim}
+We specify the row number in the $*$-operator table to be the left element, and the column number to be the right element.
+Let $x \gets 2$ and $y \gets 1$. Then, we know that $x * y = 2 * 1 = 4$. Also, $y * x = 1 * 2 = 3$. Since $4 \neq 3$, we know that $x * y \neq y * x$, which proves that the property $x * y = y * x$ indeed does not hold for this group.
 
 \section*{Problem: }
 Give a precise description of a non-trivial problem of your own choice, and