1.1 --- a/tex/theory1_ex8.tex Wed Jul 13 01:26:19 2011 +0200
1.2 +++ b/tex/theory1_ex8.tex Wed Jul 13 14:58:35 2011 +0200
1.3 @@ -21,19 +21,43 @@
1.4 \section*{Exercise 8.1}
1.5 Let $s, t \in T(\Sigma, X)$ be terms over $X$ and $p, q$ be strings over the natural numbers. We provide proofs by induction.
1.6 \subsection*{1. $pq \in \Pos(s) \implies p \in \Pos(s)$ }
1.7 -$(IH): pq \in \Pos(s) \implies p \in \Pos(s)$\\\\
1.8 +$(IH): pq \in \Pos(t_i) \implies p \in \Pos(t_i)$ for all $0 < i \leq n$\\\\
1.9 \emph{Base case:}\\
1.10 From $s \in X$ or $s \in \Sigma^{(0)}$ follows $\Pos(s) = \{\epsilon\}$.\\
1.11 -Trivially it follows that $pq \in \Pos(s) \iff pq = \epsilon$ and $pq \in \Pos(s) \implies p \in \Pos(s)$ with $pq \notin \Pos(s) \lor pq = p = \epsilon$. \\
1.12 +Trivially it follows that $pq \in \Pos(s) \iff pq = \epsilon$ and $pq \in \Pos(s) \implies p \in \Pos(s)$ with $pq \notin \Pos(s)$ or $pq = p = \epsilon$. \\
1.13
1.14 \noindent \emph{Inductive case:}\\
1.15 Let $s = f(t_1, ...,t_n) \in T(\Sigma, X)$ it follows $\Pos(s) = \{\epsilon\} \cup \bigcup_{i = 1}^{n}\{ip \mid p \in \Pos(t_i)\}$.\\
1.16 \begin{align*}
1.17 pq \in \Pos(s) &\implies p \in \Pos(s)\\
1.18 -\iff pq \in \{\epsilon\} \cup \bigcup_{i = 1}^{n}\{ip \mid p \in \Pos(t_i)\} &\implies p \in \{\epsilon\} \cup \bigcup_{i = 1}^{n}\{ip \mid p \in \Pos(t_i)\}\\
1.19 +\iff pqr \in \Pos(f(t_1,...,t_n)) &\implies pr \in \Pos(f(t_1,...,t_n))\\
1.20 +\iff pqr \in \{\epsilon\} \cup \bigcup_{i = 1}^{n}\{im \mid m \in \Pos(t_i)\} &\implies pq \in \{\epsilon\} \cup \bigcup_{i = 1}^{n}\{im \mid m \in \Pos(t_i)\}\\
1.21 \end{align*}
1.22 +By (IH) we know that $qr \in \Pos(t_i) \implies r \in \Pos(t_i)$ for all $i \leq n$ and by the left concatenation of $p$ for $0 < p \leq n$ it holds that $pqr \in \Pos(f(t_1,...,t_n)) \implies pq \in \Pos(f(t_1,...,t_n))$. \\ \qed
1.23 +
1.24 +\subsection*{2. $pq \in \Pos(s) \implies s|_{pq} = (s|_p)|_q$ }
1.25 +$(IH): pq \in \Pos(t_i) \implies t_i|_{pq} = (t_i|_p)|_q$ for all $0 < i \leq n$\\\\
1.26 +\emph{Base case:}\\
1.27 +From $s \in X$ or $s \in \Sigma^{(0)}$ follows $\Pos(s) = \{\epsilon\}$.\\
1.28 +Trivially it follows that $pq \in \Pos(s) \iff pq = q = \epsilon$ and $pq \in \Pos(s) \implies s|_{pq} = (s|_p)|_q$ with $pq \notin \Pos(s)$ or $pq = p = \epsilon$ with $s_{pq} = s = s|_p = (s|_p)|_q$.\\
1.29 +
1.30 +\noindent \emph{Inductive case:}\\
1.31 +Let $s = f(t_1, ...,t_n) \in T(\Sigma, X)$ it follows $\Pos(s) = \{\epsilon\} \cup \bigcup_{i = 1}^{n}\{ip \mid p \in \Pos(t_i)\}$.\\
1.32 +By definition we know $f(t_1, ...,t_n)|_{pqr} = t_p|_{qr}$ and from $(IH)$ it follows that $t_p|_{qr} = (t_p|_q)|_r$. \\ \qed
1.33 +
1.34 +\subsection*{3. $p \in \Pos(s) \land q \in \Pos(t) \implies (s[t]_p)|_{pq} = t|_q$ }
1.35 +$(IH): p \in \Pos(t_i) \land q \in \Pos(k_j) \implies (t_i[k_j]_p)|_{pq} = k_j|_q$ for all $0 < i \leq n, 0 < j \leq m$\\\\
1.36 +\emph{Base case:}\\
1.37 +From $s,t \in X$ or $s,t \in \Sigma^{(0)}$ follows $\Pos(s) = \Pos(t) = \{\epsilon\}$.\\
1.38 +Trivially it follows that $p \in \Pos(s) \land q \in \Pos(t) \iff p = q = \epsilon$ and $p \in \Pos(s) \land q \in \Pos(t) \implies (s[t]_p)|_{pq} = t|_q$ with $p \notin \Pos(s) \lor q \notin \Pos(t)$ or $p = q = \epsilon$ with $s[t]_p = (s[t]_p)|_{pq} = t|_q = \epsilon$.\\
1.39 +
1.40 +\noindent \emph{Inductive case:}\\
1.41 +Let $s = f(t_1, ...,t_n), t = g(k_1, ...,k_m) \in T(\Sigma, X)$.\\
1.42 +By definition we know that $f(t_1, ...,t_n)[g(k_1, ...,k_m)]_{p} = f(t_1, ...t_p[g(k_1, ...,k_m)]_\epsilon, ..t_n) = f(t_1, ...g(k_1, ...,k_m), ..t_n)$ and from $(IH)$ follows that $f(t_1, ...g(k_1, ...,k_m), ..t_n)|_{pq} = g(k_1, ...,k_m)|_q = k_q = t|_q$. \\ \qed
1.43
1.44 \section*{Exercise 8.2}
1.45 +We use symbols $\top, \bot$ for $T, F$ respectively.
1.46 +
1.47 \subsection*{1. $t = \neg (x \land (\top \lor y)), \sigma = \{x \mapsto \bot, y \mapsto \top \land x\}, \tau = \{z \mapsto \top, x \mapsto \top\}$}
1.48 \begin{align*}
1.49 \sigma(t) &= \neg (\bot \land (\top \lor ( \top \land x)))\\