X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter6.ma;h=dd6d7cc78222e90f773c2eca98479f1cbba67e77;hb=c0ac63fead67ea1902e3d923ce877a2779cf501e;hp=679331198007d38a8d2734f08042587480be18de;hpb=7f6235dca57343e63217316b6415599daef7d4aa;p=helm.git

diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma
index 679331198..dd6d7cc78 100644
--- a/weblib/tutorial/chapter6.ma
+++ b/weblib/tutorial/chapter6.ma
@@ -7,7 +7,7 @@ of words over a given alphabet, that we shall represent as a predicate over word
 include "tutorial/chapter5.ma".
 
 (* A word (or string) over an alphabet S is just a list of elements of S.*)
-definition word ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"/span S.
+img class="anchor" src="icons/tick.png" id="word"definition word ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"/span S.
 
 (* For any alphabet there is only one word of length 0, the iempty word/i, which is 
 denoted by ϵ .*) 
@@ -31,8 +31,8 @@ operations induced by string concatenation, and in particular the concatenation
 A · B of two languages A and B, the so called Kleene's star A* of A and the 
 derivative of a language A w.r.t. a given character a. *)
 
-definition cat : ∀S,l1,l2,w.Prop ≝ 
-  λS.λl1,l2.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/aspan class="error" title="Parse error: [sym_] or [ident] expected after [sym∃] (in [term])"/spanw1,w2.w1 a title="append" href="cic:/fakeuri.def(1)"@/a w2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a l1 w1 a title="logical and" href="cic:/fakeuri.def(1)"∧/aspan class="error" title="Parse error: [term] expected after [sym∧] (in [term])"/span l2 w2.
+img class="anchor" src="icons/tick.png" id="cat"definition cat : ∀S,l1,l2,w.Prop ≝ 
+  λS.λl1,l2.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/aspan class="error" title="Parse error: [sym_] or [ident] expected after [sym∃] (in [term])"/spanw1,w2a title="exists" href="cic:/fakeuri.def(1)"./aw1 a title="append" href="cic:/fakeuri.def(1)"@/a w2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a l1 w1 a title="logical and" href="cic:/fakeuri.def(1)"∧/aspan class="error" title="Parse error: [term] expected after [sym∧] (in [term])"/span l2 w2.
 
 notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
 interpretation "cat lang" 'middot a b = (cat ? a b).
@@ -45,40 +45,40 @@ w1,w2,...wk all belonging to l, such that l = w1w2...wk.
 We need to define the latter operations. The following flatten function takes in 
 input a list of words and concatenates them together. *)
 
-let rec flatten (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) on l : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S ≝ 
-match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons w tl ⇒ w a title="append" href="cic:/fakeuri.def(1)"@/a flatten ? tl ].
+img class="anchor" src="icons/tick.png" id="flatten"let rec flatten (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) on l : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S ≝ 
+match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a | cons w tl ⇒ w a title="append" href="cic:/fakeuri.def(1)"@/a flatten ? tl ].
 
 (* Given a list of words l and a language r, (conjunct l r) is true if and only if
 all words in l are in r, that is for every w in l, r w holds. *)
 
