+normalize /\ 5span class="autotactic"\ 69\ 5span class="autotrace"\ 6 trace one, more, with_boat, opposite_side, move_goat, move_wolf, move_cabbage, move_boat, east_west, west_east\ 5/span\ 6\ 5/span\ 6/ qed.
+
+(*
+\ 5h2 class="section"\ 6Application\ 5/h2\ 6
+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
+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
+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: reachable start end.
+normalize @more
+
+(*
+\ 5h2 class="section"\ 6Focusing\ 5/h2\ 6
+After performing the previous application, we have four open subgoals:
+
+ X : STATE
+ Y : reachable [east,east,east,east] X
+ W : safe_state X
+ Z : move X [west,west,west,west]
+
+That is, we must guess a state X, such that this is reachable from start, it is
+safe, and there is a move leading from X to end. All goals are active, that is
+emphasized by the fact that they are all red. Any command typed by the user is
+normally applied in parallel to all active goals, but clearly we must proceed
+here is a different way for each of them. The way to do it, is by structuring
+the script using the following syntax: [...|... |...|...] where we typically have
+as many cells inside the brackets as the number of the active subgoals. The
+interesting point is that we can associate with the three symbol "[", "|" and
+"]" a small-step semantics that allow to execute them individually. In particular
+
+- the operator "[" opens a new focusing section for the currently active goals,
+ and focus on the first of them
+- the operator "|" shift the focus to the next goal
+- the operator "]" close the focusing section, falling back to the previous level
+ and adding to it all remaining goals not yet closed
+
+Let us see the effect of the "[" on our proof:
+*)