X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter6.ma;h=dd6d7cc78222e90f773c2eca98479f1cbba67e77;hb=1083ac3b1acac5f1ac1fa40a9a417dd9d268dced;hp=cadc0065c3bc06a1b610a5312827fdf9a680ea8b;hpb=5a2800676f0a9e2bdfff0645baa131699b26af21;p=helm.git

diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma
index cadc0065c..dd6d7cc78 100644
--- a/weblib/tutorial/chapter6.ma
+++ b/weblib/tutorial/chapter6.ma
@@ -1,129 +1,189 @@
+(*
+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. 
+*)
 include "tutorial/chapter5.ma".
 
-definition word ≝ λS:DeqSet.list 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 ϵ .*) 
 
 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
 interpretation "epsilon" 'epsilon = (nil ?).
 
-(* concatenation *)
-definition cat : ∀S,l1,l2,w.Prop ≝ 
-  λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
+(* The operation that consists in appending two words to form a new word, whose 
+length is the sum of the lengths of the original words is called concatenation.
+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. *)
+
+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).
 
-let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ 
-match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
 
-let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
-match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ 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 
+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. *)
+
+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 ]. 
 
-(* kleene's star *)
-definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. 
+(* 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. *)
+
+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).
 
-lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop. 
-  A =1 C  → A · B =1 C · B.
+(* 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. *)
+
+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) /6/ 
+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:word S →Prop. 
-  B =1 C → A · B =1 A · C.
+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) /6/ 
+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/ 
 qed.
   
-lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅.
+(* Concatenating a language with the empty language results in the
+empty language. *) 
+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.
 
-lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
-  (A ∪ B) · C =1  A · C ∪ B · C. 
+(* Concatenating a language l with the singleton language containing the
+empty string, results in the language l; that is {ϵ} is a left and right 
+unit with respect to concatenation. *)
+
+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 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.
+
+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/
+  ]
+  qed.
+
+(* Concatenation is distributive w.r.t. union. *)
+
+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 * /6/ |* * #w1 * #w2 * * /6/] 
+  [* #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.
 
-(* derivative *)
+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.
 
-definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
+(* The following is a major property of derivatives *)
 
-lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ → 
-  deriv S (A·B) a =1 (deriv S A 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 @False_ind /2/
+    [* #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 @(ex_intro … w2) @(ex_intro … w3) % // % //
+     #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 @(ex_intro … (a::w1))
-   @(ex_intro … w2) % // % normalize //
+  |* #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. 
 
-(* star properties *)
-lemma espilon_in_star: ∀S.∀A:word S → Prop.
-  A^* ϵ.
-#S #A @(ex_intro … [ ]) normalize /2/
+(* 
+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. *)
+
+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:word S → Prop.
-  ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
-#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l)) 
-% normalize /2/
+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:word S → Prop. 
-  A^* =1 A · 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 * /2/]
+  [* #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 ⊢ (%→?); *
-   #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
-   % /2/ whd @(ex_intro … tl) /2/
+   #w1A #cw1 %1 @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/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))
+   % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/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/
   |* [2: whd in ⊢ (%→?); #eqw <eqw //]
-   * #w1 * #w2 * * #eqw <eqw @cat_to_star 
+   * #w1 * #w2 * * #eqw <eqw @a href="cic:/matita/tutorial/chapter6/cat_to_star.def(6)"cat_to_star/a 
   ]
 qed.
 
-lemma star_fix_eps : ∀S.∀A:word S → Prop.
-  A^* =1 (A - {ϵ}) · 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 
-        @(ex_intro … (a::w1)) @(ex_intro … (flatten S tl)) %
-         [% [@H1 | normalize % /2/] |whd @(ex_intro … tl) /2/]
+        @(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/]
        ]
     ]
-  |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @cat_to_star //
+  |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @a href="cic:/matita/tutorial/chapter6/cat_to_star.def(6)"cat_to_star/a //
      | whd in ⊢ (%→?); #H <H //
      ]
   ]
 qed. 
      
-lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
-  A^* ∪ {ϵ} =1 A^*.
-#S #A #w % /2/ * // 
-qed.
-  
-lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
-   A · {ϵ} =1  A. 
-#S #A #w %
-  [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
-  |#inA @(ex_intro … w) @(ex_intro … [ ]) /3/
-  ]
-qed.
-
-lemma epsilon_cat_l: ∀S.∀A:word S →Prop.
-   {ϵ} · A =1  A. 
-#S #A #w %
-  [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
-  |#inA @(ex_intro … ϵ) @(ex_intro … w) /3/
-  ]
-qed.
-
-lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop.
-  (A ∪ {ϵ}) · C =1  A · C ∪ C. 
-#S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
+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