1.1 --- a/tex/theory1_ex9.tex	Mon Jul 18 20:17:25 2011 +0200
     1.2 +++ b/tex/theory1_ex9.tex	Tue Jul 19 00:24:38 2011 +0200
     1.3 @@ -23,14 +23,16 @@
     1.4  
     1.5  \section*{Exercise 9.1.3}
     1.6  \begin{align*}
     1.7 -ADT_{bool} = &(\Sigma_{bool}, \E)\\
     1.8 +ADT\, bool = &(\Sigma_{bool}, \E)\\
     1.9  \Sigma_{bool} = &\{true^{(0)}, false^{(0)}, not^{(1)}, and^{(2)}, or^{(2)}\}\\
    1.10  \E = &\{true \approx not(false),\\
    1.11 -& false \approx not(true),\\
    1.12 -& not(not(x)) \approx x\\
    1.13 -& and(x, y) \approx not(or(not(x), not(y))),\\
    1.14 -& or(x, y) \approx not(and(not(x), not(y)))\}\\
    1.15 +& not(not(x)) \approx x,\\
    1.16 +& or(x, false) \approx x,\\
    1.17 +& or(x, true) \approx true,\\
    1.18 +& and(x, y) \approx not(or(not(x), not(y)))\}\\
    1.19  \end{align*}
    1.20 +Remarks: $false \approx not(true)$ follows from $true \approx not(false)$ and $not(not(x)) \approx x$.\\
    1.21 +$or(x, y) \approx not(and(not(x), not(y)))$ follows from $not(not(x)) \approx x$ and $and(x, y) \approx not(or(not(x), not(y)))$.
    1.22  
    1.23  \section*{Exercise 9.1.4}
    1.24  \begin{align*}
    1.25 @@ -43,4 +45,21 @@
    1.26  \J(or)(x, y) &= max(x, y)\\
    1.27  \end{align*}
    1.28  
    1.29 +\section*{Exercise 9.2}
    1.30 +\begin{align*}
    1.31 +ADT\, Stack = &(\Sigma_{Stack}, \E)\\
    1.32 +\Sigma_{Stack} = &\{new^{(0)}, true^{(0)}, false^{(0)}, pop^{(1)}, top^{(1)}, isEmpty^{(1)}, push^{(2)}\}\\
    1.33 +& new: Stack\\
    1.34 +& true: bool\\
    1.35 +& false: bool\\
    1.36 +& pop: Stack \to Stack\\
    1.37 +& top: Stack \to A\\
    1.38 +& isEmpty: Stack \to bool\\
    1.39 +& push: Stack \times A \to Stack\\
    1.40 +\E = &\{isEmpty(new) \approx true,\\
    1.41 +& isEmpty(push(S, x)) \approx false,\\
    1.42 +& top(push(S, x)) \approx x,\\
    1.43 +& pop(push(S, x)) \approx S\}\\
    1.44 +\end{align*}
    1.45 +The ADT $Stack$ has only one constructor $new$.
    1.46  \end{document}