\section{Problem 3}
\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$
		with an element $I\in G$, a binary operator $∗$ and a unary
		operator $inv$ satisfying.
		$$x*(y*z)=(x*y)*z, x*I=x\text{ and }x*inv(x)=I,$$
		for all $x,y,z\in G$. Determine whether in every group each of
		the four properties
		$$I*x=x, inv(inv(x))=x, inv(x)*x=I\text{ and } x*y=y*x$$
		holds for all $x,y\in G$. If a property does not hold,
		determine the size of the smallest finite group for which it
		does not hold.}\\

		As found by \textsc{prover9} a proof for $I*x=x$.
		\begin{lstlisting}
1  I * x = x.                [goal].
2  x * (y * z) = (x * y) * z.[assumption].
3  (x * y) * z = x * (y * z).[copy(2),flip(a)].
4  x * I = x.                [assumption].
5  x * inv(x) = I.           [assumption].
6  I * c1 != c1.             [deny(1)].
7  x * (I * y) = x * y.      [para(4(a,1),3(a,1,1)),flip(a)].
8  x * (inv(x) * y) = I * y. [para(5(a,1),3(a,1,1)),flip(a)].
13 I * inv(inv(x)) = x.      [para(5(a,1),8(a,1,2)),rewrite([4(2)]),flip(a)].
15 x * inv(inv(y)) = x * y.  [para(13(a,1),3(a,2,2)),rewrite([4(2)])].
16 I * x = x.                [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])].
17 \$F.                      [resolve(16,a,6,a)].
		\end{lstlisting}

		As found by \textsc{prover9} a proof for $inv(inv(x))=x$.
		\begin{lstlisting}
19 x * (inv(x) * y) = y.     [back_rewrite(8),rewrite([16(5)])].
22 inv(inv(x)) = x.          [para(5(a,1),19(a,1,2)),rewrite([4(2)]),flip(a)].
23 \$F.                      [resolve(22,a,6,a)].
		\end{lstlisting}

		As found by \textsc{prover9} a proof for $x*inv(x)=I$.
		\begin{lstlisting}
24 inv(x) * x = I.           [para(22(a,1),5(a,1,2))].
25 \$F.                      [resolve(24,a,6,a)].
\end{lstlisting}

		\textsc{prover9} fails to find a proof for $x*y=y*x$.
		Running the same file with \textsc{mace4} gives the smallest
		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{Smallest counterexample for problem 3a}\label{tab:s3a}
		\end{table}
		\newpage
	\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
		$c$ and $d$ may swapped in $a(b,a(c,a(d,a(e,a(f,a(b,g))))))$ by
		rewriting, that is, $a(b,a(c,a(d,a(e,a(f,a(b,g))))))$ rewrites
		in a finite number of steps to
		$a(b,a(d,a(c,a(e,a(f,a(b,g))))))$.}\\

		When inspecting the rewrite rule more closely we see that the
		entire structure of the formula stays the same and that only
		the variables $x,y,z$ are changed in order. Thus we can simplify the
		rule and question to
		$$x,y,z\rightarrow y,z,x\text{ and }
		b,c,d,e,f,b\overset{*?}{\rightarrow}b,d,c,e,f,b$$

		Applying these changes changes the problem into a model checking
		problem. For every position $i\in\{0\ldots5\}$ a variable $p_i$ of the
		enumeration type $\{b,c,d,e,f\}$ is defined. To keep track of the moves
		a move $m\in\{0\ldots4\}$ variable that indicates the location of the
		first variable or $0$ for the initial value is defined. The initial
		values of the position variables are
		$$p_0=b\wedge p_1=c\wedge p_2=d\wedge p_3=e\wedge p_4=f\wedge p_5=b
		\wedge m=0$$
		There are four possible transitions as shown below.
		$$\begin{array}{rrl}
			& (next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
				\wedge next(p_2)=p_0 \wedge\\
			& & next(p_3)=p_3 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5)\\
			\vee & (next(m)=2 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_2 
				\wedge next(p_2)=p_3 \wedge\\
			& & next(p_3)=p_1 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5)\\
			\vee & (next(m)=3 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
				\wedge next(p_2)=p_3 \wedge\\
			& & next(p_3)=p_4 \wedge next(p_4)=p_2 \wedge next(p_5)=p_5)\\
			\vee & (next(m)=4 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
				\wedge next(p_2)=p_2 \wedge\\
			& & next(p_3)=p_4 \wedge next(p_4)=p_5 \wedge next(p_5)=p_3)
		\end{array}$$

		With the following goal the solution below is
		found by \textsc{NuSMV} within $0.01$ seconds.
		$$\mathcal{G} \neg(p_0=b\wedge p_1=d\wedge p_2=c\wedge
		p_3=e\wedge p_4=f\wedge p_5=b)$$
		$$\begin{array}{rl}
			\overline{b,c,d},e,f,b 
				& \rightarrow c,d,\overline{b,e,f},b\\
				& \rightarrow c,d,e,\overline{f,b,b}\\
				& \rightarrow c,d,e,\overline{b,b,f}\\
				& \rightarrow c,\overline{d,e,b},f,b\\
				& \rightarrow c,\overline{e,b,d},f,b\\
				& \rightarrow \overline{c,b,d},e,f,b\\
				& \rightarrow b,\overline{d,c,e},f,b\\
				& \rightarrow b,c,e,d,f,b\\
		\end{array}$$
\end{enumerate}
