added stuff about 3a

[ar1516.git] / a2 / 3.tex

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