-(*
+(*
+\ 5h1\ 6Matita Interactive Tutorial\ 5/h1\ 6
This is an interactive tutorial. To let you interact on line with the system,
you must first of all register yourself.
previously selected by the user; the bottom button execute the whole script.
That's it: we are\ 5span style="font-family: Verdana,sans-serif;"\ 6 \ 5/span\ 6now ready to start.
-The first thing to say is that in a system like Matita's very few things are
-built-in: not even booleans or logical connectives. The main philosophy of the
-system is to let you define your own data-types and functions using a powerful
-computational mechanism based on the declaration of inductive types.
+\ 5h2 class="section"\ 6Data types, functions and theorems\ 5/h2\ 6
+Matita is both a programming language and a theorem proving environment:
+you define datatypes and programs, and then prove properties on them.
+Very few things are built-in: not even booleans or logical connectives
+(but you may of course use libraries, as in normal programming languages).
+The main philosophy of the system is to let you define your own data-types
+and functions using a powerful 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\ 6\ 5div class="paragraph"\ 6\ 5/div\ 6A farmer need to transfer a goat, a wolf and a cabbage across a river, but there
+\ 5b\ 6The goat, the wolf and the cabbage\ 5/b\ 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
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.
-(* 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
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.
// qed.
-(* A slightly more complex problem consists in proving that opposite is
-idempotent *)
+(*
+\ 5h2 class="section"\ 6Introduction\ 5/h2\ 6
+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.
(* 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,
// qed.
-(* Instead of working with functions, it is sometimes convenient to work with
+(*
+\ 5h2 class="section"\ 6Predicates\ 5/h2\ 6
+Instead of working with functions, it is sometimes convenient to work with
predicates. For instance, instead of defining a function computing the opposite
bank, we could declare a predicate stating when two banks are opposite to each
-other. Only two cases are possible, leading naturally two the following
+other. Only two cases are possible, leading naturally to the following
definition:
*)
(* In precisely the same way as "bank" is the smallest type containing east and
west, opp is the smallest predicate containing the two sub-cases east_west and
weast_east. If you have some familiarity with Prolog, you may look at opp as the
-predicate definined by the two clauses - in this case, the two facts -
-(opp east west) and (opp west east).
-At the end of this section we shall prove that forall a and b,
- (opp a b) iff a = opposite b.
-For the moment, it is time to proceed with our formalization of the farmer's
-problem.
+predicate defined by the two clauses - in this case, the two facts - ast_west and
+west_east.
+
+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 *)
+
+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.
+
+(* We start the proof introducing a, b and the hypothesis opp a b, that we
+call oppab. *)
+#a #b #oppab
+
+(* Now we proceed by cases on the possible proofs of (opp a b), that is on the
+possible shapes of oppab. By definition, there are only two possibilities,
+namely east_west or west_east. Both subcases are trivial, and can be closed by
+automation *)
+
+cases oppab // qed.
+
+(*
+\ 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.
+
+(* As usual, we start introducing a, b and the hypothesis (a = opposite b),
+that we call eqa. *)
+
+#a #b #eqa
+
+(* The right way to proceed, now, is by rewriting a into (opposite b). We do
+this by typing ">eqa". If we wished to rewrite in the opposite direction, namely
+opposite b into a, we would have typed "<eqa". *)
+
+>eqa
+
+(* We conclude the proof by cases on b. *)
+
+cases b // qed.
+
+(*
+\ 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
wolf, the cabbage, and the boat. The simplest way to declare such a data type
is to use a record.
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)
+| 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_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).
| 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.
-(* Remarkably, Matita is now able to solve the problem by itslef, provided
+(*
+\ 5h2 class="section"\ 6Automation\ 5/h2\ 6
+Remarkably, Matita is now able to solve the problem by itslef, provided
you allow automation to exploit more resources. The command /n/ is similar to
//, where n is a measure of this complexity: in particular it is a bound to
the depth of the expected proof tree (more precisely, to the number of nested
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
+(*
+\ 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".
+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: \ 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
-(* We have now four open subgoals:
+(*
+\ 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
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
+(*
+\ 5h2 class="section"\ 6Implicit arguments\ 5/h2\ 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
-intermediate state, hence instead of applying more we can apply its
-instantiation (more ? (mk_state east west west west)). The question mark is
-an implicit argument to be guessed by the system. *)
+intermediate state, hence instead of applying more we can apply this term
+already instatated on the next intermediate state. As first argument, we
+type a question mark that stands for an implicit argument to be guessed by
+the system. *)
-\ 5span style="text-decoration: underline;"\ 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/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,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/reachable.con(0,2,0)"\ 6more\ 5/a\ 6 ? (\ 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,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))
-(* All subgoals are focused (they are all red). Two of them are trivial; we
-just call automation at level 2, and it will close both of them, taking
-us to the third move.*)
+(* We now get three independent subgoals, all actives, and two of them are
+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/
-(* We must now move the wolf. Suppose that, instead of specifying the next state
-we prefer to specify the move. In the style of the previous move, this amounts
-to apply the term (more … (move_wolf … )) The dots are a convenient syntax to
-express an arbitrary number of implicit parameters. *)
+(* 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
+move. In the spirit of the previous example, we can do it in the following 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,2,0)"\ 6move_wolf\ 5/a\ 6 … ))
-(* Unfortunately this is not enough to fully instantiate the intermediate state.
-All goals still depend from an unknown bank B. Calling automation in this situation
-does not help since it refuses to close subgoals instantiating other - still
-open - goals. A way to proceed is to focus on the fourth "bank" subgoal,
-instantiating it with the appropriate value, in this case east; then we close
-focusing, and call automation. To focus on subgoal i, instead of typing "|" several
-times we can just write "i:" as described by the following command. *)
-
- [4: @\ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6] /2/
-
-(* An alternative, simpler way is to instantiate each move with the destination
-bank. Let us complete the proof adopting this style. *)
-
-@(\ 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
+(* The dots stand here for an arbitrary number of implicit arguments, to be
+guessed by the system.
+Unfortunately, the previous move is not enough to fully instantiate the new
+intermediate state: a bank B remains unknown. Automation cannot help here,
+since all goals depend from this bank and automation refuses to close some
+subgoals instantiating other subgoals remaining open (the instantiation could
+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] /\ 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 … )) /\ 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
projects / helm.git / blobdiff