\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 10 Solution}

 \author{Eugen Sawin}

 \renewcommand{\familydefault}{\sfdefault}

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

 \newcommand{\E}{\mathcal{E}}

 \newcommand{\D}{\mathcal{D}}

 \newcommand{\J}{\mathcal{J}}

 \include{pythonlisting}

 \pagestyle{empty}

 \begin{document}

 \maketitle

 \section*{Exercise 10.1}

 Let $\E = \{f(x, f(y,z)) = f(f(x,y), z), f(f(x,y), x) = x\}$, we show $f(x,x) \longrightarrow^*_\E x$:

 \begin{align*}

 &f(x,x)\\

 &\sigma = \{\}\\

 &f(x,x)|_1 = \sigma(x)\\

 &f(x,x)[\sigma(f(f(x,y), x))]_1 = f(f(f(x,y), x), x)\\

 \implies &f(x,x) \longrightarrow_\E f(f(f(x,y), x), x)\\

 &\sigma = \{z \mapsto x\}\\

 &f(f(f(x,y), x), x)|_1 = \sigma(f(f(x,y), z))\\

 &f(f(f(x,y), x), x)[\sigma(f(x, f(y,z)))]_1 = f(f(x, f(y,x)), x)\\

 \implies &f(f(f(x,y), x), x) \longrightarrow_\E f(f(x, f(y,x)), x)\\

 &\sigma = \{y \mapsto f(y,x)\}\\

 &f(f(x, f(y,x)), x)|_\epsilon = \sigma(f(f(x,y), x))\\

 &f(f(x, f(y,x)), x)[\sigma(x)]_\epsilon = x\\

 \implies &f(f(x, f(y,x)), x) \longrightarrow_\E x\\

 \end{align*}

 \section*{Exercise 10.2}

 \[\{f(x,y) =^? f(h(a), x)\} \xRightarrow{DEC} \{x =^? h(a), y =^? x\} \xRightarrow{ELIM} \{x =^? h(a), y =^? h(a) \}\]

 \[\overrightarrow{S} = \{x =^? h(a), y =^? h(a) \} \text{ is a solution.}\]\\

 \[\{f(x,y) =^? f(h(x), x)\} \xRightarrow{DEC} \{x =^? h(x), y =^? x\}\]

 \[\text{ Occurs check fails, there is no solution.}\]\\

 \[\{f(x,b) =^? f(h(y),z)\} \xRightarrow{DEC} \{x=^?h(y), b=^?z\} \xRightarrow{ORIENT} \{x=^?h(y), z=^?b\}\]

 \[\overrightarrow{S} = \{x=^?h(y), z=^?b\} \text{ is a solution.}\]\\

 \[\{f(x,x)=^?f(h(y),y)\} \xRightarrow{DEC} \{x=^?h(y),x=^?y\} \xRightarrow{ELIM} \{x=^?h(y), h(y)=^?y\} \xRightarrow{ORIENT} \{x=^?h(y), y=^?h(y)\}\]

 \[\text{ Occurs check fails, there is no solution.}\]\\

 \end{document}