From 2189d01c6498c9926c39b7b2883aab32f6b059ea Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 3 Jan 2016 18:41:06 +0100
Subject: [PATCH] solution for 3a

---
 a2/3.tex        | 27 ++++++++++++++++++++++++---
 a2/pre.tex      |  1 +
 a2/src/3a.prvr9 |  8 ++++----
 3 files changed, 29 insertions(+), 7 deletions(-)

diff --git a/a2/3.tex b/a2/3.tex
index c2c610f..a7b1b60 100644
--- a/a2/3.tex
+++ b/a2/3.tex
@@ -68,10 +68,31 @@ tools rather than elaborating the questions by hand.}
 
 		\textsc{prover9} fails to find a proof for $x*y=y*x$.
 		Running the same file with \textsc{mace4} gives the following
-		counterexample.
-
-
+		counterexample listed in Table~\ref{tab:s3a}.
 
+		\begin{table}[H]
+			\centering
+			\begin{tabular}{llll}
+				$G=\{0,1,2,3,4,5\}$ & $I=0$ & 
+				$inv(x)=\left\{\begin{array}{ll}
+					x=3 & 4\\
+					x=4 & 3\\
+					\text{else} & x
+				\end{array}\right.$ &
+				$x*y=\left\{\begin{array}{ll|llllll}
+					& & \multicolumn{6}{c}{x}\\
+					 & & 0& 1 & 2 & 3 & 4 & 5\\
+					\hline
+					\multirow{6}{*}{y}& 1 & 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
+				\end{array}\right.$
+			\end{tabular}
+			\caption{Solution for problem 3a}\label{tab:s3a}
+		\end{table}
 	\item\emph{A term rewrite system consists of the single rule
 		$$a(x,a(y,a(z,u)))\rightarrow a(y,a(z,a(x,u))),$$
 		in which $a$ is a binary symbol and $x,y,z,u$ are variables.
diff --git a/a2/pre.tex b/a2/pre.tex
index 5fc61c6..cd9af74 100644
--- a/a2/pre.tex
+++ b/a2/pre.tex
@@ -9,6 +9,7 @@
 \usepackage{float} % For nice tables
 \usepackage{graphicx}
 \usepackage{xypic}
+\usepackage{multirow}
 
 \everymath{\displaystyle}
 
diff --git a/a2/src/3a.prvr9 b/a2/src/3a.prvr9
index 812fdd4..a12d73d 100644
--- a/a2/src/3a.prvr9
+++ b/a2/src/3a.prvr9
@@ -1,11 +1,11 @@
 formulas(assumptions).
 all x all y all z (x*(y*z)=(x*y)*z).
-all x (x*I=x).
-all x (x*inv(x)=I).
+all x (x*a=x).
+all x (x*inv(x)=a).
 end_of_list.
 formulas(goals).
-%I*x=x.
+%a*x=x.
 %inv(inv(x))=x.
-%inv(x)*x=I.
+%inv(x)*x=a.
 all x all y (x*y=y*x).
 end_of_list.
-- 
2.20.1