Skip to content
Snippets Groups Projects
Commit ce87116e authored by Philip Kaluđerčić's avatar Philip Kaluđerčić :u7121:
Browse files

Indicate that Kleene's theorem involves induction

parent 7529edb3
No related branches found
No related tags found
No related merge requests found
...@@ -36,7 +36,7 @@ ...@@ -36,7 +36,7 @@
&& \bot &\sqsubseteq x\\ && \bot &\sqsubseteq x\\
\implies && \phi(\bot) &\sqsubseteq \phi(x) = x \tag{\(\phi\) is \defn{monotone}{mono.}}\\ \implies && \phi(\bot) &\sqsubseteq \phi(x) = x \tag{\(\phi\) is \defn{monotone}{mono.}}\\
\implies && \phi^2(\bot) &\sqsubseteq \phi^2(x) = \phi(x) = x\\ \implies && \phi^2(\bot) &\sqsubseteq \phi^2(x) = \phi(x) = x\\
&&&\;\;\vdots\\ &&&\;\;\vdots \; \tag{i.e.\ induction}\\
% \implies && \phi^n(\bot) &\sqsubseteq \phi^n(x) = \dots = x\\ % \implies && \phi^n(\bot) &\sqsubseteq \phi^n(x) = \dots = x\\
% &&&\;\;\vdots\\ % &&&\;\;\vdots\\
\implies && \underline{\mu\phi} = \bigsqcup_{i = 0}^\infty \phi^i(\bot) &\sqsubseteq \bigsqcup_{i = 0}^\infty \phi^i(x) = \underline{x} \implies && \underline{\mu\phi} = \bigsqcup_{i = 0}^\infty \phi^i(\bot) &\sqsubseteq \bigsqcup_{i = 0}^\infty \phi^i(x) = \underline{x}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment