Difference between revisions of "Induction proof"
From Event-B
Jump to navigationJump to searchimported>Christophe |
imported>Mathieu m (ortho) |
||
(5 intermediate revisions by 2 users not shown) | |||
Line 1: | Line 1: | ||
− | This page explains how to | + | This page explains how to prove with [[wikipedia:Mathematical induction|induction]] method on the natural number with Rodin tools. |
− | In other words, how to | + | In other words, how to prove : |
+ | |||
<math> | <math> | ||
P(0) | P(0) | ||
Line 10: | Line 11: | ||
\vdash | \vdash | ||
</math><br/> | </math><br/> | ||
− | <math>\forall i. i \in \mathbb{N} \Rightarrow P(i | + | <math>\forall i. i \in \mathbb{N} \Rightarrow P(i)</math> |
---- | ---- | ||
− | The proof key is the following theorem: | + | The proof key is the following theorem: |
+ | |||
<math> | <math> | ||
− | \forall s.s \subseteq \mathbb{N} \land 0 \in s \land (\forall n.n \in s | + | \forall s.s \subseteq \mathbb{N} \land 0 \in s \land (\forall n.n \in s \Rightarrow n+1 \in s)\Rightarrow \mathbb{N} \subseteq s |
</math> | </math> | ||
---- | ---- | ||
− | The proof of the previous theorem is given by | + | The proof of the previous theorem is given by instantiating the key theorem with : <math> \{x|x\in \mathbb{N} \land P(x)\}</math> |
+ | |||
+ | [[Category:Proof patterns]] |
Latest revision as of 14:11, 30 October 2008
This page explains how to prove with induction method on the natural number with Rodin tools. In other words, how to prove :
The proof key is the following theorem:
The proof of the previous theorem is given by instantiating the key theorem with :