weblib/tutorial/chapter6.ma

   1 include "tutorial/chapter5.ma".
   2
   3 (* In this chapter we shall apply our notion of DeqSet, and the list operations
   4 defined in Chapter 4 to formal languages. A formal language is an arbitrary set
   5 of words over a given alphabet, that we shall represent as a predicate over words.
   6 A word (or string) over an alphabet S is just a list of elements of S. *)
   7
   8 definition word ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S.
   9
  10 (* For any alphabet there is only one word of length 0, the \ 5i\ 6empty word\ 5/i\ 6, which is
  11 denoted by ϵ .*)
  12
  13 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
  14 interpretation "epsilon" 'epsilon = (nil ?).
  15
  16 (* The operation that consists in appending two words to form a new word, whose
  17 length is the sum of the lengths of the original words is called concatenation.
  18 String concatenation is just the append operation over lists, hence there is no
  19 point to define it. Similarly, many of its properties, such as the fact that
  20 concatenating a word with the empty word gives the original word, follow by
  21 general results over lists.
  22
  23 Languages inherit all the basic operations for sets, namely union, intersection,
  24 complementation, substraction, and so on. In addition, we may define some new
  25 operations induced by string concatenation, and in particular the concatenation
  26 A · B of two languages A and B, the so called Kleene's star A* of A and the
  27 derivative of a language A w.r.t. a given character a. *)
  28
  29 definition cat : ∀S,l1,l2,w.Prop ≝
  30   λS.λl1,l2.λw:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6w1,w2.w1 \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 w2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l1 w1 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 w2.
  31
  32 notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
  33 interpretation "cat lang" 'middot a b = (cat ? a b).
  34
  35 (* Given a list of words, the flatten operation concatenates them all. *)
  36
  37 let rec flatten (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S)) on l : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S ≝
  38 match l with [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] | cons w tl ⇒ w \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 flatten ? tl ].
  39
  40 (* Given a list of words l and a language r, (conjunct l r) is true if and only if
  41 all words in l are in r, that is for every w in l, r w holds. *)
  42
  43 let rec conjunct (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S)) (r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop) on l: Prop ≝
  44 match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons w tl ⇒ r w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 conjunct ? tl r ].
  45
  46 (* Given a language l, the kleene's star of l, denoted by l*, is the set of
  47 finite-length strings that can be generated by concatenating arbitrary strings of
  48 l. In other words, w belongs to l* is and only if there exists a list of strings
  49 lw all belonging to l, such that l = flatten lw. *)
  50
  51 definition star ≝ λS.λl.λw:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6lw.\ 5a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 ? lw \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter6/conjunct.fix(0,1,4)"\ 6conjunct\ 5/a\ 6 ? lw l.
  52 notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
  53 interpretation "star lang" 'star l = (star ? l).
  54
  55 (* Equality between languages is just the usual extensional equality between
  56 sets. The operation of concatenation behaves well with respect to this equality. *)
  57
  58 lemma cat_ext_l: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
  59   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C  → A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B.
  60 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
  61 cases (H w1) /\ 5span class="autotactic"\ 66\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  62 qed.
  63
  64 lemma cat_ext_r: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
  65   B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C.
  66 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
  67 cases (H w2) /\ 5span class="autotactic"\ 66\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  68 qed.
  69
  70 (* Concatenating a language with the empty language results in the
  71 empty language. *)
  72 lemma cat_empty_l: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S→Prop. \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6.
  73 #S #A #w % [|*] * #w1 * #w2 * * #_ *
  74 qed.
  75
  76 (* Concatenating a language l with the singleton language containing the
  77 empty string, results in the language l; that is {ϵ} is a left and right
  78 unit with respect to concatenation. *)
  79
  80 lemma epsilon_cat_r: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
  81   A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61  A.
  82 #S #A #w %
  83   [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
  84   |#inA @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]) /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  85   ]
  86 qed.
  87
  88 lemma epsilon_cat_l: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
  89   \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61  A.
  90 #S #A #w %
  91   [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
  92   |#inA @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w) /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  93   ]
  94   qed.
  95
  96 (* Concatenation is distributive w.r.t. union. *)
  97
  98 lemma distr_cat_r: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
  99   (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61  A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C.
 100 #S #A #B #C #w %
 101   [* #w1 * #w2 * * #eqw * /\ 5span class="autotactic"\ 66\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ |* * #w1 * #w2 * * /\ 5span class="autotactic"\ 66\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
 102 qed.
 103
 104 lemma distr_cat_r_eps: ∀S.∀A,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
 105   (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6}) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61  A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 C \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 C.
 106   #S #A #C @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6 |@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/epsilon_cat_l.def(5)"\ 6epsilon_cat_l\ 5/a\ 6]
 107 qed.
 108
 109 (* The derivative of a language A with respect to a character a is the set of
 110 all strings w such that aw is in A. *)
 111
 112 definition deriv ≝ λS.λA:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.λa,w. A (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w).
 113
 114 lemma deriv_middot: ∀S,A,B,a. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter6/deriv.def(4)"\ 6deriv\ 5/a\ 6 S (A\ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6B) a \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (\ 5a href="cic:/matita/tutorial/chapter6/deriv.def(4)"\ 6deriv\ 5/a\ 6 S A a) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B.
 115 #S #A #B #a #noteps #w normalize %
 116   [* #w1 cases w1
 117     [* #w2 * * #_ #Aeps @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 118     |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct
 119      #H #H1 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w2) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w3) % // % //
 120     ]
 121   |* #w1 * #w2 * * #H #H1 #H2 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w1))
 122    @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w2) % // % normalize //
 123   ]
 124 qed.
 125
 126 (* We conclude this section with some important properties of Kleene's
 127 star that will be usde in the following chapters. *)
 128
 129 lemma espilon_in_star: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
 130   A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6.
 131 #S #A @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/True.con(0,1,0)"\ 6I\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 132 qed.
 133
 134 lemma cat_to_star:∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
 135   ∀w1,w2. A w1 → A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* w2 → A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* (w1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6w2).
 136 #S #A #w1 #w2 #Aw * #l * #H #H1 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (w1\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))
 137 % normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 138 qed.
 139
 140 lemma fix_star: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
 141   A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6}.
 142 #S #A #w %
 143   [* #l generalize in match w; -w cases l [normalize #w * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
 144    #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
 145    #w1A #cw1 %1 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w1) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 S tl))
 146    % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ whd @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … tl) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 147   |* [2: whd in ⊢ (%→?); #eqw <eqw //]
 148    * #w1 * #w2 * * #eqw <eqw @\ 5a href="cic:/matita/tutorial/chapter6/cat_to_star.def(6)"\ 6cat_to_star\ 5/a\ 6
 149   ]
 150 qed.
 151
 152 lemma star_fix_eps : ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
 153   A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6}) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6}.
 154 #S #A #w %
 155   [* #l elim l
 156     [* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw //
 157     |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
 158        |#a #w1 #tl #Hind * whd in ⊢ ((??%?)→?); #H1 * #H2 #H3 %1
 159         @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w1)) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 S tl)) %
 160          [% [@H1 | normalize % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"\ 6sym_not_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] |whd @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … tl) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
 161        ]
 162     ]
 163   |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @\ 5a href="cic:/matita/tutorial/chapter6/cat_to_star.def(6)"\ 6cat_to_star\ 5/a\ 6 //
 164      | whd in ⊢ (%→?); #H <H //
 165      ]
 166   ]
 167 qed.
 168
 169 lemma star_epsilon: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
 170   A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
 171 #S #A #w % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * //
 172 qed.
 173