-let rec conjunct (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: RPAREN expected after [term] (in [arg])"/span (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop) on l: Prop ≝
+img class="anchor" src="icons/tick.png" id="conjunct"let rec conjunct (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/aspan class="error" title="Parse error: RPAREN expected after [term] (in [arg])"/span (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop) on l: Prop ≝
 match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons w tl ⇒ r w a title="logical and" href="cic:/fakeuri.def(1)"∧/a conjunct ? tl r ]. 
 
 (* We are ready to give the formal definition of the Kleene's star of l:
 a word w belongs to l* is and only if there exists a list of strings 
 lw such that (conjunct lw l) and  l = flatten lw. *)
 
-definition star ≝ λS.λl.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/alw.a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"flatten/a ? lw a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/tutorial/chapter6/conjunct.fix(0,1,4)"conjunct/a ? lw l. 
+img class="anchor" src="icons/tick.png" id="star"definition star ≝ λS.λl.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/alw.a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"flatten/a ? lw a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/tutorial/chapter6/conjunct.fix(0,1,4)"conjunct/a ? lw l. 
 notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
 interpretation "star lang" 'star l = (star ? l).
 
 (* The derivative of a language A with respect to a character a is the set of
 all strings w such that aw is in A. *)
 
-definition deriv ≝ λS.λA:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.λa,w. A (aa title="cons" href="cic:/fakeuri.def(1)":/a:w).
+img class="anchor" src="icons/tick.png" id="deriv"definition deriv ≝ λS.λA:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.λa,w. A (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw).
 
 (* 
 h2 class="section"Language equalities/h2
 Equality between languages is just the usual extensional equality between
 sets. The operation of concatenation behaves well with respect to this equality. *)
 
-lemma cat_ext_l: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. 
+img class="anchor" src="icons/tick.png" id="cat_ext_l"lemma cat_ext_l: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. 
   A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="cat lang" href="cic:/fakeuri.def(1)"·/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="cat lang" href="cic:/fakeuri.def(1)"·/a B.
 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
 cases (H w1) /span class="autotactic"6span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
 qed.
 
-lemma cat_ext_r: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. 
+img class="anchor" src="icons/tick.png" id="cat_ext_r"lemma cat_ext_r: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. 
   B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="cat lang" href="cic:/fakeuri.def(1)"·/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="cat lang" href="cic:/fakeuri.def(1)"·/a C.
 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
 cases (H w2) /span class="autotactic"6span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ 
@@ -86,7 +86,7 @@ qed.
   
 (* Concatenating a language with the empty language results in the
 empty language. *) 
-lemma cat_empty_l: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S→Prop. a title="empty set" href="cic:/fakeuri.def(1)"∅/a a title="cat lang" href="cic:/fakeuri.def(1)"·/a A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="empty set" href="cic:/fakeuri.def(1)"∅/a.
+img class="anchor" src="icons/tick.png" id="cat_empty_l"lemma cat_empty_l: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S→Prop. a title="empty set" href="cic:/fakeuri.def(1)"∅/a a title="cat lang" href="cic:/fakeuri.def(1)"·/a A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="empty set" href="cic:/fakeuri.def(1)"∅/a.
 #S #A #w % [|*] * #w1 * #w2 * * #_ *
 qed.
 
@@ -94,16 +94,16 @@ qed.
 empty string, results in the language l; that is {ϵ} is a left and right 
 unit with respect to concatenation. *)
 
-lemma epsilon_cat_r: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop.
-  A a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1  A. 
+img class="anchor" src="icons/tick.png" id="epsilon_cat_r"lemma epsilon_cat_r: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop.
+  A a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/aa title="singleton" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1  A. 
 #S #A #w %
   [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
-  |#inA @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … w) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a title="nil" href="cic:/fakeuri.def(1)"[/a ]) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
+  |#inA @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … w) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
   ]
 qed.
 
