-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 ≝
-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 ].
+(* 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. *)
+
+\ 5img class="anchor" src="icons/tick.png" id="flatten"\ 6let 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 ≝
+match l with [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 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 ].