\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{\symdiff}{\mathbin{\ominus}}
\newcommand{\boolean}{{\mathbb B}}



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


\usepackage{circus}
\usepackage{pifont}



\begin{document}


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


\newpage
\section{ZBol2SMTVerit Operators Documentation}

\begin{tabular}{|c|c|c|c|}
     \hline 
     \textbf{Predicate} & \textbf{Bol++} & \textbf{Z2Bol++} & \textbf{veriT} \\ 

     \hline
    $ \begin{block}
   	\lnot \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\		
     
    \hline
    $ \begin{block}
    	 \_ \land \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\		

    \hline
    $\begin{block}
    	 \_ \lor \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\		     

    \hline
    $\begin{block}
    	 \_ \implies \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\		      

    \hline
    $\begin{block}
    	 \_ \iff \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\		       
     \hline 
     
    \hline
    $\begin{block}
 	\forall \_ | \_ @ \_
     \end{block} $ & \checkedtrue  &  \checkedtrue & \checkedtrue \\		       
    
    \hline
    $\begin{block}
 	\exists \_ | \_ @ \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue \\	

    \hline
    $\begin{block}
 	\exists_1 \_ | \_ @ \_
     \end{block} $ & \checkedfalse  &  & \checkedfalse \\

    \hline
    $ \begin{block}
   	\true \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\

    \hline
    $ \begin{block}
   	\false \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\
	
    \hline
     Expression & \checkedtrue  & \checkedtrue & \checkedtrue\\

    \hline 
	

\end{tabular}

\newpage

\begin{tabular}{|c|c|c|c|}
     \hline 
     \textbf{Expression} & \textbf{Bol++} & \textbf{Z2Bol++} & \textbf{veriT} \\ 

    \hline
    $\begin{block}
    	 \_ \in \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\

    \hline
    $\begin{block}
    	 \_ \notin \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\

    \hline
    $\begin{block}
    	 \_ \cap \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\		

    \hline
    $\begin{block}
    	 \_ \cup \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\
     \hline 	

    \hline
    $\begin{block}
    	 \_ \subset \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\

    \hline
    $\begin{block}
    	 \_ \subseteq \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \\

    \hline
    $\begin{block}
    	 \_  \emptyset \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\

    \hline
    $\begin{block}
    	 \_  \power \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \\

    \hline
    $\begin{block}
    	 \_  \setminus \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \\

    \hline
    $\begin{block}
    	\_ \symdiff \_
     \end{block} $ & \checkedfalse  &  & \checkedtrue\\

    \hline
    $\begin{block}
    	 \_  \mapsto \_
     \end{block} $ & \checkedfalse  & \checkedtrue & \\


    \hline
    $\begin{block}
    	 \_  \cross \_
     \end{block} $ & \checkedfalse  & \checkedtrue & \\

    \hline
    $\begin{block}
    	   \seq 
     \end{block} $ & \checkedtrue  & \checkedtrue & \\

    \hline
    $\begin{block}
    	   \iseq 
     \end{block} $ & \checkedtrue  & \checkedtrue & \\ 

    \hline
    $\begin{block}
    	 \_ = \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\

    \hline
    $\begin{block}
    	 \_ \neq \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\
 	
    \hline
    $\begin{block}
    	 \_ \leq \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\
    
    \hline
    $\begin{block}
    	 \_ < \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\
    
    \hline
    $\begin{block}
    	 \_ \geq \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\ 	
    
    \hline
    $\begin{block}
    	 \_  > \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\


    \hline
    $\begin{block}
    	 \_  - \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\
 
    \hline
    $\begin{block}
    	 \_  + \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\

    \hline
    $\begin{block}
    	 \_  \succ \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\ 

    \hline
    $\begin{block}
    	 \_  \mod \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\ 

    \hline
    $\begin{block}
    	 \_  \upto \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\	

    \hline
    $\begin{block}
    	 \_  \rel \_
     \end{block} $ & \checkedtrue  & \checkedtrue & \\

    \hline
    $\begin{block}
    	 \nat
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\


    \hline
    $\begin{block}
    	 \nat_1
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\

    \hline
    $\begin{block}
    	 \num
     \end{block} $ & \checkedtrue  & \checkedtrue & \checkedtrue\\

   \hline
    $\begin{block}
    	 \finset
     \end{block} $ & \checkedtrue  & \checkedtrue & \\

    \hline
    $\begin{block}
    	 \boolean
     \end{block} $ & \checkedtrue  & \checkedtrue & \\
    
    \hline
    $\begin{block}
    	 \extract
     \end{block} $ &  \checkedfalse &  & \\

     \hline 	
     $\begin{block}
    	 \extract
     \end{block} $ & \checkedfalse &  & \\

     \hline 	
     $\begin{block}
    	 \cat
     \end{block} $ & \checkedtrue & \checkedtrue & \\

    \hline 	
     $\begin{block}
    	 \fun
     \end{block} $ & \checkedtrue & \checkedtrue & \\

     \hline 	
     $\begin{block}
    	 \pfun
     \end{block} $ & \checkedtrue & \checkedtrue & \\

     \hline 	
     $\begin{block}
    	 \inj
     \end{block} $ & \checkedtrue & \checkedtrue & \\

	\hline 	
     $\begin{block}
    	 \pinj
     \end{block} $ & \checkedtrue & \checkedtrue & \\

	\hline 	
     $\begin{block}
    	 \surj
     \end{block} $ & \checkedtrue & \checkedtrue & \\

	\hline 	
     $\begin{block}
    	 \psurj
     \end{block} $ & \checkedtrue & \checkedtrue & \\

	\hline 	
     $\begin{block}
    	 \bij
     \end{block} $ & \checkedtrue &  \checkedtrue & \\

	\hline 	
     $\begin{block}
    	 \ffun
     \end{block} $ & \checkedfalse &  & \\
	
	\hline 	
     $\begin{block}
    	 \finj
     \end{block} $ & \checkedfalse &  & \\



    \hline
    RefName & \checkedtrue  & \checkedtrue & \checkedtrue\\ 

    \hline
    NumberExpression & \checkedtrue  & \checkedtrue & \checkedtrue\\ 

    \hline
    SetExpression & \checkedtrue  & \checkedtrue & \checkedtrue\\ 		

    \hline 	  	 	
\end{tabular}


\section{Z Elements which does not have corresponding elements in Bol}

\begin{itemize}
	\item SymDiff
	\item Mapsto
	\item Ffun
	\item Extract
	\item Filter
	\item Definite Description
	\item Binding Construction
	\item Unique Existential Quantification
	\item Tuple Selection
	\item Schema Projection
	\item Schema Hiding
	\item Schema Piping
	\item Schema Composition
	\item Schema Piping
	\item Schema Precondition
\end{itemize}


\section{Changes in Bol grammar}

\begin{enumerate}
	\item  add PredicateExpression
\end{enumerate}


\section{Obs}


\end{document}