From: matitaweb Date: Thu, 13 Oct 2011 15:46:31 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2191 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4cfd39d4bae224eb6f6391c7423f8ee722f7f00b;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index b81ecb07c..29979affd 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -30,8 +30,8 @@ match n with (* It is worth to observe that the previous algorithm works by recursion over the first argument. This means that, for instance, (add O x) will reduce to x, as expected, but (add x O) -is stack. How can we prove that, for a generic x, (add x O) = x? The mathematical tool do it is -called induction. The induction principle states that, given a property P(n) over natural +is stack. How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do it +is called induction. The induction principle states that, given a property P(n) over natural numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), than we can conclude P(n) for any n.