From 948676ae86382ebdfd13b7d485da02137cce558d Mon Sep 17 00:00:00 2001 From: matitaweb Date: Thu, 13 Oct 2011 21:09:09 +0000 Subject: [PATCH] commit by user enrico --- 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 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). -- 2.39.2