2015-10-06 16:49:42 +02:00
|
|
|
\documentclass{article}
|
|
|
|
\usepackage{amsmath}
|
|
|
|
\usepackage{nccmath}
|
|
|
|
\DeclareMathSizes{10}{10}{10}{10}
|
|
|
|
\setlength{\parindent}{0pt}
|
|
|
|
\title{Konfluenz}
|
|
|
|
\date{ }
|
|
|
|
\begin{document}
|
|
|
|
\maketitle
|
2015-10-07 14:02:58 +02:00
|
|
|
%----------------------------------%
|
|
|
|
\textbf{Referenzaufgabe:} \\
|
2015-10-06 16:49:42 +02:00
|
|
|
\\
|
2015-10-07 14:02:58 +02:00
|
|
|
\textbf{data List} a = $Nil$ $|$ $Cons$ a \textbf{List} a
|
2015-10-06 16:49:42 +02:00
|
|
|
\begin{align*}
|
2015-10-07 14:02:58 +02:00
|
|
|
snoc\;Nil\;a &= Cons\;a\;Nil\\
|
|
|
|
snoc(Cons\;x\;xs)\;a &= Cons\;x\;(snoc\;xs\;a)
|
2015-10-06 16:49:42 +02:00
|
|
|
\end{align*}
|
2015-10-07 14:02:58 +02:00
|
|
|
\begin{align*}
|
|
|
|
Nil + ys &= ys\\
|
|
|
|
(Cons\;x\;xs) + ys &= Cons\;x\;(xs + ys)
|
|
|
|
\end{align*}
|
|
|
|
\underline{Beweisen sie dass:}\\
|
|
|
|
$\forall e,\;xs,\;ys\\xs+(Cons\;e\;ys) = (snoc\;xs\;e)+ys$ \\\\
|
|
|
|
%----------------------------------%
|
|
|
|
\textbf{Induktionsanfang:}\\\\
|
|
|
|
$xs = Nil$\;\;$\Rightarrow$ Einsetzen und beide Seiten maximal vereinfachen
|
|
|
|
\begin{align*}
|
|
|
|
Nil+(Cons\;e\;ys) &= (snoc\;Nil\;e)+ys\\
|
|
|
|
Cons\;e\;ys &= (snoc\;Nil\;e)+ys\\
|
|
|
|
Cons\;e\;ys &= (Cons e Nil) + ys\\
|
|
|
|
Cons\;e\;ys &= Cons\;e (Nil + ys)\\
|
|
|
|
Cons\;e\;ys &= Cons\;e\;ys
|
|
|
|
\end{align*}
|
|
|
|
|
2015-10-06 16:49:42 +02:00
|
|
|
\begin{tiny}
|
|
|
|
\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
|
|
|
|
\end{tiny}
|
|
|
|
\end{document}
|