From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Apr 2013 11:53:15 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1198
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=0c94f81f769d3c7377811a584f647553ebe7ceaf

commit by user andrea
---

diff --git a/weblib/While/syntax.ma b/weblib/While/syntax.ma
new file mode 100644
index 000000000..b55d89d43
--- /dev/null
+++ b/weblib/While/syntax.ma
@@ -0,0 +1,58 @@
+(* While Syntax *)
+
+include "basics/logic.ma".
+include "basics/types.ma".
+include "basics/bool.ma".
+include "arithmetics/nat.ma".
+
+(* Variables *)
+
+inductive Var : Type[0] ≝
+  Id : nat → Var.
+ 
+(* Arithmetic expressions *)
+
+inductive Aexp : Type[0] ≝
+  | Const : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Aexp
+  | Aid : span style="text-decoration: underline;"/spanVar → Aexp
+  | Add : Aexp → Aexp → Aexp
+  | Sub : Aexp → Aexp → Aexp
+  | Mul : Aexp → Aexp → Aexp
+  | Div : Aexp → Aexp → Aexp
+  | Mod : Aexp → Aexp → Aexp
+ .
+
+interpretation "Aexp plus" 'plus x y = (Add x y).
+interpretation "Aexp minus" 'plus x y = (Sub x y).
+interpretation "Aexp times" 'times x y = (Mul x y).
+
+(* Boolean expressions *)
+inductive Bexp : Type[0] ≝
+  | BFalse : Bexp
+  | BTtrue : Bexp
+  | BNot : Bexp → Bexp
+  | BAnd : Bexp → Bexp → Bexp
+  | BOr : Bexp → Bexp → Bexp
+  | Eq : a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Bexp
+  | LE : a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Bexp
+.
+
+interpretation "Bexp not" 'not x = (BNot x).
+interpretation "Bexp and" 'and x y = (BAnd x y).
+interpretation "Bexp or" 'or x y = (BOr x y).
+interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y).
+
+(* Commands *)
+inductive Cmd : Type[0] ≝
+  | Skip : Cmd
+  | Assign : Var → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Cmd
+  | Seq : Cmd → Cmd → Cmd
+  | If : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd → Cmd
+  | While : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd
+.
+
+notation "hvbox(c1 break ; c2)"
+  left associative with precedence 47 for @{Seq $c1 $c2}.
+
+notation "hvbox(var break <- val)"
+  left associative with precedence 48 for @{Assign $var $val}.
\ No newline at end of file
diff --git a/weblib/prova.ma b/weblib/prova.ma
new file mode 100644
index 000000000..5fe5dcee7
--- /dev/null
+++ b/weblib/prova.ma
@@ -0,0 +1 @@
+(* new script *)
\ No newline at end of file
diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index 51fe4a402..ba759d47c 100644
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -11,9 +11,9 @@ lifted operators of the previous section:
 
 include "tutorial/chapter8.ma".
 
-img class="anchor" src="icons/tick.png" id="move"let rec move (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (x:S) (E: a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S) on E : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝
+let rec move (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (x:S) (E: a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S) on E : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝
  match E with
-  [ pz ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/a S, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a
+  [ pz ⇒ 〈a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/a S, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a
   | pe ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem epsilon" href="cic:/fakeuri.def(1)"ϵ/a, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a
   | ps y ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem ps" href="cic:/fakeuri.def(1)"`/ay, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a
   | pp y ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem ps" href="cic:/fakeuri.def(1)"`/ay, x a title="eqb" href="cic:/fakeuri.def(1)"=/aa title="eqb" href="cic:/fakeuri.def(1)"=/a y a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a
@@ -21,15 +21,15 @@ include "tutorial/chapter8.ma".
   | pc e1 e2 ⇒ (move ? x e1) a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a (move ? x e2)
   | pk e ⇒ (move ? x e)a title="lk" href="cic:/fakeuri.def(1)"^/aa title="lk" href="cic:/fakeuri.def(1)"⊛/a ].
   
-img class="anchor" src="icons/tick.png" id="move_plus"lemma move_plus: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
+lemma move_plus: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
   a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S x (i1 a title="pitem or" href="cic:/fakeuri.def(1)"+/a i2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i1) a title="oplus" href="cic:/fakeuri.def(1)"⊕/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i2).
 // qed.
 
-img class="anchor" src="icons/tick.png" id="move_cat"lemma move_cat: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
+lemma move_cat: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
   a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S x (i1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i1) a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i2).
 // qed.
 
-img class="anchor" src="icons/tick.png" id="move_star"lemma move_star: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
+lemma move_star: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
   a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S x ia title="pitem star" href="cic:/fakeuri.def(1)"^/aa title="pitem star" href="cic:/fakeuri.def(1)"*/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i)a title="lk" href="cic:/fakeuri.def(1)"^/aa title="lk" href="cic:/fakeuri.def(1)"⊛/a.
 // qed.
 
