X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter6.ma;h=dd6d7cc78222e90f773c2eca98479f1cbba67e77;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=21e6e75aa935862bb4be22dceed0dab8a13ed066;hpb=01feaa4859598983ee07f43760811ff73eea001b;p=helm.git

diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma
index 21e6e75aa..dd6d7cc78 100644
--- a/weblib/tutorial/chapter6.ma
+++ b/weblib/tutorial/chapter6.ma
@@ -1,11 +1,13 @@
-include "tutorial/chapter5.ma".
-
-(* In this chapter we shall apply our notion of DeqSet, and the list operations 
+(*
+h1 class="section"Formal Languages/h1
+In this chapter we shall apply our notion of DeqSet, and the list operations 
 defined in Chapter 4 to formal languages. A formal language is an arbitrary set
 of words over a given alphabet, that we shall represent as a predicate over words. 
-A word (or string) over an alphabet S is just a list of elements of S. *) 
+*)
+include "tutorial/chapter5.ma".
 
-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/a S.
+(* A word (or string) over an alphabet S is just a list of elements of 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 ϵ .*) 
@@ -19,49 +21,64 @@ String concatenation is just the append operation over lists, hence there is no
 point to define it. Similarly, many of its properties, such as the fact that 
 concatenating a word with the empty word gives the original word, follow by 
 general results over lists.
+*)
 
+(*
+h2 class="section"Operations over languages/h2
 Languages inherit all the basic operations for sets, namely union, intersection, 
 complementation, substraction, and so on. In addition, we may define some new 
 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)"∃/aw1,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)"∧/a 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).
 
-(* Given a list of words, the flatten operation concatenates them all. *)
 
-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 ].
+(* Given a language l, the Kleene's star of l, denoted by l*, is the set of 
+finite-length strings that can be generated by concatenating arbitrary strings of 
+l. In other words, w belongs to l* is and only if there exists a list of strings 
+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. *)
+
+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/a (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 ]. 
 
-(* Given a language l, the kleene's star of l, denoted by l*, is the set of 
-finite-length strings that can be generated by concatenating arbitrary strings of 
-l. In other words, w belongs to l* is and only if there exists a list of strings 
-lw all belonging to l, such that l = flatten lw. *)
+(* 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).
 
-(* Equality between languages is just the usual extensional equality between
+(* 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. *)
+
+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/ 
+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/ 
@@ -69,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.
 
@@ -77,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/
@@ -95,50 +112,49 @@ 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 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).
+(* 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. 
 
-(* We conclude this section with some important properties of Kleene's
-star that will be usde in the following chapters. *)
+(* 
+h2 class="section"Main Properties of Kleene's star/h2
+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 ⊢ (%→?); *
@@ -149,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/]
        ]
     ]
@@ -166,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