\documentclass[a4paper, 10pt, pagesize, smallheadings]{article}  

\usepackage{graphicx}

%\usepackage[latin1]{inputenc}

\usepackage{amsmath, amsthm, amssymb}

\usepackage{typearea}

\usepackage{algorithm}

\usepackage{algorithmic}

\usepackage{fullpage}

\usepackage{mathtools}

\usepackage[all]{xy}

\title{Theory I, Sheet 8 Solution}

\author{Eugen Sawin}

\renewcommand{\familydefault}{\sfdefault}

\newcommand{\Pos}{\mathcal{P}os}

\include{pythonlisting}

\pagestyle{empty}

\begin{document}

\maketitle

\section*{Exercise 8.1}

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.

\subsection*{1. $pq \in \Pos(s) \implies p \in \Pos(s)$ }

$(IH): pq \in \Pos(s) \implies p \in \Pos(s)$\\\\

\emph{Base case:}\\

From $s \in X$ or $s \in \Sigma^{(0)}$ follows $\Pos(s) = \{\epsilon\}$.\\

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$. \\ 

\noindent \emph{Inductive case:}\\

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)\}$.\\

\begin{align*}

pq \in \Pos(s) &\implies p \in \Pos(s)\\ 

\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)\}\\

\end{align*}

\section*{Exercise 8.2}

\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\}$}

\begin{align*}

\sigma(t) &= \neg (\bot \land (\top \lor ( \top \land x)))\\

\tau \sigma(t) &= \tau(\neg (\bot \land (\top \lor ( \top \land x)))) = \neg (\bot \land (\top \lor (\top \land \top)))\\

\end{align*}

\subsection*{2. $t = \neg(\top \land (\bot \lor y)), s = \neg(x \land (\bot \lor (x \land \bot)))$}

\[\sigma(t) = \sigma(s) \text{ with } \sigma = \{x \mapsto \top, y \mapsto \top \land \bot \} \]

\subsection*{3.}

Substitution composition is \emph{not} commutative, we give a counterexample.

Let $t = x$, $\sigma = \{x \mapsto \bot\}$ and $\tau = \{x \mapsto \top\}$, it follows:

\[\tau\sigma(t) = \bot\]

\[\sigma\tau(t) = \top\]

We see that $\tau\sigma(t) \neq \sigma\tau(t)$.

\end{document}