From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 3 Jan 2016 14:40:27 +0000 (+0100)
Subject: added stuff about 3a
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=1720129ce172e0d36a56a5a6b97a358a86602d07;p=ar1516.git

added stuff about 3a
---

diff --git a/a2/3.tex b/a2/3.tex
index d29e965..7d59e59 100644
--- a/a2/3.tex
+++ b/a2/3.tex
@@ -11,7 +11,65 @@ tools rather than elaborating the questions by hand.}
 		$$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.}
+		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}
+1  inv(inv(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  inv(inv(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)])].
+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}
+1  inv(x) * x = I.           [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  inv(c1) * c1 != I.        [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)])].
+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)].
+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$.
+
+
+
 	\item\emph{A term rewrite sysetm 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 37f6b7e..5fc61c6 100644
--- a/a2/pre.tex
+++ b/a2/pre.tex
@@ -12,10 +12,11 @@
 
 \everymath{\displaystyle}
 
-\lstset{keepspaces=true,captionpos=b,basicstyle=\ttfamily}
+\lstset{keepspaces=true,captionpos=b,basicstyle=\scriptsize\ttfamily}
 
 \CompileMatrices%
 
+
 \author{Mart Lubbers (s4109503)}
 \title{Automated reasoning Assignment 2} 
 \date{\today}
diff --git a/a2/src/3a.prvr9 b/a2/src/3a.prvr9
new file mode 100644
index 0000000..8ee213c
--- /dev/null
+++ b/a2/src/3a.prvr9
@@ -0,0 +1,11 @@
+formulas(assumptions).
+x*(y*z)=(x*y)*z.
+x*I=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.
+end_of_list.