commit by user andrea

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

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index b21fd3e1787add792e06acdb24dbf62c14dba2b0..9043bdad712795d8f6f76104e72d4dc6601a3455 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -243,7 +243,7 @@ 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.
-normalize /9/ 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. 
 
 (* 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 
@@ -304,7 +304,7 @@ requires /2/ since move_goat opens an additional subgoal. By applying "]" we
 refocus on the skipped goal, going back to a situation similar to the one we
 started with. *)
 
-  | /2/ ] 
+  | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ ] 
 
 (* Let us perform the next step, namely moving back the boat, in a sligtly 
 different way. The more operation expects as second argument the new 
@@ -319,7 +319,7 @@ the system. *)
 trivial. We\ 5span style="font-family: Verdana,sans-serif;"\ 6 \ 5/span\ 6can just apply automation to all of them, and it will close the two
 trivial goals. *)
 
-/2/
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 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,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/
 
 (* Let us come to the next step, that consists in moving the wolf. Suppose that 
 instead of specifying the next intermediate state, we prefer to specify the next 
@@ -338,12 +338,12 @@ be arbitrary). The simplest way to proceed is to focus on the bank, that is
 the fourth subgoal, and explicitly instatiate it. Instead of repeatedly using "|",
 we can perform focusing by typing "4:" as described by the following command. *)
 
-[4: @\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6] /2/
+[4: @\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6] /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"\ 6with_boat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 
 (* Alternatively, we can directly instantiate the bank into the move. Let
 us complete the proof in this, very readable way. *)
 
-@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 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/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /2/
-@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 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/bank.con(0,1,0)"\ 6east\ 5/a\ 6 … )) /2/
-@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 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/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /2/
-@\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6 /2/ qed.
\ No newline at end of file
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 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/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"\ 6with_boat\ 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/
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 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/bank.con(0,1,0)"\ 6east\ 5/a\ 6 … )) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"\ 6opposite_side\ 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/
+@(\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"\ 6more\ 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/bank.con(0,2,0)"\ 6west\ 5/a\ 6 … )) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"\ 6with_boat\ 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/
+@\ 5a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"\ 6one\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"\ 6move_goat\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"\ 6east_west\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
\ No newline at end of file