Fix to formal spec in T11

Tutorials/T11-FinalReview/document.tex

@@ -8,12 +8,25 @@
 \newcommand\tab[1][0.8cm]{\hspace*{#1}}
 
 \begin{document}
-     \begin{eqnarray*}
-	\lefteqn{\forall (i, j: \mathbb{N} | 0 \leq i < SIZE \wedge 0 \leq j < SIZE :}\\
-	&& \exists(k, l: \mathbb{N} | 0 \leq k < SIZE \wedge 0 \leq l < SIZE \wedge (k \neq i \wedge l \neq j) : \\
-	&& \tab \exists(m, n: \mathbb{N} | 0 \leq m < SIZE \wedge 0 \leq n < SIZE 
-	\wedge (m \neq k \wedge n \neq j) \\
-	&& \tab \wedge  i - k  = -( i - m) \wedge  j - l  = -( j - n) ) : \\
-	&& \tab \tab board[i][j] = board[k][l] = board[m][n] )
-\end{eqnarray*}
+\noindent
+$\forall (i, j: \mathbb{N} ~|~ 0 \leq i < SIZE \wedge 0 \leq j < SIZE : \newline
+ ~\qquad \mbox{checkHoriz}(i, j) \lor \mbox{checkVert}(i, j) \lor \mbox{checkDiag}(i, j))$\\
+
+\noindent{\bf local functions}\\
+checkHoriz: $\mathbb{N} \times \mathbb{N} \rightarrow \mathbb{B}$\\
+$\mbox{checkHoriz}(i, j) \equiv (\newline
+~\qquad i + 2 \geq SIZE \Rightarrow \mbox{false} ~|\newline
+~\qquad \mbox{true} \Rightarrow board[i][j] = board[i+1][j] \land board[i][j] = board[i+2][j] \newline
+)$\\[\baselineskip]
+checkHoriz: $\mathbb{N} \times \mathbb{N} \rightarrow \mathbb{B}$\\
+$\mbox{checkHoriz}(i, j) \equiv (\newline
+~\qquad j + 2 \geq SIZE \Rightarrow \mbox{false} ~|\newline
+~\qquad \mbox{true} \Rightarrow board[i][j] = board[i][j+1] \land board[i][j] = board[i][j+2] \newline
+)$\\[\baselineskip]
+checkDiag: $\mathbb{N} \times \mathbb{N} \rightarrow \mathbb{B}$\\
+$\mbox{checkHoriz}(i, j) \equiv (\newline
+~\qquad i + 2 \geq SIZE \Rightarrow \mbox{false} ~|\newline
+~\qquad j + 2 \geq SIZE \Rightarrow \mbox{false} ~|\newline
+~\qquad \mbox{true} \Rightarrow board[i][j] = board[i+1][j+1] \land board[i][j] = board[i+2][j+2] \newline
+)$
 \end{document}
\ No newline at end of file