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. *)
-definition opposite ≝ λs.
+\ 5img class="anchor" src="icons/tick.png" id="opposite"\ 6definition opposite ≝ λs.
match s with
- [ east ⇒ west
- | west ⇒ east
+ [ 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
].
(* Functions are live entities, and can be actually computed. To check this, let
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 : opposite east = west.
+\ 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.
(*
\ 5h2 class="section"\ 6The goal window\ 5/h2\ 6
In this case, we avoid the unnecessary simplification step: // will take care of
it. *)
-lemma west_to_east : opposite west = east.
+\ 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.
(*
\ 5h2 class="section"\ 6Introduction\ 5/h2\ 6
A slightly more complex problem consists in proving that opposite is idempotent *)
-lemma idempotent_opposite : ∀x. opposite (opposite x) = 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
definition:
*)
-inductive opp : bank → bank → Prop ≝
-| east_west : opp east west
-| west_east : opp west east.
+\ 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.
(* 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
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. opp a b → a = opposite 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. *)
\ 5h2 class="section"\ 6Rewriting\ 5/h2\ 6
Let us come to the opposite direction. *)
-lemma opposite_to_opp: ∀a,b. a = opposite b → opp 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. *)
is to use a record.
*)
-record state : Type[0] ≝
- {goat_pos : bank;
- wolf_pos : bank;
- cabbage_pos: bank;
- boat_pos : bank}.
+\ 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;
+ boat_pos : \ 5a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"\ 6bank\ 5/a\ 6}.
(* When you define a record named foo, the system automatically defines a record
constructor named mk_foo. To construct a new record you pass as arguments to
mk_foo the values of the record fields *)
-definition start ≝ mk_state east east east east.
-definition end ≝ mk_state west west west west.
+\ 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. *)
-inductive move : state → state → Prop ≝
-| move_goat: ∀g,g1,w,c. opp g g1 → move (mk_state g w c g) (mk_state g1 w c g1)
+\ 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_wolf: ∀g,w,w1,c. opp w w1 → move (mk_state g w c w) (mk_state g w1 c w1)
-| move_cabbage: ∀g,w,c,c1.opp c c1 → move (mk_state g w c c) (mk_state g w c1 c1)
-| move_boat: ∀g,w,c,b,b1. opp b b1 → move (mk_state g w c b) (mk_state g w c b1).
+| 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).
(* 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 : state → Prop ≝
-| with_boat : ∀g,w,c.safe_state (mk_state g w c g)
-| opposite_side : ∀g,g1,b.opp g g1 → safe_state (mk_state g g1 g1 b).
+\ 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).
(* Finally, a state y is reachable from x if either there is a single move
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 : state → state → Prop ≝
-| one : ∀x,y.move x y → reachable x y
-| more : ∀x,z,y. \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6reachable x z → safe_state z → \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6move z y → reachable x y.
+\ 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.
(*
\ 5h2 class="section"\ 6Automation\ 5/h2\ 6
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: reachable start end.
-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.
+\ 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.
(*
\ 5h2 class="section"\ 6Application\ 5/h2\ 6
step, and so on).
*)
-lemma problem1: reachable start end.
-normalize @more
+\ 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
(*
\ 5h2 class="section"\ 6Focusing\ 5/h2\ 6
provide the intermediate state, that is [east,west,west,east]. We can do it, by
just applying this term. *)
- @(mk_state east west west east)
+ @(\ 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,1,0)"\ 6east\ 5/a\ 6)
(* This application closes the goal; at present, no goal has the focus on.
In order to act on the next goal, we must focus on it using the "|" operator. In
refocus on the skipped goal, going back to a situation similar to the one we
started with. *)
- | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace move_goat, east_west\ 5/span\ 6\ 5/span\ 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/ ]
(*
\ 5h2 class="section"\ 6Implicit arguments\ 5/h2\ 6
type a question mark that stands for an implicit argument to be guessed by
the system. *)
-@(more ? (mk_state east west west west))
+@(\ 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))
(* 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. *)
-/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace opposite_side, move_boat, east_west, west_east\ 5/span\ 6\ 5/span\ 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/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
move. In the spirit of the previous example, we can do it in the following way
*)
-@(more … (move_wolf … ))
+@(\ 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 … ))
(* The dots stand here for an arbitrary number of implicit arguments, to be
guessed by the system.
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: @east] /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace with_boat, east_west\ 5/span\ 6\ 5/span\ 6/
+[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. *)
-@(more … (move_goat west … )) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace with_boat, west_east\ 5/span\ 6\ 5/span\ 6/
-@(more … (move_cabbage ?? east … )) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace opposite_side, east_west, west_east\ 5/span\ 6\ 5/span\ 6/
-@(more … (move_boat ??? west … )) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace with_boat, west_east\ 5/span\ 6\ 5/span\ 6/
-@one /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace move_goat, east_west\ 5/span\ 6\ 5/span\ 6/ 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
projects / helm.git / blobdiff