From 4cfd39d4bae224eb6f6391c7423f8ee722f7f00b Mon Sep 17 00:00:00 2001 From: matitaweb Date: Thu, 13 Oct 2011 15:46:31 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter2.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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. -- 2.39.2