From 8adcc68861bcd71f5c2ec3df437e5d492902a061 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 3 Oct 2011 11:04:53 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter1.ma | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 -- 2.39.2