Keine Lust.
1 \documentclass[a4paper, 10pt, pagesize, smallheadings]{article}
3 %\usepackage[latin1]{inputenc}
4 \usepackage{amsmath, amsthm, amssymb}
7 \usepackage{algorithmic}
11 \title{Theory I, Sheet 10 Solution}
13 \renewcommand{\familydefault}{\sfdefault}
14 \newcommand{\Pos}{\mathcal{P}os}
15 \newcommand{\E}{\mathcal{E}}
16 \newcommand{\D}{\mathcal{D}}
17 \newcommand{\J}{\mathcal{J}}
18 \include{pythonlisting}
24 \section*{Exercise 10.1}
25 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$:
29 &f(x,x)|_1 = \sigma(x)\\
30 &f(x,x)[\sigma(f(f(x,y), x))]_1 = f(f(f(x,y), x), x)\\
31 \implies &f(x,x) \longrightarrow_\E f(f(f(x,y), x), x)\\
32 &\sigma = \{z \mapsto x\}\\
33 &f(f(f(x,y), x), x)|_1 = \sigma(f(f(x,y), z))\\
34 &f(f(f(x,y), x), x)[\sigma(f(x, f(y,z)))]_1 = f(f(x, f(y,x)), x)\\
35 \implies &f(f(f(x,y), x), x) \longrightarrow_\E f(f(x, f(y,x)), x)\\
36 &\sigma = \{y \mapsto f(y,x)\}\\
37 &f(f(x, f(y,x)), x)|_\epsilon = \sigma(f(f(x,y), x))\\
38 &f(f(x, f(y,x)), x)[\sigma(x)]_\epsilon = x\\
39 \implies &f(f(x, f(y,x)), x) \longrightarrow_\E x\\
42 \section*{Exercise 10.2}
43 \[\{f(x,y) =^? f(h(a), x)\} \xRightarrow{DEC} \{x =^? h(a), y =^? x\} \xRightarrow{ELIM} \{x =^? h(a), y =^? h(a) \}\]
44 \[\overrightarrow{S} = \{x =^? h(a), y =^? h(a) \} \text{ is a solution.}\]\\
45 \[\{f(x,y) =^? f(h(x), x)\} \xRightarrow{DEC} \{x =^? h(x), y =^? x\}\]
46 \[\text{ Occurs check fails, there is no solution.}\]\\
47 \[\{f(x,b) =^? f(h(y),z)\} \xRightarrow{DEC} \{x=^?h(y), b=^?z\} \xRightarrow{ORIENT} \{x=^?h(y), z=^?b\}\]
48 \[\overrightarrow{S} = \{x=^?h(y), z=^?b\} \text{ is a solution.}\]\\
49 \[\{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)\}\]
50 \[\text{ Occurs check fails, there is no solution.}\]\\