added proof bit

diff --git a/mbt_exercises/mbt.tex b/mbt_exercises/mbt.tex
index 18857c5..8efa296 100644 (file)
--- a/mbt_exercises/mbt.tex
+++ b/mbt_exercises/mbt.tex
@@ -97,42 +97,75 @@
        \item $\bordermatrix{
                        i\setminus s& P_1 & P_2 & P_3 & P_4\cr
                        P_1 & 1 & 0 & 0 & 0\cr
-                       P_2 & 0 & 1 & \cr
-                       P_3 & 0 & 0 & 1\cr
+                       P_2 & 0 & 1 & 0 & 0\cr
+                       P_3 & 0 & 0 & 1 & 0\cr
                        P_4 & 0 & 0 & 1 & 1\cr
                }$
        \item
-               $P_1=\xymatrix{
+               $P_1=\xymatrix@C=1pc@R=1pc{
                        \ar[dr]&\\
-                              & s_0\ar[d]^a\\
-                              & s_1\ar[d]^b\\
-                              & s_2\ar[d]^c\\
-                              & s_3\\
+                               & *+[o][F-]{s_0}\ar[d]^a\\
+                               & *+[o][F-]{s_1}\ar[d]^b\\
+                               & *+[o][F-]{s_2}\ar[d]^c\\
+                               & *+[o][F-]{s_3}\\
                }$
-               $P_2=\xymatrix{
+               $P_2=\xymatrix@C=1pc@R=1pc{
                        \ar[dr]&\\
-                              & s_0\ar[d]^a\\
-                              & s_1\ar[d]^b\\
-                              & s_2\ar[dl]^c\ar[dr]^d\\
-                       s_3    & & s_4\\
+                               & *+[o][F-]{s_0}\ar[d]^a\\
+                               & *+[o][F-]{s_1}\ar[d]^b\\
+                               & *+[o][F-]{s_2}\ar[dl]_c\ar[dr]^d\\
+                       *+[o][F-]{s_3} & & *+[o][F-]{s_4}\\
                }$
-               $P_3=\xymatrix{
-                       \ar[dr]     &\\
-                                   & s_0\ar[d]^a\\
-                                   & s_1\ar[dl]^b\ar[dr]^b\\
-                       s_2\ar[d]^c & & s_3\ar[d]^d\\
-                       s_4         & & s_5\\
+               $P_3=\xymatrix@C=1pc@R=1pc{
+                       \ar[dr] &\\
+                               & *+[o][F-]{s_0}\ar[d]^a\\
+                               & *+[o][F-]{s_1}\ar[dl]_b\ar[dr]^b\\
+                       *+[o][F-]{s_2}\ar[d]^c & & *+[o][F-]{s_3}\ar[d]^d\\
+                       *+[o][F-]{s_4} & & *+[o][F-]{s_5}\\
                }$
-               $P_4=\xymatrix{
-                       \ar[dr]     &\\
-                                   & s_0\ar[dl]^a\ar[dr]^a\\
-                       s_2\ar[d]^b & & s_3\ar[d]^b\\
-                       s_4\ar[d]^c & & s_5\ar[d]^d\\
-                       s_6         & & s_7
+               $P_4=\xymatrix@C=1pc@R=1pc{
+                       \ar[dr] &\\
+                               & *+[o][F-]{s_0}\ar[dl]_a\ar[dr]^a\\
+                       *+[o][F-]{s_2}\ar[d]^b & & *+[o][F-]{s_3}\ar[d]^b\\
+                       *+[o][F-]{s_4}\ar[d]^c & & *+[o][F-]{s_5}\ar[d]^d\\
+                       *+[o][F-]{s_6} & & *+[o][F-]{s_7}
                }$
 \end{enumerate}
 
 \subsection{Testing equivalences}
+\begin{enumerate}[a)]
+       \item
+               \begin{align*}
+                       \sigma\in traces(p)\leftrightarrow
+                               p\text{ \bf after }\sigma\text{ \bf refuses }\emptyset\\
+                       \sigma\in traces(p)\leftrightarrow
+                               \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in
+                               \emptyset:p'\cancel{\overset{a}{\rightarrow}} & & 2.\\
+                       \sigma\in traces(p)\leftrightarrow
+                               \exists p':p\overset{\sigma}{\Rightarrow}p'\\
+                       \sigma\in \{\sigma\in L^*|p\overset{\sigma}{\Rightarrow}\}\leftrightarrow
+                               \exists p':p\overset{\sigma}{\Rightarrow}p'& & \square\\
+               \end{align*}
+       \item
+               \begin{align*}
+                       p\text{ \bf after }\sigma\text{ \bf refuses } A\leftrightarrow
+                               \sigma\cdot A\in Ftraces(p)\\
+                       \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in
+                               A:p'\cancel{\overset{a}{\rightarrow}} \leftrightarrow
+                               \sigma\cdot A\in Ftraces(p) & & 2.\\
+                       \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in
+                               A:p'\cancel{\overset{a}{\rightarrow}} \leftrightarrow
+                               \sigma\cdot A\in \{\psi\in(L\cup
+                               \mathcal{P}(L))^*|p\overset{\sigma}{\Rightarrow}\} & & 4.\\
+               \end{align*}
+       \item
+               \begin{align*}
+               \end{align*}
+       \item
+               \begin{align*}
+               \end{align*}
+\end{enumerate}
+
 \subsection{Testing equivalences}
 \subsection{Testing equivalences}
 

diff --git a/mbt_exercises/pre.tex b/mbt_exercises/pre.tex
index 59d2e91..723347a 100644 (file)
--- a/mbt_exercises/pre.tex
+++ b/mbt_exercises/pre.tex
@@ -1,7 +1,8 @@
-\documentclass{article}
+\documentclass[twocolumn]{article}
 
 \usepackage{enumerate}
 \usepackage{amssymb}
+\usepackage{cancel}
 \usepackage{amsmath}
 \usepackage{a4wide}
 \usepackage{xypic}