update in staic_2 and basic_2

[helm.git] / weblib / tutorial / chapter1.ma

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index c46004f24d106a7f03eea1812ebc5620ee7d65a9..4cf145d60f53f72c70b08846444700cd9b1afc7e 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -44,14 +44,14 @@ few preliminary notions not worth discussing for the moment.
 
 include "basics/logic.ma".
 
 
 include "basics/logic.ma".
 

-inductive bank: Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="bank"\ 6inductive bank: Type[0] ≝

 | east : bank 
 | west : bank.
 
 (* We can now define a simple function computing, for each bank of the river, the
 opposite one. *)
 
 | east : bank 
 | west : bank.
 
 (* We can now define a simple function computing, for each bank of the river, the
 opposite one. *)
 

-definition opposite ≝ λs.
+\ 5img class="anchor" src="icons/tick.png" id="opposite"\ 6definition opposite ≝ λs.

 match s with
   [ east ⇒ \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6
   | west ⇒ \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6
 match s with
   [ east ⇒ \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6
   | west ⇒ \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6


@@ -61,9 +61,11 @@ match s with
 us state the property that the opposite bank of east is west; every lemma needs a 
 name for further reference, and we call it "east_to_west". *)
  
 us state the property that the opposite bank of east is west; every lemma needs a 
 name for further reference, and we call it "east_to_west". *)
  

-lemma east_to_west : \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="east_to_west"\ 6lemma east_to_west : \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6.

 
 

-(* If you stop the execution here you will see a new window on the  right side
+(* 
+\ 5h2 class="section"\ 6The goal window\ 5/h2\ 6
+If you stop the execution here you will see a new window on the  right side

 of the screen: it is the goal window, providing a sequent like representation of
 the form
 
 of the screen: it is the goal window, providing a sequent like representation of
 the form
 


@@ -100,14 +102,14 @@ lemma performing some book-keeping operations.
 In this case, we avoid the unnecessary simplification step: // will take care of 
 it. *) 
 
 In this case, we avoid the unnecessary simplification step: // will take care of 
 it. *) 
 

-lemma west_to_east : \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="west_to_east"\ 6lemma west_to_east : \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6.

 // qed.
 
 (*
 // qed.
 
 (*

-\ 5h2 class="section"\ 6Case analysis\ 5/h2\ 6
+\ 5h2 class="section"\ 6Introduction\ 5/h2\ 6

 A slightly more complex problem consists in proving that opposite is idempotent *)
 
 A slightly more complex problem consists in proving that opposite is idempotent *)
 

-lemma idempotent_opposite : ∀x. \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 x) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
+\ 5img class="anchor" src="icons/tick.png" id="idempotent_opposite"\ 6lemma idempotent_opposite : ∀x. \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 x) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.

 
 (* we start the proof moving x from the conclusion into the context, that is a 
 (backward) introduction step. Matita syntax for an introduction step is simply 
 
 (* we start the proof moving x from the conclusion into the context, that is a 
 (backward) introduction step. Matita syntax for an introduction step is simply 


@@ -120,7 +122,10 @@ wish to rename x into b (since it is a bank), we just type #b. *)
 (* See the effect of the execution in the goal window on the right: b has been 
 added to the context (replacing x in the conclusion); moreover its implicit type 
 "bank" has been made explicit. 
 (* See the effect of the execution in the goal window on the right: b has been 
 added to the context (replacing x in the conclusion); moreover its implicit type 
 "bank" has been made explicit. 

+*)

 
 

+(*
+\ 5h2 class="section"\ 6Case analysis\ 5/h2\ 6

 But how are we supposed to proceed, now? Simplification cannot help us, since b
 is a variable: just try to call normalize and you will see that it has no effect.
 The point is that we must proceed by cases according to the possible values of b,
 But how are we supposed to proceed, now? Simplification cannot help us, since b
 is a variable: just try to call normalize and you will see that it has no effect.
 The point is that we must proceed by cases according to the possible values of b,


@@ -150,7 +155,7 @@ other. Only two cases are possible, leading naturally to the following
 definition:
 *)
 
 definition:
 *)
 

-inductive opp : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6 → Prop ≝ 
+\ 5img class="anchor" src="icons/tick.png" id="opp"\ 6inductive opp : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6 → Prop ≝ 

 | east_west : opp \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6
 | west_east : opp \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6.
 
 | east_west : opp \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6
 | west_east : opp \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6.
 


@@ -164,7 +169,7 @@ Between opp and opposite we have the following relation:
     opp a b iff a = opposite b
 Let us prove it, starting from the left to right implication, first *)
 
     opp a b iff a = opposite b
 Let us prove it, starting from the left to right implication, first *)
 

