commit by user andrea

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index 6598df5c14a13dede5438c154a5f2b398e853a7f..5da976a523cbfd08ef18f9967a1a871d488e8b9e 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -23,7 +23,8 @@ computational mechanism based on the declaration of inductive types.
 Let us start this tutorial with a simple example based on the following well 
 known problem.
 
-\ 5h2 class="section"\ 6The goat, the wolf and the cabbage\ 5/h2\ 6A farmer need to transfer a goat, a wolf and a cabbage across a river, but there
+\ 5h2 class="section"\ 6The goat, the wolf and the cabbage\ 5/h2\ 6
+A farmer need to transfer a goat, a wolf and a cabbage across a river, but there
 is only one place available on his boat. Furthermore, the goat will eat the 
 cabbage if they are left alone on the same bank, and similarly the wolf will eat
 the goat. The problem consists in bringing all three items safely across the 
@@ -211,11 +212,8 @@ of a relation (a binary predicate) over states. *)
 
 inductive move : \ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"\ 6state\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"\ 6state\ 5/a\ 6 → Prop ≝
 | move_goat: ∀g,g1,w,c. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 g g1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c g) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g1 w c g1)
-         (* Every time g and g1 are two opposite banks, it is legal to put
-                the state "\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c g", which says that goat and boat are on the same bank g,
-            and the state "\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g1 w c g1", which says that goat and boat are on the same bank g1
-            in the relation "move" because, for example, moving the goat from bank g to bank g1 requires
-            moving the boat as well. *) 
+  (* We can move the goat from a bank g to the opposite bank g1 if and only if the
+     boat is on the same bank g of the goat and we move the boat along with it. *)
 | move_wolf: ∀g,w,w1,c. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 w w1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c w) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w1 c w1)
 | move_cabbage: ∀g,w,c,c1.\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 c c1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c c) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c1 c1)
 | move_boat: ∀g,w,c,b,b1. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 b b1 → move (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c b) (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c b1).