mirror of
https://gitlab.cs.fau.de/ik15ydit/latexandmore.git
synced 2024-11-22 11:49:32 +01:00
Strukturelle Induktion fertig und Titel gefixt
This commit is contained in:
parent
cb01955cc4
commit
2f0ac44482
@ -3,7 +3,7 @@
|
|||||||
\usepackage{nccmath}
|
\usepackage{nccmath}
|
||||||
\DeclareMathSizes{10}{10}{10}{10}
|
\DeclareMathSizes{10}{10}{10}{10}
|
||||||
\setlength{\parindent}{0pt}
|
\setlength{\parindent}{0pt}
|
||||||
\title{Konfluenz}
|
\title{Struckturelle Induktion}
|
||||||
\date{ }
|
\date{ }
|
||||||
\begin{document}
|
\begin{document}
|
||||||
\maketitle
|
\maketitle
|
||||||
@ -22,7 +22,7 @@
|
|||||||
\underline{Beweisen sie dass:}\\
|
\underline{Beweisen sie dass:}\\
|
||||||
$\forall e,\;xs,\;ys\\xs+(Cons\;e\;ys) = (snoc\;xs\;e)+ys$ \\\\
|
$\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
|
$xs = Nil$\;\;$\Rightarrow$ Einsetzen und beide Seiten maximal vereinfachen
|
||||||
\begin{align*}
|
\begin{align*}
|
||||||
Nil+(Cons\;e\;ys) &= (snoc\;Nil\;e)+ys\\
|
Nil+(Cons\;e\;ys) &= (snoc\;Nil\;e)+ys\\
|
||||||
@ -31,7 +31,20 @@
|
|||||||
Cons\;e\;ys &= Cons\;e (Nil + ys)\\
|
Cons\;e\;ys &= Cons\;e (Nil + ys)\\
|
||||||
Cons\;e\;ys &= Cons\;e\;ys
|
Cons\;e\;ys &= Cons\;e\;ys
|
||||||
\end{align*}
|
\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}
|
\begin{tiny}
|
||||||
\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
|
\copyright\ Joint-Troll-Expert-Group (JTEG) 2015
|
||||||
\end{tiny}
|
\end{tiny}
|
||||||
|
Loading…
Reference in New Issue
Block a user