-lemma opp_to_opposite: ∀a,b. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 a b → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 b.
+\ 5img class="anchor" src="icons/tick.png" id="opp_to_opposite"\ 6lemma opp_to_opposite: ∀a,b. \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 a b → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 b.

  
 (* We start the proof introducing a, b and the hypothesis opp a b, that we
 call oppab. *)
  
 (* We start the proof introducing a, b and the hypothesis opp a b, that we
 call oppab. *)


@@ -181,7 +186,7 @@ cases oppab // qed.
 \ 5h2 class="section"\ 6Rewriting\ 5/h2\ 6
 Let us come to the opposite direction. *)
 
 \ 5h2 class="section"\ 6Rewriting\ 5/h2\ 6
 Let us come to the opposite direction. *)
 

-lemma opposite_to_opp: ∀a,b. a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 b → \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 a b.
+\ 5img class="anchor" src="icons/tick.png" id="opposite_to_opp"\ 6lemma opposite_to_opp: ∀a,b. a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 b → \ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 a b.

 
 (* As usual, we start introducing a, b and the hypothesis (a = opposite b), 
 that we call eqa. *)
 
 (* As usual, we start introducing a, b and the hypothesis (a = opposite b), 
 that we call eqa. *)


@@ -201,12 +206,12 @@ cases b // qed.
 (*
 \ 5h2 class="section"\ 6Records\ 5/h2\ 6
 It is time to proceed with our formalization of the farmer's problem. 
 (*
 \ 5h2 class="section"\ 6Records\ 5/h2\ 6
 It is time to proceed with our formalization of the farmer's problem. 

-A state of the system is defined by the position of four item: the goat, the 
+A state of the system is defined by the position of four items: the goat, the 

 wolf, the cabbage, and the boat. The simplest way to declare such a data type
 is to use a record.
 *)
 
 wolf, the cabbage, and the boat. The simplest way to declare such a data type
 is to use a record.
 *)
 

-record state : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="state"\ 6record state : Type[0] ≝

   {goat_pos : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6;
    wolf_pos : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6;
    cabbage_pos: \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6;
   {goat_pos : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6;
    wolf_pos : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6;
    cabbage_pos: \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6;


@@ -216,13 +221,13 @@ record state : Type[0] ≝
 constructor named mk_foo. To construct a new record you pass as arguments to 
 mk_foo the values of the record fields *)
 
 constructor named mk_foo. To construct a new record you pass as arguments to 
 mk_foo the values of the record fields *)
 

-definition start ≝ \ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6.
-definition end ≝ \ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="start"\ 6definition start ≝ \ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="end"\ 6definition end ≝ \ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6.

 
 (* We must now define the possible moves. A natural way to do it is in the form 
 of a relation (a binary predicate) over states. *)
 
 
 (* We must now define the possible moves. A natural way to do it is in the form 
 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 ≝
+\ 5img class="anchor" src="icons/tick.png" id="move"\ 6inductive 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)
   (* 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_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)
   (* 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. *)


@@ -233,7 +238,7 @@ inductive move : \ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"\ 6state\ 5
 (* A state is safe if either the goat is on the same bank of the boat, or both 
 the wolf and the cabbage are on the opposite bank of the goat. *)
 
 (* A state is safe if either the goat is on the same bank of the boat, or both 
 the wolf and the cabbage are on the opposite bank of the goat. *)
 

