From: matitaweb Date: Mon, 3 Oct 2011 11:04:53 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2245 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8adcc68861bcd71f5c2ec3df437e5d492902a061;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index 1d9359bb6..161cd325c 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -204,8 +204,8 @@ applicative nodes). In this case, there is a solution in six moves, and we need a few more applications to handle reachability, and side conditions. The magic number to let automation work is, in this case, 9. *) -(* lemma problem: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a. -normalize /9/ qed. *) +lemma problem: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a. +normalize /9/ qed. (* Let us now try to derive the proof in a more interactive way. Of course, we expect to need several moves to transfer all items from a bank to the other, so @@ -348,7 +348,7 @@ cases b // qed. (* Let's do now an important remark. Comment both problem and problem1, state another time the problem of the goat, the -wolf and the cabbage, and try again to run automation at level /9/. *) +wolf and the cabbage, and try again to run automation at level /9/. lemma problem_bis: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a. -normalize /9/ \ No newline at end of file +normalize /9/ qed. *) \ No newline at end of file