diff --git a/Public/thprog/Strukturelle Induktion.tex b/Public/thprog/Strukturelle Induktion.tex index ee080a4..0ba1a4b 100644 --- a/Public/thprog/Strukturelle Induktion.tex +++ b/Public/thprog/Strukturelle Induktion.tex @@ -3,7 +3,7 @@ \usepackage{nccmath} \DeclareMathSizes{10}{10}{10}{10} \setlength{\parindent}{0pt} - \title{Konfluenz} + \title{Struckturelle Induktion} \date{ } \begin{document} \maketitle @@ -22,7 +22,7 @@ \underline{Beweisen sie dass:}\\ $\forall e,\;xs,\;ys\\xs+(Cons\;e\;ys) = (snoc\;xs\;e)+ys$ \\\\ %----------------------------------% - \textbf{Induktionsanfang:}\\\\ + \textbf{Induktionsanfang (IA):}\\\\ $xs = Nil$\;\;$\Rightarrow$ Einsetzen und beide Seiten maximal vereinfachen \begin{align*} Nil+(Cons\;e\;ys) &= (snoc\;Nil\;e)+ys\\ @@ -31,7 +31,20 @@ 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}