solution for 3a

[ar1516.git] / a2 / 3.tex

diff --git a/a2/3.tex b/a2/3.tex
index c2c610f..a7b1b60 100644 (file)
--- 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.