manual commit after active hyperlinks

[helm.git] / weblib / tutorial / chapter6.ma

diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma
index 679331198007d38a8d2734f08042587480be18de..dd6d7cc78222e90f773c2eca98479f1cbba67e77 100644 (file)
--- a/weblib/tutorial/chapter6.ma
+++ b/weblib/tutorial/chapter6.ma
@@ -7,7 +7,7 @@ of words over a given alphabet, that we shall represent as a predicate over word
 include "tutorial/chapter5.ma".
 
 (* A word (or string) over an alphabet S is just a list of elements of S.*)
-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\ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6\ 5/span\ 6 S.
+\ 5img class="anchor" src="icons/tick.png" id="word"\ 6definition 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\ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6\ 5/span\ 6 S.
 
 (* For any alphabet there is only one word of length 0, the \ 5i\ 6empty word\ 5/i\ 6, which is 
 denoted by ϵ .*) 
@@ -31,8 +31,8 @@ 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:\ 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\ 6\ 5span class="error" title="Parse error: [sym_] or [ident] expected after [sym∃] (in [term])"\ 6\ 5/span\ 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\ 5span class="error" title="Parse error: [term] expected after [sym∧] (in [term])"\ 6\ 5/span\ 6 l2 w2.
+\ 5img class="anchor" src="icons/tick.png" id="cat"\ 6definition cat : ∀S,l1,l2,w.Prop ≝ 
+  λ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\ 6\ 5span class="error" title="Parse error: [sym_] or [ident] expected after [sym∃] (in [term])"\ 6\ 5/span\ 6w1,w2\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6w1 \ 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\ 5span class="error" title="Parse error: [term] expected after [sym∧] (in [term])"\ 6\ 5/span\ 6 l2 w2.
 
 notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
 interpretation "cat lang" 'middot a b = (cat ? a b).
@@ -45,40 +45,40 @@ 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. *)
 
-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 ].
+\ 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 ].
 
 (* 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 : \ 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\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 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 ≝
+\ 5img class="anchor" src="icons/tick.png" id="conjunct"\ 6let 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\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 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 ≝
 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 ]. 
 
 (* 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:\ 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. 
+\ 5img class="anchor" src="icons/tick.png" id="star"\ 6definition 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. 
 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. *)
 
-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).
+\ 5img class="anchor" src="icons/tick.png" id="deriv"\ 6definition 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w).
 
 (* 
 \ 5h2 class="section"\ 6Language equalities\ 5/h2\ 6
 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:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop. 
+\ 5img class="anchor" src="icons/tick.png" id="cat_ext_l"\ 6lemma cat_ext_l: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop. 
   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.
 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
 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/
 qed.
 
-lemma cat_ext_r: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop. 
+\ 5img class="anchor" src="icons/tick.png" id="cat_ext_r"\ 6lemma cat_ext_r: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop. 
   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.
 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
 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/ 
@@ -86,7 +86,7 @@ qed.
   
 (* Concatenating a language with the empty language results in the
 empty language. *) 
-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.
+\ 5img class="anchor" src="icons/tick.png" id="cat_empty_l"\ 6lemma 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.
 #S #A #w % [|*] * #w1 * #w2 * * #_ *
 qed.
 
@@ -94,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:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
-  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. 
+\ 5img class="anchor" src="icons/tick.png" id="epsilon_cat_r"\ 6lemma epsilon_cat_r: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
+  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="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61  A. 
 #S #A #w %
   [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
-  |#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/
+  |#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 \ 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/
   ]
 qed.
 
-lemma epsilon_cat_l: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
-  \ 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. 
+\ 5img class="anchor" src="icons/tick.png" id="epsilon_cat_l"\ 6lemma epsilon_cat_l: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
+  \ 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="singleton" 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. 
 #S #A #w %
   [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
   |#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/
@@ -112,27 +112,27 @@ lemma epsilon_cat_l: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3
 
 (* Concatenation is distributive w.r.t. union. *)
 
-lemma distr_cat_r: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
+\ 5img class="anchor" src="icons/tick.png" id="distr_cat_r"\ 6lemma distr_cat_r: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
   (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. 
 #S #A #B #C #w %
   [* #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/] 
 qed.
 
-lemma distr_cat_r_eps: ∀S.∀A,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
-  (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. 
+\ 5img class="anchor" src="icons/tick.png" id="distr_cat_r_eps"\ 6lemma distr_cat_r_eps: ∀S.∀A,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
+  (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="singleton" 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. 
   #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]
 qed.
 
 (* The following is a major property of derivatives *)
 
-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.
+\ 5img class="anchor" src="icons/tick.png" id="deriv_middot"\ 6lemma 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.
 #S #A #B #a #noteps #w normalize %
   [* #w1 cases w1 
     [* #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/
     |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct
      #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) % // % //
     ]
-  |* #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))
+  |* #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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w1))
    @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … w2) % // % normalize //
   ]
 qed. 
@@ -142,19 +142,19 @@ qed.
 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:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
-  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.
-#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/
+\ 5img class="anchor" src="icons/tick.png" id="espilon_in_star"\ 6lemma espilon_in_star: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
+  A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 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.
+#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 \ 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/
 qed.
 
-lemma cat_to_star:∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
-  ∀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).
-#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)) 
+\ 5img class="anchor" src="icons/tick.png" id="cat_to_star"\ 6lemma cat_to_star:∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
+  ∀w1,w2. A w1 → A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 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\ 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).
+#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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l)) 
 % 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/
 qed.
 
-lemma fix_star: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop. 
-  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}.
+\ 5img class="anchor" src="icons/tick.png" id="fix_star"\ 6lemma fix_star: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop. 
+  A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 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="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="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
 #S #A #w %
   [* #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/]
    #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
@@ -165,14 +165,14 @@ lemma fix_star: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6wo
   ]
 qed.
 
-lemma star_fix_eps : ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
-  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}.  
+\ 5img class="anchor" src="icons/tick.png" id="star_fix_eps"\ 6lemma star_fix_eps : ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
+  A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 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="singleton" 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="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="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.  
 #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 
-        @(\ 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)) %
+        @(\ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w1)) @(\ 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)) %
          [% [@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/]
        ]
     ]
@@ -182,8 +182,8 @@ lemma star_fix_eps : ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3
   ]
 qed. 
      
-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.
-  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*.
+\ 5img class="anchor" src="icons/tick.png" id="star_epsilon"\ 6lemma 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.
+  A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 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="singleton" 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\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6.
 #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/ * // 
 qed.
   
\ No newline at end of file