1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/tex/theory1_ex10.tex	Mon Jul 25 17:53:35 2011 +0200
     1.3 @@ -0,0 +1,51 @@
     1.4 +\documentclass[a4paper, 10pt, pagesize, smallheadings]{article}  
     1.5 +\usepackage{graphicx}
     1.6 +%\usepackage[latin1]{inputenc}
     1.7 +\usepackage{amsmath, amsthm, amssymb}
     1.8 +\usepackage{typearea}
     1.9 +\usepackage{algorithm}
    1.10 +\usepackage{algorithmic}
    1.11 +\usepackage{fullpage}
    1.12 +\usepackage{mathtools}
    1.13 +\usepackage[all]{xy}
    1.14 +\title{Theory I, Sheet 10 Solution}
    1.15 +\author{Eugen Sawin}
    1.16 +\renewcommand{\familydefault}{\sfdefault}
    1.17 +\newcommand{\Pos}{\mathcal{P}os}
    1.18 +\newcommand{\E}{\mathcal{E}}
    1.19 +\newcommand{\D}{\mathcal{D}}
    1.20 +\newcommand{\J}{\mathcal{J}}
    1.21 +\include{pythonlisting}
    1.22 +
    1.23 +\pagestyle{empty}
    1.24 +\begin{document}
    1.25 +\maketitle
    1.26 +
    1.27 +\section*{Exercise 10.1}
    1.28 +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$:
    1.29 +\begin{align*}
    1.30 +&f(x,x)\\
    1.31 +&\sigma = \{\}\\
    1.32 +&f(x,x)|_1 = \sigma(x)\\
    1.33 +&f(x,x)[\sigma(f(f(x,y), x))]_1 = f(f(f(x,y), x), x)\\
    1.34 +\implies &f(x,x) \longrightarrow_\E f(f(f(x,y), x), x)\\
    1.35 +&\sigma = \{z \mapsto x\}\\
    1.36 +&f(f(f(x,y), x), x)|_1 = \sigma(f(f(x,y), z))\\
    1.37 +&f(f(f(x,y), x), x)[\sigma(f(x, f(y,z)))]_1 = f(f(x, f(y,x)), x)\\
    1.38 +\implies &f(f(f(x,y), x), x) \longrightarrow_\E f(f(x, f(y,x)), x)\\
    1.39 +&\sigma = \{y \mapsto f(y,x)\}\\
    1.40 +&f(f(x, f(y,x)), x)|_\epsilon = \sigma(f(f(x,y), x))\\
    1.41 +&f(f(x, f(y,x)), x)[\sigma(x)]_\epsilon = x\\
    1.42 +\implies &f(f(x, f(y,x)), x) \longrightarrow_\E x\\
    1.43 +\end{align*}
    1.44 +
    1.45 +\section*{Exercise 10.2}
    1.46 +\[\{f(x,y) =^? f(h(a), x)\} \xRightarrow{DEC} \{x =^? h(a), y =^? x\} \xRightarrow{ELIM} \{x =^? h(a), y =^? h(a) \}\]
    1.47 +\[\overrightarrow{S} = \{x =^? h(a), y =^? h(a) \} \text{ is a solution.}\]\\
    1.48 +\[\{f(x,y) =^? f(h(x), x)\} \xRightarrow{DEC} \{x =^? h(x), y =^? x\}\]
    1.49 +\[\text{ Occurs check fails, there is no solution.}\]\\
    1.50 +\[\{f(x,b) =^? f(h(y),z)\} \xRightarrow{DEC} \{x=^?h(y), b=^?z\} \xRightarrow{ORIENT} \{x=^?h(y), z=^?b\}\]
    1.51 +\[\overrightarrow{S} = \{x=^?h(y), z=^?b\} \text{ is a solution.}\]\\
    1.52 +\[\{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)\}\]
    1.53 +\[\text{ Occurs check fails, there is no solution.}\]\\
    1.54 +\end{document}