-lemma epsilon_cat_l: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop.
-  a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a} a title="cat lang" href="cic:/fakeuri.def(1)"·/a A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1  A. 
+img class="anchor" src="icons/tick.png" id="epsilon_cat_l"lemma epsilon_cat_l: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop.
+  a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/aa title="singleton" href="cic:/fakeuri.def(1)"}/a a title="cat lang" href="cic:/fakeuri.def(1)"·/a A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1  A. 
 #S #A #w %
   [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
   |#inA @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … w) /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
@@ -112,27 +112,27 @@ lemma epsilon_cat_l: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3
 
 (* Concatenation is distributive w.r.t. union. *)
 
-lemma distr_cat_r: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop.
+img class="anchor" src="icons/tick.png" id="distr_cat_r"lemma distr_cat_r: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop.
   (A a title="union" href="cic:/fakeuri.def(1)"∪/a B) a title="cat lang" href="cic:/fakeuri.def(1)"·/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1  A a title="cat lang" href="cic:/fakeuri.def(1)"·/a C a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="cat lang" href="cic:/fakeuri.def(1)"·/a C. 
 #S #A #B #C #w %
   [* #w1 * #w2 * * #eqw * /span class="autotactic"6span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a, a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ |* * #w1 * #w2 * * /span class="autotactic"6span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a, a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/] 
 qed.
 
-lemma distr_cat_r_eps: ∀S.∀A,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop.
-  (A a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a}) a title="cat lang" href="cic:/fakeuri.def(1)"·/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1  A a title="cat lang" href="cic:/fakeuri.def(1)"·/a C a title="union" href="cic:/fakeuri.def(1)"∪/a C. 
+img class="anchor" src="icons/tick.png" id="distr_cat_r_eps"lemma distr_cat_r_eps: ∀S.∀A,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop.
+  (A a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/aa title="singleton" href="cic:/fakeuri.def(1)"}/a) a title="cat lang" href="cic:/fakeuri.def(1)"·/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1  A a title="cat lang" href="cic:/fakeuri.def(1)"·/a C a title="union" href="cic:/fakeuri.def(1)"∪/a C. 
   #S #A #C @a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"eqP_trans/a [|@a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"distr_cat_r/a |@a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"eqP_union_l/a @a href="cic:/matita/tutorial/chapter6/epsilon_cat_l.def(5)"epsilon_cat_l/a]
 qed.
 
 (* The following is a major property of derivatives *)
 
-lemma deriv_middot: ∀S,A,B,a. a title="logical not" href="cic:/fakeuri.def(1)"¬/a A a title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a → a href="cic:/matita/tutorial/chapter6/deriv.def(4)"deriv/a S (Aa title="cat lang" href="cic:/fakeuri.def(1)"·/aB) a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (a href="cic:/matita/tutorial/chapter6/deriv.def(4)"deriv/a S A a) a title="cat lang" href="cic:/fakeuri.def(1)"·/a B.
+img class="anchor" src="icons/tick.png" id="deriv_middot"lemma deriv_middot: ∀S,A,B,a. a title="logical not" href="cic:/fakeuri.def(1)"¬/a A a title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a → a href="cic:/matita/tutorial/chapter6/deriv.def(4)"deriv/a S (Aa title="cat lang" href="cic:/fakeuri.def(1)"·/aB) a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (a href="cic:/matita/tutorial/chapter6/deriv.def(4)"deriv/a S A a) a title="cat lang" href="cic:/fakeuri.def(1)"·/a B.
 #S #A #B #a #noteps #w normalize %
   [* #w1 cases w1 
     [* #w2 * * #_ #Aeps @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/
     |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct
      #H #H1 @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … w2) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … w3) % // % //
     ]
-  |* #w1 * #w2 * * #H #H1 #H2 @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (aa title="cons" href="cic:/fakeuri.def(1)":/a:w1))
+  |* #w1 * #w2 * * #H #H1 #H2 @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw1))
    @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … w2) % // % normalize //
   ]
 qed. 
@@ -142,19 +142,19 @@ qed.
 We conclude this section with some important properties of Kleene's
 star that will be used in the following chapters. *)
 
-lemma espilon_in_star: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.
-  Aa title="star lang" href="cic:/fakeuri.def(1)"^/a* a title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a.
-#S #A @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a title="nil" href="cic:/fakeuri.def(1)"[/a ]) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/basics/logic/True.con(0,1,0)"I/a/span/span/
+img class="anchor" src="icons/tick.png" id="espilon_in_star"lemma espilon_in_star: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.
+  Aa title="star lang" href="cic:/fakeuri.def(1)"^/aa title="star lang" href="cic:/fakeuri.def(1)"*/a a title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a.
+#S #A @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/basics/logic/True.con(0,1,0)"I/a/span/span/
 qed.
 
