From 6aaf14d508bd3ff12e0639accfc91d55b346d562 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 3 Jan 2016 16:16:27 +0100
Subject: [PATCH] update, table

---
 a2/3.tex        | 13 ++++++-------
 a2/4.tex        |  7 ++++++-
 a2/src/3a.prvr9 |  8 ++++----
 3 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/a2/3.tex b/a2/3.tex
index 7d59e59..c2c610f 100644
--- a/a2/3.tex
+++ b/a2/3.tex
@@ -1,5 +1,5 @@
 \section{Problem 3}
-\emph{The goal of this problem is to exploit the power of the recom mended
+\emph{The goal of this problem is to exploit the power of the recommended
 tools rather than elaborating the questions by hand.}
 \begin{enumerate}[a.]
 	\item\emph{In mathematics, a \emph{group} is defined to be a set $G$
@@ -67,10 +67,12 @@ tools rather than elaborating the questions by hand.}
 \end{lstlisting}
 
 		\textsc{prover9} fails to find a proof for $x*y=y*x$.
+		Running the same file with \textsc{mace4} gives the following
+		counterexample.
 
 
 
-	\item\emph{A term rewrite sysetm consists of the single rule
+	\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.
 		Moreover, there are constants $b,c,d,e,f,g$. Determine whether
@@ -96,7 +98,7 @@ tools rather than elaborating the questions by hand.}
 		values of the position variables is
 		$$p_0=b,p_1=c,p_2=d,p_3=e,p_4=f,p_5=b$$
 		There are four possible transitions and they are put in a
-		disjuction and shown below:
+		disjunction and shown below:
 		$$\begin{array}{rl}
 			next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
 				\wedge next(p_2)=p_0 \wedge\\
@@ -119,7 +121,7 @@ tools rather than elaborating the questions by hand.}
 		p_3=e\wedge p_4=f\wedge p_5=b)$$
 
 		The solution described below is found by
-		\textsc{NuSMV} within $0.01$ seconds. Overline triples are the
+		\textsc{NuSMV} within $0.01$ seconds. Overlined triples are the
 		ones changed in the next.
 		$$\begin{array}{rl}
 			\overline{b,c,d},e,f,b 
@@ -132,7 +134,4 @@ tools rather than elaborating the questions by hand.}
 				& \rightarrow b,\overline{d,c,e},f,b\\
 				& \rightarrow b,c,e,d,f,b\\
 		\end{array}$$
-
-		
-
 \end{enumerate}
diff --git a/a2/4.tex b/a2/4.tex
index 1147320..7fcece0 100644
--- a/a2/4.tex
+++ b/a2/4.tex
@@ -107,6 +107,11 @@ $$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right)
 
 \subsection{Solution}
 The conversion to SMT-Lib is trivial however on a $3.8Ghz$ processor running
-\textsc{yices} it takes about $4$ hours and $15$ minutes to find a solution.
+\textsc{yices} it takes about $4$ hours and $15$ minutes to find the solution
+listed in Table~\ref{tab:sol}.
 
+\begin{table}[H]
+	\centering
 \input{src/4/a4.tex}
+	\caption{Solution for \emph{English peg solitaire}}\label{tab:sol}
+\end{table}
diff --git a/a2/src/3a.prvr9 b/a2/src/3a.prvr9
index 8ee213c..812fdd4 100644
--- a/a2/src/3a.prvr9
+++ b/a2/src/3a.prvr9
@@ -1,11 +1,11 @@
 formulas(assumptions).
-x*(y*z)=(x*y)*z.
-x*I=x.
-x*inv(x)=I.
+all x all y all z (x*(y*z)=(x*y)*z).
+all x (x*I=x).
+all x (x*inv(x)=I).
 end_of_list.
 formulas(goals).
 %I*x=x.
 %inv(inv(x))=x.
 %inv(x)*x=I.
-x*y=y*x.
+all x all y (x*y=y*x).
 end_of_list.
-- 
2.20.1