@@ -52,13 +52,13 @@ while the other point reaches the end of b* and must go back through b*a:
 
 *)
 
-img class="anchor" src="icons/tick.png" id="pmove"definition pmove ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λx:S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e).
+definition pmove ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λx:S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e).
 
-img class="anchor" src="icons/tick.png" id="pmove_def"lemma pmove_def : ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b. 
+lemma pmove_def : ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b. 
   a href="cic:/matita/tutorial/chapter9/pmove.def(7)"pmove/a ? x a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i.
 // qed.
 
-img class="anchor" src="icons/tick.png" id="eq_to_eq_hd"lemma eq_to_eq_hd: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a,b. 
+lemma eq_to_eq_hd: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a,b. 
   aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ba title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al2 → a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b.
 #A #l1 #l2 #a #b #H destruct //
 qed. 
@@ -66,7 +66,7 @@ qed.
 (* Obviously, a move does not change the carrier of the item, as one can easily 
 prove by induction on the item. *)
 
-img class="anchor" src="icons/tick.png" id="same_kernel"lemma same_kernel: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
+lemma same_kernel: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.
   a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? a i)a title="forget" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a.
 #S #a #i elim i //
   [#i1 #i2 #H1 #H2 >a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"move_cat/a >a href="cic:/matita/tutorial/chapter8/erase_odot.def(7)"erase_odot/a //
@@ -77,7 +77,7 @@ qed.
 (* Here is our first, major result, stating the correctness of the
 move operation. The proof is a simple induction on i. *)
 
-img class="anchor" src="icons/tick.png" id="move_ok"theorem move_ok:
+theorem move_ok:
  ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. 
    a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? a ia title="in_prl" href="cic:/fakeuri.def(1)"}/a w a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{ia title="in_pl" href="cic:/fakeuri.def(1)"}/a (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw).
 #S #a #i elim i 
@@ -107,39 +107,39 @@ qed.
 
 notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
 
-img class="anchor" src="icons/tick.png" id="moves"let rec moves (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) w e on w : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝
+let rec moves (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) w e on w : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝
  match w with
   [ nil ⇒ e
   | cons x w' ⇒ w' ↦* (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S x (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e))]. 
 
-img class="anchor" src="icons/tick.png" id="moves_empty"lemma moves_empty: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
+lemma moves_empty: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
   a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a e.
 // qed.
 
-img class="anchor" src="icons/tick.png" id="moves_cons"lemma moves_cons: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀w.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
+lemma moves_cons: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀w.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
   a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw)  e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e)).
 // qed.
 
-img class="anchor" src="icons/tick.png" id="moves_left"lemma moves_left : ∀S,a,w,e. 
+lemma moves_left : ∀S,a,w,e. 
   a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S (wa title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a)) e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e)). 
 #S #a #w elim w // #x #tl #Hind #e >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a //
 qed.
 
-img class="anchor" src="icons/tick.png" id="not_epsilon_sem"lemma not_epsilon_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. ∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
+lemma not_epsilon_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. ∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
   a href="cic:/matita/basics/logic/iff.def(1)"iff/a ((aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw) a title="in_prl mem" href="cic:/fakeuri.def(1)"∈/a e) ((aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw) a title="in_pl mem" href="cic:/fakeuri.def(1)"∈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e).
 #S #a #w * #i #b cases b normalize 
   [% /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ * // #H destruct |% normalize /span class="autotactic"2span class="autotrace" trace /span/span/]
 qed.
 
-img class="anchor" src="icons/tick.png" id="same_kernel_moves"lemma same_kernel_moves: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀w.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.
+lemma same_kernel_moves: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀w.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.
   a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e)a title="forget" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a ea title="forget" href="cic:/fakeuri.def(1)"|/a.
 #S #w elim w //
 qed.
 
