From def489dbcf463db0afe0b1db8f9379bf88516294 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Mon, 30 Nov 2015 18:04:30 +0100
Subject: [PATCH] added proof bit

---
 mbt_exercises/mbt.tex | 81 ++++++++++++++++++++++++++++++-------------
 mbt_exercises/pre.tex |  3 +-
 2 files changed, 59 insertions(+), 25 deletions(-)

diff --git a/mbt_exercises/mbt.tex b/mbt_exercises/mbt.tex
index 18857c5..8efa296 100644
--- 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
--- 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}
-- 
2.20.1