-inductive safe_state : \ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"\ 6state\ 5/a\ 6 → Prop ≝
+\ 5img class="anchor" src="icons/tick.png" id="safe_state"\ 6inductive safe_state : \ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"\ 6state\ 5/a\ 6 → Prop ≝

 | with_boat : ∀g,w,c.safe_state (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c g)
 | opposite_side : ∀g,g1,b.\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 g g1 → safe_state (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g g1 g1 b).
 
 | with_boat : ∀g,w,c.safe_state (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g w c g)
 | opposite_side : ∀g,g1,b.\ 5a href="cic:/matita/tutorial/chapter1/opp.ind(1,0,0)"\ 6opp\ 5/a\ 6 g g1 → safe_state (\ 5a href="cic:/matita/tutorial/chapter1/state.con(0,1,0)"\ 6mk_state\ 5/a\ 6 g g1 g1 b).
 


@@ -241,7 +246,7 @@ inductive safe_state : \ 5a href="cic:/matita/tutorial/chapter1/state.ind(1,0,0)"\ 6
 leading from x to y, or there is a safe state z such that z is reachable from x 
 and there is a move leading from z to y *)
 
 leading from x to y, or there is a safe state z such that z is reachable from x 
 and there is a move leading from z to y *)
 

-inductive reachable : \ 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 ≝
+\ 5img class="anchor" src="icons/tick.png" id="reachable"\ 6inductive reachable : \ 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 ≝

 | one : ∀x,y.\ 5a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"\ 6move\ 5/a\ 6 x y → reachable x y
 | more : ∀x,z,y. \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6reachable x z → \ 5a href="cic:/matita/tutorial/chapter1/safe_state.ind(1,0,0)"\ 6safe_state\ 5/a\ 6 z → \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"\ 6move\ 5/a\ 6 z y → reachable x y.
 
 | one : ∀x,y.\ 5a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"\ 6move\ 5/a\ 6 x y → reachable x y
 | more : ∀x,z,y. \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6reachable x z → \ 5a href="cic:/matita/tutorial/chapter1/safe_state.ind(1,0,0)"\ 6safe_state\ 5/a\ 6 z → \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5a href="cic:/matita/tutorial/chapter1/move.ind(1,0,0)"\ 6move\ 5/a\ 6 z y → reachable x y.
 


@@ -255,7 +260,7 @@ 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.  *)
 
 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: \ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"\ 6reachable\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"\ 6start\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"\ 6end\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="problem"\ 6lemma problem: \ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"\ 6reachable\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"\ 6start\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"\ 6end\ 5/a\ 6.

 normalize /\ 5span class="autotactic"\ 69\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"\ 6with_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"\ 6opposite_side\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,2,0)"\ 6move_wolf\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"\ 6move_cabbage\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"\ 6move_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"\ 6west_east\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
 
 (* 
 normalize /\ 5span class="autotactic"\ 69\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"\ 6with_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"\ 6opposite_side\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,2,0)"\ 6move_wolf\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"\ 6move_cabbage\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"\ 6move_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"\ 6west_east\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
 
 (* 


@@ -265,11 +270,12 @@ expect to need several moves to transfer all items from a bank to the other, so
 we should start our proof by applying "more". Matita syntax for invoking the 
 application of a property named foo is to write "@foo". In general, the philosophy 
 of Matita is to describe each proof of a property P as a structured collection of 
 we should start our proof by applying "more". Matita syntax for invoking the 
 application of a property named foo is to write "@foo". In general, the philosophy 
 of Matita is to describe each proof of a property P as a structured collection of 

-results required for proving P, prefixed by simple modalities (<,@,...) explaining 
-the way the result is used (e.g. for rewriting, in an applicative step, and so on).
+objects involved in the proof, prefixed by simple modalities (#,<,@,...) explaining 
+the way it is actually used (e.g. for introduction, rewriting, in an applicative 
+step, and so on).

 *)
 
 *)
 

-lemma problem1: \ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"\ 6reachable\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"\ 6start\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"\ 6end\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="problem1"\ 6lemma problem1: \ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"\ 6reachable\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"\ 6start\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"\ 6end\ 5/a\ 6.

 normalize @\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6
 
 (* 
 normalize @\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 5/a\ 6
 
 (*