From 0f356708951ed635f69b0f15527acb9b0d6b4173 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 24 Feb 2016 13:38:07 +0100
Subject: [PATCH] product automaton

---
 e3.tex | 43 +++++++++++++++++++++++++++++++++++--------
 1 file changed, 35 insertions(+), 8 deletions(-)

diff --git a/e3.tex b/e3.tex
index 33bcca5..4bce446 100644
--- a/e3.tex
+++ b/e3.tex
@@ -21,13 +21,23 @@
 \maketitle
 \begin{enumerate}
 	\item
+		$\begin{array}{rl}
+			\Psi_1 
+			& =\exists\ev\forall\al c\\
+			& =\exists(true\un\forall\al c)\\
+			& =\exists(true\un\neg\exists\ev\neg c)\\
+			& =\exists(true\un\neg\exists(true\un \neg c))\\
+			\Psi_2
+			& =\forall(a\un\forall\ev c)\\
+			\ldots
+		\end{array}$
 	\item 
 		$\text{TS}\vDash\Phi_1\Leftrightarrow \{s_0\}\subseteq Sat(
 			\exists\ev\forall\al c)\\
 		Sat(c)= \{s_3, s_4\}\\
 		Sat(\forall\al (s_3\vee s_4))= \{s_4\}\\
 		Sat(\exists\ev(s_4)= \{s_0,s_1\}\\
-		\{s_0\}\subseteq \{s_0,s_1\}\text{ thus }\Phi_1\text{ is satisfied}$
+		\{s_0\}\subseteq \{s_0,s_1,s_4\}\text{ thus }\Phi_1\text{ is satisfied}$
 		\\\strut\\
 		$\text{TS}\vDash\Phi_2\Leftrightarrow \{s_0\}\subseteq Sat(
 			\forall(a\un \forall\ev c))\\
@@ -37,6 +47,7 @@
 		Sat(\forall(a\un \forall\ev c))=\{s_0,s_1,s_4\}\\
 		\{s_0\}\subseteq \{s_0,s_1,s_4\}\text{ thus }\Phi_2\text{ is satisfied} $
 	\item 
+
 	\item
 		For formula:
 		$$\varphi:=\al(a\ra(\neg b\un(a\wedge b)))$$
@@ -45,13 +56,29 @@
 			\neg\varphi 
 			& :=\ev\neg(a\ra(\neg b\un(a\wedge b)))\\
 			& :=\ev(a\wedge\neg(\neg b\un(a\wedge b)))\\
-			& :=\ev(a\wedge(\al\neg b\vee
-				
-				
-		\end{array}$$
-		Elementary sets:
-		$$\begin{array}{lll}
-			a & b & 
+			& :=\ev(a\wedge\neg\ev b\vee(\neg b\un(b\wedge \neg a)))
 		\end{array}$$
+		$$\xymatrix{
+			\ar[r] & 
+				*+[Fo]{q_0}
+					\ar[r]^{a\wedge\neg b}
+					\ar@(ul,ur)^{\neg a}
+					\ar[d]^{a\wedge b} &
+				*+[F]{q_2}
+					\ar@(ul,ur)^{\neg b}
+					\ar[d]^{b\vee\neg a}\\
+			  	& *+[Fo]{q_1} \ar@(dl,ul)^{true}
+			  	& *+[F]{q_3} \ar@(dr,ur)_{true}
+		}$$
+		Which leads to the following product TS:
+		$$\xymatrix{
+			\ar[dr] & s_0 & s_1 & s_2 & s_3\\
+			q_0 & *+[Fo]{}\ar[r]\ar[ddrrr]   & *+[Fo]{}\ar[dr]\\
+			q_1 & *+[Fo]{}\ar[r]\ar@/_/[rrr] & *+[Fo]{}\ar[r] & *+[Fo]{}\ar@(u,r)\ar[r] & *+[Fo]{}\ar@/^/[lll]\\
+			q_2 & *+[F]{}\ar@/_/[rrr]\ar[dr] &                &                         & *+[F]{}\ar@/^/[lll]\\
+			q_3 & *+[F]{}\ar@/_/[rrr]\ar[r]  & *+[F]{}\ar[r]  & *+[F]{}\ar@(u,r)\ar[r]  & *+[F]{}\ar@/^/[lll]
+		}$$
+		Thus forexample the path: $(s_0s_3)^{\omega}$ is a counterexample.
+
 \end{enumerate}
 \end{document}
-- 
2.20.1