-lemma cat_to_star:∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.
-  ∀w1,w2. A w1 → Aa title="star lang" href="cic:/fakeuri.def(1)"^/a* w2 → Aa title="star lang" href="cic:/fakeuri.def(1)"^/a* (w1a title="append" href="cic:/fakeuri.def(1)"@/aw2).
-#S #A #w1 #w2 #Aw * #l * #H #H1 @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (w1a title="cons" href="cic:/fakeuri.def(1)":/a:l)) 
+img class="anchor" src="icons/tick.png" id="cat_to_star"lemma cat_to_star:∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.
+  ∀w1,w2. A w1 → Aa title="star lang" href="cic:/fakeuri.def(1)"^/aa title="star lang" href="cic:/fakeuri.def(1)"*/a w2 → Aa title="star lang" href="cic:/fakeuri.def(1)"^/aa title="star lang" href="cic:/fakeuri.def(1)"*/a (w1a title="append" href="cic:/fakeuri.def(1)"@/aw2).
+#S #A #w1 #w2 #Aw * #l * #H #H1 @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (w1a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al)) 
 % normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
 qed.
 
-lemma fix_star: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop. 
-  Aa title="star lang" href="cic:/fakeuri.def(1)"^/a* a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="cat lang" href="cic:/fakeuri.def(1)"·/a Aa title="star lang" href="cic:/fakeuri.def(1)"^/a* a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a}.
+img class="anchor" src="icons/tick.png" id="fix_star"lemma fix_star: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop. 
+  Aa title="star lang" href="cic:/fakeuri.def(1)"^/aa title="star lang" href="cic:/fakeuri.def(1)"*/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="cat lang" href="cic:/fakeuri.def(1)"·/a Aa title="star lang" href="cic:/fakeuri.def(1)"^/aa title="star lang" href="cic:/fakeuri.def(1)"*/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/aa title="singleton" href="cic:/fakeuri.def(1)"}/a.
 #S #A #w %
   [* #l generalize in match w; -w cases l [normalize #w * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/]
    #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
@@ -165,14 +165,14 @@ lemma fix_star: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"wo
   ]
 qed.
 
-lemma star_fix_eps : ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.
-  Aa title="star lang" href="cic:/fakeuri.def(1)"^/a* a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (A a title="substraction" href="cic:/fakeuri.def(1)"-/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a}) a title="cat lang" href="cic:/fakeuri.def(1)"·/a Aa title="star lang" href="cic:/fakeuri.def(1)"^/a* a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a}.  
+img class="anchor" src="icons/tick.png" id="star_fix_eps"lemma star_fix_eps : ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.
+  Aa title="star lang" href="cic:/fakeuri.def(1)"^/aa title="star lang" href="cic:/fakeuri.def(1)"*/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (A a title="substraction" href="cic:/fakeuri.def(1)"-/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/aa title="singleton" href="cic:/fakeuri.def(1)"}/a) a title="cat lang" href="cic:/fakeuri.def(1)"·/a Aa title="star lang" href="cic:/fakeuri.def(1)"^/aa title="star lang" href="cic:/fakeuri.def(1)"*/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/aa title="singleton" href="cic:/fakeuri.def(1)"}/a.  
 #S #A #w %
   [* #l elim l 
     [* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw // 
     |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
        |#a #w1 #tl #Hind * whd in ⊢ ((??%?)→?); #H1 * #H2 #H3 %1 
-        @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (aa title="cons" href="cic:/fakeuri.def(1)":/a:w1)) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"flatten/a S tl)) %
+        @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw1)) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"flatten/a S tl)) %
          [% [@H1 | normalize % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a/span/span/] |whd @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … tl) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/]
        ]
     ]
@@ -182,8 +182,8 @@ lemma star_fix_eps : ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3
   ]
 qed. 
      
-lemma star_epsilon: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.
-  Aa title="star lang" href="cic:/fakeuri.def(1)"^/a* a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 Aa title="star lang" href="cic:/fakeuri.def(1)"^/a*.
+img class="anchor" src="icons/tick.png" id="star_epsilon"lemma star_epsilon: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop.
+  Aa title="star lang" href="cic:/fakeuri.def(1)"^/aa title="star lang" href="cic:/fakeuri.def(1)"*/a a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/aa title="singleton" href="cic:/fakeuri.def(1)"}/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 Aa title="star lang" href="cic:/fakeuri.def(1)"^/aa title="star lang" href="cic:/fakeuri.def(1)"*/a.
 #S #A #w % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ * // 
 qed.
   
\ No newline at end of file