solution for 3a

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.

diff --git a/a2/pre.tex b/a2/pre.tex
index 5fc61c6..cd9af74 100644 (file)
--- 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 (file)
--- 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.