X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter6.ma;h=dd6d7cc78222e90f773c2eca98479f1cbba67e77;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hp=58e349509ec31ae4fda010b4e47b2570d319236e;hpb=05bcc10ec41117f33d2eb6a120df4024ae14b185;p=helm.git

diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma
index 58e349509..dd6d7cc78 100644
--- a/weblib/tutorial/chapter6.ma
+++ b/weblib/tutorial/chapter6.ma
@@ -1,97 +1,189 @@
-include "basics/logic.ma".
+(*
+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".
 
-(* Given a universe A, we can consider sets of elements of type A by means of their 
-characteristic predicates A → Prop. *)
+(* 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.
 
-definition set ≝ λA:Type[0].A → Prop.
+(* For any alphabet there is only one word of length 0, the iempty word/i, which is 
+denoted by ϵ .*) 
 
-(* For instance, the empty set is the set defined by an always False predicate *)
-
-definition empty : ∀A.a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA.λa:A.a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a.
-
-(* the singleton set {a} can be defined by the characteristic predicate stating 
-equality with a *)
-
-definition singleton: ∀A.A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA.λa,x.aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax. 
-
-(* Complement, union and intersection are easily defined, by means of logical 
-connectives *)
-
-definition complement: ∀A. a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA,P,x.a title="logical not" href="cic:/fakeuri.def(1)"¬/a(P x).
-
-definition intersection: ∀A. a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA,P,Q,x.(P x) a title="logical and" href="cic:/fakeuri.def(1)"∧/a (Q x). 
-
-definition union: ∀A. a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A → a href="cic:/matita/tutorial/chapter4/set.def(1)"set/a A ≝ λA,P,Q,x.(P x) a title="logical or" href="cic:/fakeuri.def(1)"∨/a (Q x).
-
-
-
-
-
-
-
- (* The reader could probably wonder what is the difference between Prop and bool.
-In fact, they are quite distinct entities. In type theory, all objects are structured
-in a three levels hierarchy
-   t : A : s 
-where, t is a term, A is a type, and s is called a sort. Sorts are special, primitive
-constants used to give a type to types. Now, Prop is a primitive sort, while bool is
-just a user defined data type (whose sort his Type[0]). In particular, Prop is the 
-sort of Propositions: its elements are logical statements in the usual sense. The important
-point is that statements are inhabited by their proofs: a triple of the kind
-   p : Q : Prop
-should be read as p is a proof of the proposition Q.*)
-
-
-
-include "arithmetics/nat.ma".
-include "basics/list.ma".
-
-interpretation "iff" 'iff a b = (iff a b).  
+notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
+interpretation "epsilon" 'epsilon = (nil ?).
 
-record Alpha : Type[1] ≝ { carr :> Type[0];
-   eqb: carr → carr →    a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a;
-   eqb_true: ∀x,y. (eqb x y 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 (x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y)
-}.
- 
-notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
-interpretation "eqb" 'eqb a b = (eqb ? a b).
+(* 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.
+*)
 
-definition word ≝ λS:a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S.
+(*
+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. *)
 
-inductive re (S: a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a) : Type[0] ≝
-   z: re S
- | e: re S
- | s: S → re S
- | c: re S → re S → re S
- | o: re S → re S → re S
- | k: re S → re S.
- 
-notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
-notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
-interpretation "star" 'pk a = (k ? a).
-interpretation "or" 'plus a b = (o ? a b).
-           
-notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
-interpretation "cat" 'pc a b = (c ? a b).
+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.
 
-(* to get rid of \middot 
-coercion c  : ∀S:Alpha.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?. *)
+notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
+interpretation "cat lang" 'middot a b = (cat ? a b).
 
-notation < "a" non associative with precedence 90 for @{ 'ps $a}.
-notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
-interpretation "atom" 'ps a = (s ? a).
 
-notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
-interpretation "epsilon" 'epsilon = (e ?).
+(* 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. *)
 
-notation "∅" non associative with precedence 90 for @{ 'empty }.
-interpretation "empty" 'empty = (z ?).
+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 ].
 
-let rec flatten (S : a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"Alpha/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/re/word.def(3)"word/a S)) on l : a href="cic:/matita/tutorial/re/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 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/re/Alpha.ind(1,0,0)"Alpha/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/re/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/re/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 ]. 
 
-definition empty_lang ≝ λS.λw:a href="cic:/matita/tutorial/re/word.def(3)"word/a S.a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a.
-notation "{}" non associative with precedence 90 f
\ No newline at end of file
+(* 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).
+
+(* 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) /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.
+
+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/ 
+qed.
+  
+(* 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.
+
+(* 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 * /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.
+
+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 *)
+
+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)":/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. 
+
+(* 
+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.
+
+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.
+
+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 ⊢ (%→?); *
+   #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 @a href="cic:/matita/tutorial/chapter6/cat_to_star.def(6)"cat_to_star/a 
+  ]
+qed.
+
+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)":/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 @a href="cic:/matita/tutorial/chapter6/cat_to_star.def(6)"cat_to_star/a //
+     | whd in ⊢ (%→?); #H <H //
+     ]
+  ]
+qed. 
+     
+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