-img class="anchor" src="icons/tick.png" id="decidable_sem"theorem decidable_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. ∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
+theorem decidable_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. ∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. 
    (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{ea title="in_prl" href="cic:/fakeuri.def(1)"}/a w.
 #S #w elim w 
- [* #i #b >a href="cic:/matita/tutorial/chapter9/moves_empty.def(8)"moves_empty/a cases b % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter7/true_to_epsilon.def(9)"true_to_epsilon/a/span/span/span class="error" title="error location"/span #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
+ [* #i #b >a href="cic:/matita/tutorial/chapter9/moves_empty.def(8)"moves_empty/a cases b % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter7/true_to_epsilon.def(9)"true_to_epsilon/a/span/span/ #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
  |#a #w1 #Hind #e >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a
   @a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a [||@a href="cic:/matita/basics/logic/iff_sym.def(2)"iff_sym/a @a href="cic:/matita/tutorial/chapter9/not_epsilon_sem.def(9)"not_epsilon_sem/a]
   @a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a [||@a href="cic:/matita/tutorial/chapter9/move_ok.def(14)"move_ok/a] @Hind
@@ -188,12 +188,12 @@ are final, while 8 and 9 are not).
 We conclude this chapter with a few properties of the move opertions in relation
 with the pit state. *)
 
-img class="anchor" src="icons/tick.png" id="pit_pre"definition pit_pre ≝ λS.λi.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a), a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. 
+definition pit_pre ≝ λS.λi.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a), a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. 
 
 (* The following function compute the list of characters occurring in a given
 item i. *)
 
-img class="anchor" src="icons/tick.png" id="occur"let rec occur (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on i ≝  
+let rec occur (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on i ≝  
   match i with
   [ z ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a
   | e ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a
@@ -205,7 +205,7 @@ item i. *)
 (* If a symbol a does not occur in i, then move(i,a) gets to the
 pit state. *)
 
-img class="anchor" src="icons/tick.png" id="not_occur_to_pit"lemma not_occur_to_pit: ∀S,a.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a)) a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a →
+lemma not_occur_to_pit: ∀S,a.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a)) a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a →
   a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a i  a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i.
 #S #a #i elim i //
   [#x normalize cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/aa title="eqb" href="cic:/fakeuri.def(1)"=/ax) normalize // #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
@@ -221,7 +221,7 @@ qed.
 
 (* We cannot escape form the pit state. *)
 
-img class="anchor" src="icons/tick.png" id="move_pit"lemma move_pit: ∀S,a,i. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i.
+lemma move_pit: ∀S,a,i. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i.
 #S #a #i elim i //
   [#i1 #i2 #Hind1 #Hind2 >a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"move_cat/a >Hind1 >Hind2 // 
   |#i1 #i2 #Hind1 #Hind2 >a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"move_plus/a >Hind1 >Hind2 // 
@@ -229,14 +229,14 @@ qed.
   ]
 qed. 
 
-img class="anchor" src="icons/tick.png" id="moves_pit"lemma moves_pit: ∀S,w,i. a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w (a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i.
+lemma moves_pit: ∀S,w,i. a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w (a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i.
 #S #w #i elim w // 
 qed. 
  
 (* If any character in w does not occur in i, then moves(i,w) gets
 to the pit state. *)
 
-img class="anchor" src="icons/tick.png" id="to_pit"lemma to_pit: ∀S,w,e. a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S w (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a ea title="forget" href="cic:/fakeuri.def(1)"|/a)) →
+lemma to_pit: ∀S,w,e. a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S w (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a ea title="forget" href="cic:/fakeuri.def(1)"|/a)) →
  a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e).
 #S #w elim w
   [#e * #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @H normalize #a #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
@@ -247,4 +247,4 @@ to the pit state. *)
     |#Hfalse >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a >a href="cic:/matita/tutorial/chapter9/not_occur_to_pit.def(8)"not_occur_to_pit/a // >Hfalse /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/ 
     ]
   ]
-qed.
+qed.
\ No newline at end of file