\documentclass{article}

\usepackage{a4wide}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage[all]{xypic}

\newcommand{\ra}{\rightarrow}
\newcommand{\un}{\text{ \textsf{U} }}
\newcommand{\ev}{\lozenge}
\newcommand{\al}{\square}
\newcommand{\nx}{\bigcirc}

\everymath{\displaystyle}

\author{Mart Lubbers}
\date{\today}
\title{Model Checking Excercises 3}

\begin{document}
\maketitle
\begin{enumerate}
	\item
	\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}$
		\\\strut\\
		$\text{TS}\vDash\Phi_2\Leftrightarrow \{s_0\}\subseteq Sat(
			\forall(a\un \forall\ev c))\\
		Sat(c)= \{s_3, s_4\}\\
		Sat(\forall\ev(s_3\vee s_4))=\{s_0,s_1,s_4\}\\
		Sat(a)= \{s_0, s_1\}\\
		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)))$$
		We create an automaton $\neg\varphi$ where
		$$\begin{array}{rlr}
			\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(\neg b\un(a\wedge b))))\\
			& :=\ev(a\wedge\al\neg b)\vee\ev(a\wedge(\neg b\un(a\wedge b)))\\
			& :=\ev(a\wedge\neg\ev b) & \ev(a\wedge(\neg b\un(a\wedge b)))\\
		\end{array}$$
		Elementary sets for $\varphi=\ev(a\wedge\neg\ev b)$ where
		$\psi=a\wedge\neg\ev b$:
		$$\begin{array}{llll}
			a & b & \varphi & \ev\psi\\
			a & b & \varphi & \ev\psi\\
		\end{array}$$
\end{enumerate}
\end{document}
