\documentclass{article}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% COMANDOS AUXILIARES 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\newcommand{\handwriting}{\ding{45}}
\newcommand{\checkedtrue}{\ding{52}}
\newcommand{\checkedfalse}{\ding{56}}
\newcommand{\manualchecktrue}{\handwriting \checkedtrue}
\newcommand{\manualcheckfalse}{\handwriting \checkedfalse}
\newcommand{\circrefines}{\sqsubseteq}
\newcommand{\circsimulates}{\preceq}
\newcommand{\true}{true}
\newcommand{\false}{false}
\newcommand{\arithmos}{\it Arithmos}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% ADICIONANDO PACOTES 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\usepackage{circus}
\usepackage{pifont}
\begin{document}

\tableofcontents


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% OBRIGACOES DE PROVA 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\newpage
\section{Obrigacoes de Prova}

\begin{tabular}{|c|c|l|}
     \hline 
     \textbf{Operadores} & \textbf{B++} & \textbf{Harvey} \\ 
     \hline
     \textbf{(I)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((((((second' \in (0 \upto 59)) \\
     \t1   \land ((minute' \in (0 \upto 59)) \\
     \t1   \land \true)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land ((second' = minute') \\
     \t1   \land (minute' = 0))) \\
     \t1   \iff ((second' = 0) \\
     \t1   \land (minute' = 0)))  \\
     \end{block} $ \\		
     
     \hline
     \textbf{(II)} &   \checkedtrue  &
     $ \begin{block}
     \t1  (((\alpha  ([second' : \arithmos ;   \\) \\
     \t1  | \true ]  \\) \cap (\alpha  ([minute' : \arithmos ;   \\) \\
     \t1  | \true ]  \\)) = \emptyset) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(III)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((DFV-E  (second' = 0)) \subseteq (\alpha  ([second' : \arithmos ;   \\) \\
     \t1  | \true ]  \\)) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(IV)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((DFV-E  (minute' = 0)) \subseteq (\alpha  ([minute' : \arithmos ;   \\) \\
     \t1  | \true ]  \\)) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(V)} &   \checkedtrue  &
     $ \begin{block}
     \t1  \lnot((SecSt \in (FV-P  (Achronometer)))) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(VI)} &   \checkedtrue  &
     $ \begin{block}
     \t1  \lnot((MinSt \in (FV-P  (Achronometer)))) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(VII)} &   \checkedtrue  &
     $ \begin{block}
     \t1  \lnot((SecInit \in (FV-P  (Achronometer)))) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(VIII)} &   \checkedtrue  &
     $ \begin{block}
     \t1  \lnot((MinInit \in (FV-P  (Achronometer)))) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(IX)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((((((second' \in (0 \upto 59)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land (second' = 0)) \\
     \t1   \iff (second' = 0))  \\
     \end{block} $ \\		
     
     \hline
     \textbf{(X)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((((((minute' \in (0 \upto 59)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land (minute' = 0)) \\
     \t1   \iff (minute' = 0))  \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XI)} &   \checkedtrue  &
     $ \begin{block}
     \t1  \lnot((RunSec \in (FV-P  (Achronometer)))) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XII)} &   \checkedtrue  &
     $ \begin{block}
     \t1  \lnot((RunMin \in (FV-P  (Achronometer)))) \\
     \end{block} $ \\		
     
     \hline
     \end{tabular}
     \newpage
     \begin{tabular}{|c|c|l|}
     \hline
     \textbf{(XIII)} &  ? &
     $ \begin{block}
     \t1     \t1    \t1 Run \\
     \t1     \t1 \circseq \\
     \t1     \t1    \t1 (   \t1 \circmu X @  \\
     \t1     \t1    \t1    \t1    \t1    \t1 RunSec \\
     \t1     \t1    \t1    \t1    \t1 \circseq \\
     \t1     \t1    \t1    \t1    \t1    \t1 X \\
     \t1     \t1    \t1    \lpar \{second\} | Sync | \{minute\} \rpar \\
     \t1     \t1    \t1    \t1 \circmu X @  \\
     \t1     \t1    \t1    \t1    \t1    \t1 RunMin \\
     \t1     \t1    \t1    \t1    \t1 \circseq \\
     \t1     \t1    \t1    \t1    \t1    \t1 X \\
     \t1     \t1    \t1 ) \circhide Sync \\
     \t1  \circrefines \\
     \t1     \t1 (   \t1 \circmu X @  \\
     \t1     \t1    \t1    \t1    \t1 RunSec \\
     \t1     \t1    \t1    \t1 \circseq \\
     \t1     \t1    \t1    \t1    \t1 X \\
     \t1     \t1    \lpar \{second\} | Sync | \{minute\} \rpar \\
     \t1     \t1    \t1 \circmu X @  \\
     \t1     \t1    \t1    \t1    \t1 RunMin \\
     \t1     \t1    \t1    \t1 \circseq \\
     \t1     \t1    \t1    \t1    \t1 X \\
     \t1     \t1 ) \circhide Sync \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XIV)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((Sync \cap (usedC (\t1 [second' : \arithmos ;   \\ \t1 | (second' = 0) ]  \\ \circseq \t1 [minute' : \arithmos ;   \\ \t1 | (minute' = 0) ]  \\))) = \emptyset) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XV)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((wrtV ([minute' : \arithmos ;   \\ | (minute' = 0) ]  \\)) \subseteq \{minute\}) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XVI)} &   \checkedtrue  &
     $ \begin{block}
     \t1  (((wrtV ([minute' : \arithmos ;   \\ | (minute' = 0) ]  \\)) \cap (usedV  (\circmu X @ \t1    \t1 RunSec \t1 \circseq \t1    \t1 X))) = \emptyset) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XVII)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((wrtV ([second' : \arithmos ;   \\ | (second' = 0) ]  \\)) \subseteq \{second\}) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XVIII)} &   \checkedtrue  &
     $ \begin{block}
     \t1  (((wrtV ([second' : \arithmos ;   \\ | (second' = 0) ]  \\)) \cap (usedV  (\t1 [minute' : \arithmos ;   \\ \t1 | (minute' = 0) ]  \\ \circseq \t1 \circmu X @ \t1    \t1    \t1 RunMin \t1    \t1 \circseq \t1    \t1    \t1 X))) = \emptyset) \\
     \end{block} $ \\		
     
     \hline
     \end{tabular}
     \newpage
     \begin{tabular}{|c|c|l|}
     \hline
     \textbf{(XIX)} &   \checkedtrue  &
     $ \begin{block}
     \t1  (((((second' = ((second + 1) \mod 60)) \\
     \t1   \land (minute' = minute)) \\
     \t1   \land (((((second \in (0 \upto 59)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land ((minute \in (0 \upto 59)) \\
     \t1   \land \true)) \\
     \t1   \land \true)) \\
     \t1   \land (((((second' \in (0 \upto 59)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land ((minute' \in (0 \upto 59)) \\
     \t1   \land \true)) \\
     \t1   \land \true)) \\
     \t1   \iff ((((second \in (0 \upto 59)) \\
     \t1   \land (second' \in (0 \upto 59))) \\
     \t1   \land (second' = ((second + 1) \mod 60))) \\
     \t1   \land (((minute' \in (0 \upto 59)) \\
     \t1   \land (minute \in (0 \upto 59))) \\
     \t1   \land (minute' = minute))))  \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XX)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((FV-E  (((second \in (0 \upto 59)) \\
     \t1   \land (second' \in (0 \upto 59))) \\
     \t1   \land (second' = ((second + 1) \mod 60)))) \subseteq (\alpha  ([ second : \arithmos ;   \\) \\
     \t1  second' : \arithmos ;   ])) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XXI)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((FV-E  (((minute' \in (0 \upto 59)) \\
     \t1   \land (minute \in (0 \upto 59))) \\
     \t1   \land (minute' = minute))) \subseteq (\alpha  ([ minute : \arithmos ;   \\) \\
     \t1  minute' : \arithmos ;   ])) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XXII)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((((minute' \in (0 \upto 59)) \\
     \t1   \land (minute \in (0 \upto 59))) \\
     \t1   \land (minute' = minute)) \\
     \t1   \iff ((minute' = minute) \\
     \t1   \land ((minute \in (0 \upto 59)) \\
     \t1   \land (minute' \in (0 \upto 59)))))  \\
     \end{block} $ \\		
     
     \hline
     \end{tabular}
     \newpage
     \begin{tabular}{|c|c|l|}
     \hline
     \textbf{(XXIII)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((((((minute \in (0 \upto 59)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land ((((minute' \in (0 \upto 59)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land \true)) \\
     \t1   \land \true) \\
     \t1   \iff ((minute \in (0 \upto 59)) \\
     \t1   \land (minute' \in (0 \upto 59))))  \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XXIV)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((((\alpha  (MinSt)) \cup (\alpha  (MinSt'))) \cap (\alpha  ([second : \arithmos ;   \\) \\
     \t1  second' : \arithmos ;   \\
     \t1  | (((second \in (0 \upto 59)) \\
     \t1   \land (second' \in (0 \upto 59))) \\
     \t1   \land (second' = ((second + 1) \mod 60)))  ]  \\)) = \emptyset) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XXV)} &   \checkedtrue  &
     $ \begin{block}
     \t1  (((((minute' = ((minute + 1) \mod 60)) \\
     \t1   \land (second' = second)) \\
     \t1   \land (((((second \in (0 \upto 59)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land ((minute \in (0 \upto 59)) \\
     \t1   \land \true)) \\
     \t1   \land \true)) \\
     \t1   \land (((((second' \in (0 \upto 59)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land ((minute' \in (0 \upto 59)) \\
     \t1   \land \true)) \\
     \t1   \land \true)) \\
     \t1   \iff ((((minute \in (0 \upto 59)) \\
     \t1   \land (minute' \in (0 \upto 59))) \\
     \t1   \land (minute' = ((minute + 1) \mod 60))) \\
     \t1   \land (((second \in (0 \upto 59)) \\
     \t1   \land (second' \in (0 \upto 59))) \\
     \t1   \land (second' = second))))  \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XXVI)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((FV-E  (((minute \in (0 \upto 59)) \\
     \t1   \land (minute' \in (0 \upto 59))) \\
     \t1   \land (minute' = ((minute + 1) \mod 60)))) \subseteq (\alpha  ([ minute : \arithmos ;   \\) \\
     \t1  minute' : \arithmos ;   ])) \\
     \end{block} $ \\		
     
     \hline
     \end{tabular}
     \newpage
     \begin{tabular}{|c|c|l|}
     \hline
     \textbf{(XXVII)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((FV-E  (((second \in (0 \upto 59)) \\
     \t1   \land (second' \in (0 \upto 59))) \\
     \t1   \land (second' = second))) \subseteq (\alpha  ([ second : \arithmos ;   \\) \\
     \t1  second' : \arithmos ;   ])) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XXVIII)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((((second \in (0 \upto 59)) \\
     \t1   \land (second' \in (0 \upto 59))) \\
     \t1   \land (second' = second)) \\
     \t1   \iff ((second' = second) \\
     \t1   \land ((second \in (0 \upto 59)) \\
     \t1   \land (second' \in (0 \upto 59)))))  \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XXIX)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((((((second \in (0 \upto 59)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land ((((second' \in (0 \upto 59)) \\
     \t1   \land \true) \\
     \t1   \land \true) \\
     \t1   \land \true)) \\
     \t1   \land \true) \\
     \t1   \iff ((second \in (0 \upto 59)) \\
     \t1   \land (second' \in (0 \upto 59))))  \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XXX)} &   \checkedtrue  &
     $ \begin{block}
     \t1  ((((\alpha  (SecSt)) \cup (\alpha  (SecSt'))) \cap (\alpha  ([minute : \arithmos ;   \\) \\
     \t1  minute' : \arithmos ;   \\
     \t1  | (((minute \in (0 \upto 59)) \\
     \t1   \land (minute' \in (0 \upto 59))) \\
     \t1   \land (minute' = ((minute + 1) \mod 60)))  ]  \\)) = \emptyset) \\
     \end{block} $ \\		
     
     \hline
     \textbf{(XXXI)} &   \checkedtrue  &
     $ \begin{block}
     \t1  (((\alpha  ([ second : RANGE;   ])) \cap (\alpha  ([ minute : RANGE;   ]))) = \emptyset) \\
     \end{block} $ \\		
     
     \hline 
\end{tabular}


\end{document}