latexandmore/Vorlesungen/ThProg/Strukturelle_Induktion.tex
Sheppy 8752cdd412 finalized Pumping Lemma
changed titlelayout and pagebreaks in multiple documents
2015-10-08 10:45:48 +02:00

52 lines
1.9 KiB
TeX

\documentclass{article}
\usepackage{amsmath}
\usepackage{nccmath}
\DeclareMathSizes{10}{10}{10}{10}
\setlength{\parindent}{0pt}
\title{Strukturelle Induktion}
\date{ }
\begin{document}
\section*{Strukturelle Induktion}
%\maketitle
%----------------------------------%
\textbf{Referenzaufgabe:} \\
\\
\textbf{data List} a = $Nil$ $|$ $Cons$ a \textbf{List} a
\begin{align*}
snoc\;Nil\;a &= Cons\;a\;Nil\\
snoc(Cons\;x\;xs)\;a &= Cons\;x\;(snoc\;xs\;a)
\end{align*}
\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 (IA):}\\\\
$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*}
\textbf{Induktionshypothese/-voraussetzeung (IH/IV):}\\\\
- $xs$ durch allgemeines as ersetzen
\[as+(Cons\;e\;ys) = (snoc\;as\;e)+ys\]
\newpage
\textbf{Induktionsschritt (IS):}\\\\
$as\;=\;Cons\;a\;as$\\$\Rightarrow$ Einsetzen und wieder beide Seiten maximal vereinfachen,auf einer Seite die Induktionshypothese reinfrikeln (idR. nur auf einer Seite,z.B. auf der linken)
\begin{align*}
Cons\;a\;as\;+(Cons\;e\;ys)\;&=\;snoc\;((Cons\;a\;as)\;e)+ys \\
Cons\;a\;(\underbrace{as\;+(Cons\;e\;ys)}_{IH\;links})\;&=\;snoc\;((Cons\;a\;as)\;e)+ys\\
Cons\;a\;(\underbrace{(snoc\;as\;e)\;+\;ys)}_{IH\;rechts})\;&=\;snoc\;((Cons\;a\;as)\;e)+ys\\
Cons\;a\;((snoc\;as\;e)\;+\;ys))\;&=\;Cons\;a\;((\;snoc\;as\;e)\;+\;ys))
\end{align*}\\
\textbf{Q.E.D. und fertig!}\\
\\\\
\begin{tiny}
\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
\end{tiny}
\end{document}