From: matitaweb Date: Thu, 13 Oct 2011 21:09:09 +0000 (+0000) Subject: commit by user enrico X-Git-Tag: make_still_working~2190 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=948676ae86382ebdfd13b7d485da02137cce558d;p=helm.git commit by user enrico --- diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index 29979affd..7a60a7b52 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -94,8 +94,8 @@ definition nat_of_bool ≝ λb. match b with definition twice ≝ λn.a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a n n. -(* We are interested to prove that for any natural number m there exists a natural number m that -is the integer half of m. This will give us the opportunity to introduce new connectives and +(* We are interested to prove that for any natural number n there exists a natural number m that +is the integer half of n. This will give us the opportunity to introduce new connectives and quantifiers and, later on, to make some interesting consideration on proofs and computations. *) theorem ex_half: ∀n.a title="exists" href="cic:/fakeuri.def(1)"∃/am. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a m a title="logical or" href="cic:/fakeuri.def(1)"∨/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a m).