weblib/tutorial/chapter8.ma

   1 (*
   2 \ 5h1\ 6Broadcasting points\ 5/h1\ 6
   3 Intuitively, a regular expression e must be understood as a pointed expression with a single
   4 point in front of it. Since however we only allow points before symbols, we must broadcast
   5 this initial point inside e traversing all nullable subexpressions, that essentially corresponds
   6 to the ϵ-closure operation on automata. We use the notation •(_) to denote such an operation;
   7 its definition is the expected one: let us start discussing an example.
   8
   9 \ 5b\ 6Example\ 5/b\ 6
  10 Let us broadcast a point inside (a + ϵ)(b*a + b)b. We start working in parallel on the
  11 first occurrence of a (where the point stops), and on ϵ that gets traversed. We have hence
  12 reached the end of a + ϵ and we must pursue broadcasting inside (b*a + b)b. Again, we work in
  13 parallel on the two additive subterms b^*a and b; the first point is allowed to both enter the
  14 star, and to traverse it, stopping in front of a; the second point just stops in front of b.
  15 No point reached that end of b^*a + b hence no further propagation is possible. In conclusion:
  16                •((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉
  17 *)
  18
  19 include "tutorial/chapter7.ma".
  20
  21 (* Broadcasting a point inside an item generates a pre, since the point could possibly reach
  22 the end of the expression.
  23 Broadcasting inside a i1+i2 amounts to broadcast in parallel inside i1 and i2.
  24 If we define
  25                  〈i1,b1〉 ⊕ 〈i2,b2〉 = 〈i1 + i2, b1∨ b2〉
  26 then, we just have •(i1+i2) = •(i1)⊕ •(i2).
  27 *)
  28
  29 definition lo ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λa,b:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 a \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 b,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 a \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 b〉.
  30 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
  31 interpretation "oplus" 'oplus a b = (lo ? a b).
  32
  33 lemma lo_def: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀b1,b2. \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,b1〉\ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i2,b2〉\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1\ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i2,b1\ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6b2〉.
  34 // qed.
  35
  36 (*
  37 Concatenation is a bit more complex. In order to broadcast a point inside i1 · i2
  38 we should start broadcasting it inside i1 and then proceed into i2 if and only if a
  39 point reached the end of i1. This suggests to define •(i1 · i2) as •(i1) ▹ i2, where
  40 e ▹ i is a general operation of concatenation between a pre and an item, defined by
  41 cases on the boolean in e:
  42
  43        〈i1,true〉 ▹ i2  = i1 ◃ •(i_2)
  44        〈i1,false〉 ▹ i2 = i1 · i2
  45 In turn, ◃ says how to concatenate an item with a pre, that is however extremely simple:
  46         i1 ◃ 〈i1,b〉  = 〈i_1 · i2, b〉
  47 Let us come to the formalized definitions:
  48 *)
  49
  50 definition pre_concat_r ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λi:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
  51   match e with [ mk_Prod i1 b ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i1, b〉].
  52
  53 notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
  54 interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
  55
  56 lemma eq_to_ex_eq: ∀S.∀A,B:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
  57   A \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 B → A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B.
  58 #S #A #B #H >H #x % // qed.
  59
  60 (* The behaviour of ◃ is summarized by the following, easy lemma: *)
  61
  62 lemma sem_pre_concat_r : ∀S,i.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
  63   \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i \ 5a title="pre_concat_r" href="cic:/fakeuri.def(1)"\ 6◃\ 5/a\ 6 e} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e}.
  64 #S #i * #i1 #b1 cases b1 [2: @\ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6 //]
  65 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"\ 6sem_cat\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
  66 qed.
  67
  68 (* The definition of $•(-)$ (eclose) and ▹ (pre_concat_l) are mutually recursive.
  69 In this situation, a viable alternative that is usually simpler to reason about,
  70 is to abstract one of the two functions with respect to the other. In particular
  71 we abstract pre_concat_l with respect to an input bcast function from items to
  72 pres. *)
  73
  74 definition pre_concat_l ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λbcast:∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S → \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.λe1:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.λi2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
  75   match e1 with
  76   [ mk_Prod i1 b1 ⇒ match b1 with
  77     [ true ⇒ (i1 \ 5a title="pre_concat_r" href="cic:/fakeuri.def(1)"\ 6◃\ 5/a\ 6 (bcast ? i2))
  78     | false ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉
  79     ]
  80   ].
  81
  82 notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
  83 interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
  84
  85 (* We are ready to give the formal definition of the broadcasting operation. *)
  86
  87 notation "•" non associative with precedence 60 for @{eclose ?}.
  88
  89 let rec eclose (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (i: \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on i : \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
  90  match i with
  91   [ pz ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"\ 6pz\ 5/a\ 6 ?, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 〉
  92   | pe ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6,  \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 〉
  93   | ps x ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem pp" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6.x, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉
  94   | pp x ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem pp" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6.x, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 〉
  95   | po i1 i2 ⇒ •i1 \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 •i2
  96   | pc i1 i2 ⇒ •i1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i2
  97   | pk i ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (•i))\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉].
  98
  99 notation "• x" non associative with precedence 60 for @{'eclose $x}.
 100 interpretation "eclose" 'eclose x = (eclose ? x).
 101
 102 (* Here are a few simple properties of ▹ and •(-) *)
 103
 104 lemma pcl_true : ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 105   \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i1 \ 5a title="pre_concat_r" href="cic:/fakeuri.def(1)"\ 6◃\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2).
 106 // qed.
 107
 108 lemma pcl_true_bis : ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 109   \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2), \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2)〉.
 110 #S #i1 #i2 normalize cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2) // qed.
 111
 112 lemma pcl_false: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 113   \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6  i2  \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉.
 114 // qed.
 115
 116 lemma eclose_plus: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 117   \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6(i1 \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i1 \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2.
 118 // qed.
 119
 120 lemma eclose_dot: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 121   \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6(i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i2.
 122 // qed.
 123
 124 lemma eclose_star: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 125   \ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6(\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i))\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉.
 126 // qed.
 127
 128 (* The definition of •(-) (eclose) can then be lifted from items to pres
 129 in the obvious way. *)
 130
 131 definition lift ≝ λS.λf:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S →\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
 132   match e with
 133   [ mk_Prod i b ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (f i), \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (f i) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b〉].
 134
 135 definition preclose ≝ λS. \ 5a href="cic:/matita/tutorial/chapter8/lift.def(2)"\ 6lift\ 5/a\ 6 S (\ 5a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"\ 6eclose\ 5/a\ 6 S).
 136 interpretation "preclose" 'eclose x = (preclose ? x).
 137
 138 (* Obviously, broadcasting does not change the carrier of the item,
 139 as it is easily proved by structural induction. *)
 140
 141 lemma erase_bull : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i)| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i|.
 142 #S #i elim i //
 143   [ #i1 #i2 #IH1 #IH2 >\ 5a href="cic:/matita/tutorial/chapter7/erase_dot.def(4)"\ 6erase_dot\ 5/a\ 6 <IH1 >\ 5a href="cic:/matita/tutorial/chapter8/eclose_dot.def(5)"\ 6eclose_dot\ 5/a\ 6
 144     cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i1) #i11 #b1 cases b1 // <IH2 >\ 5a href="cic:/matita/tutorial/chapter8/pcl_true_bis.def(5)"\ 6pcl_true_bis\ 5/a\ 6 //
 145   | #i1 #i2 #IH1 #IH2 >\ 5a href="cic:/matita/tutorial/chapter8/eclose_plus.def(5)"\ 6eclose_plus\ 5/a\ 6 >(\ 5a href="cic:/matita/tutorial/chapter7/erase_plus.def(4)"\ 6erase_plus\ 5/a\ 6 … i1) <IH1 <IH2
 146     cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i1) #i11 #b1 cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2) #i21 #b2 //
 147   | #i #IH >\ 5a href="cic:/matita/tutorial/chapter8/eclose_star.def(5)"\ 6eclose_star\ 5/a\ 6 >(\ 5a href="cic:/matita/tutorial/chapter7/erase_star.def(4)"\ 6erase_star\ 5/a\ 6 … i) <IH cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i) //
 148   ]
 149 qed.
 150
 151 (* We are now ready to state the main semantic properties of ⊕, ◃ and •(-):
 152
 153 sem_oplus:     \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}
 154 sem_pcl:       \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}
 155 sem_bullet     \sem{•i} =1 \sem{i} ∪ \sem{|i|}
 156
 157 The proof of sem_oplus is straightforward. *)
 158
 159 lemma sem_oplus: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
 160   \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 e2} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2}.
 161 #S * #i1 #b1 * #i2 #b2 #w %
 162   [cases b1 cases b2 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 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\ 5/span\ 6\ 5/span\ 6/ * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 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\ 5/span\ 6\ 5/span\ 6/
 163   |cases b1 cases b2 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 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\ 5/span\ 6\ 5/span\ 6/ * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 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\ 5/span\ 6\ 5/span\ 6/
 164   ]
 165 qed.
 166
 167 (* For the others, we proceed as follow: we first prove the following
 168 auxiliary lemma, that assumes sem_bullet:
 169
 170 sem_pcl_aux:
 171    \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
 172    \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
 173
 174 Then, using the previous result, we prove sem_bullet by induction
 175 on i. Finally, sem_pcl_aux and sem_bullet give sem_pcl. *)
 176
 177 lemma LcatE : ∀S.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 178   \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 e2} \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6e2|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2}.
 179 // qed.
 180
 181 lemma sem_pcl_aux : ∀S.∀e1:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.∀i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 182    \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61  \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2|} →
 183    \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i2} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61  \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2}.
 184 #S * #i1 #b1 #i2 cases b1
 185   [2:#th >\ 5a href="cic:/matita/tutorial/chapter8/pcl_false.def(5)"\ 6pcl_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"\ 6sem_cat\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 186   |#H >\ 5a href="cic:/matita/tutorial/chapter8/pcl_true.def(5)"\ 6pcl_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 @(\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter8/sem_pre_concat_r.def(10)"\ 6sem_pre_concat_r\ 5/a\ 6 …))
 187    >\ 5a href="cic:/matita/tutorial/chapter8/erase_bull.def(6)"\ 6erase_bull\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@(\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 … H)]
 188     @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 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/chapter4/union_comm.def(3)"\ 6union_comm\ 5/a\ 6 ]]
 189     @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6 ] /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6, \ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 190   ]
 191 qed.
 192
 193 lemma minus_eps_pre_aux: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀A.
 194  \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 A → \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (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="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]}).
 195 #S #e #i #A #seme
 196 @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter7/minus_eps_pre.def(10)"\ 6minus_eps_pre\ 5/a\ 6]
 197 @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter7/minus_eps_item.def(9)"\ 6minus_eps_item\ 5/a\ 6]]
 198 @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/distribute_substract.def(3)"\ 6distribute_substract\ 5/a\ 6]
 199 @\ 5a href="cic:/matita/tutorial/chapter4/eqP_substract_r.def(3)"\ 6eqP_substract_r\ 5/a\ 6 //
 200 qed.
 201
 202 theorem sem_bull: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6. ∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.  \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i|}.
 203 #S #e elim e
 204   [#w normalize % [/\ 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/ | * //]
 205   |/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 206   |#x 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/ | * [@\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 | //]]
 207   |#x 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/ | * // ]
 208   |#i1 #i2 #IH1 #IH2 >\ 5a href="cic:/matita/tutorial/chapter8/eclose_dot.def(5)"\ 6eclose_dot\ 5/a\ 6
 209    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_pcl_aux.def(11)"\ 6sem_pcl_aux\ 5/a\ 6 //] >\ 5a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"\ 6sem_cat\ 5/a\ 6
 210    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6
 211      [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6
 212        [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@(\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 … IH1)] @\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6]]
 213    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
 214    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
 215    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 //
 216   |#i1 #i2 #IH1 #IH2 >\ 5a href="cic:/matita/tutorial/chapter8/eclose_plus.def(5)"\ 6eclose_plus\ 5/a\ 6
 217    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_oplus.def(9)"\ 6sem_oplus\ 5/a\ 6] >\ 5a href="cic:/matita/tutorial/chapter7/sem_plus.def(8)"\ 6sem_plus\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/erase_plus.def(4)"\ 6erase_plus\ 5/a\ 6
 218    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@(\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 … IH2)]
 219    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
 220    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6
 221    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
 222    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 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/chapter4/union_comm.def(3)"\ 6union_comm\ 5/a\ 6]]
 223    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 224   |#i #H >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter8/erase_bull.def(6)"\ 6erase_bull\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6
 225    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/minus_eps_pre_aux.def(11)"\ 6minus_eps_pre_aux\ 5/a\ 6 //]]]
 226    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6]]
 227    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 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/chapter7/erase_star.def(4)"\ 6erase_star\ 5/a\ 6
 228    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/star_fix_eps.def(7)"\ 6star_fix_eps\ 5/a\ 6
 229   ]
 230 qed.
 231
 232 (*
 233 \ 5h2\ 6Blank item\ 5/h2\ 6
 234
 235 As a corollary of theorem sem_bullet, given a regular expression e, we can easily
 236 find an item with the same semantics of $e$: it is enough to get an item (blank e)
 237 having e as carrier and no point, and then broadcast a point in it. The semantics of
 238 (blank e) is obviously the empty language: from the point of view of the automaton,
 239 it corresponds with the pit state. *)
 240
 241 let rec blank (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (i: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on i :\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S ≝
 242  match i with
 243   [ z ⇒ \ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"\ 6pz\ 5/a\ 6 ?
 244   | e ⇒ \ 5a title="pitem epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6
 245   | s y ⇒ \ 5a title="pitem ps" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6y
 246   | o e1 e2 ⇒ (blank S e1) \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (blank S e2)
 247   | c e1 e2 ⇒ (blank S e1) \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (blank S e2)
 248   | k e ⇒ (blank S e)\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* ].
 249
 250 lemma forget_blank: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S.\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 S e| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 e.
 251 #S #e elim e normalize //
 252 qed.
 253
 254 lemma sem_blank: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S.\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 S e} \ 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.
 255 #S #e elim e
 256   [1,2:@\ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6 //
 257   |#s @\ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6 //
 258   |#e1 #e2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter7/sem_cat.def(8)"\ 6sem_cat\ 5/a\ 6
 259    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@(\ 5a href="cic:/matita/tutorial/chapter4/union_empty_r.def(3)"\ 6union_empty_r\ 5/a\ 6 … \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6)]
 260    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6[|@Hind2]] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6
 261    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@(\ 5a href="cic:/matita/tutorial/chapter6/cat_empty_l.def(5)"\ 6cat_empty_l\ 5/a\ 6 … ?)] @\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 @Hind1
 262   |#e1 #e2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter7/sem_plus.def(8)"\ 6sem_plus\ 5/a\ 6
 263    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@(\ 5a href="cic:/matita/tutorial/chapter4/union_empty_r.def(3)"\ 6union_empty_r\ 5/a\ 6 … \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6)]
 264    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6[|@Hind2]] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 @Hind1
 265   |#e #Hind >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6
 266    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@(\ 5a href="cic:/matita/tutorial/chapter6/cat_empty_l.def(5)"\ 6cat_empty_l\ 5/a\ 6 … ?)] @\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 @Hind
 267   ]
 268 qed.
 269
 270 theorem re_embedding: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S.
 271   \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 S e)} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e}.
 272 #S #e @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_bull.def(12)"\ 6sem_bull\ 5/a\ 6] >\ 5a href="cic:/matita/tutorial/chapter8/forget_blank.def(4)"\ 6forget_blank\ 5/a\ 6
 273 @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_blank.def(9)"\ 6sem_blank\ 5/a\ 6]]
 274 @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_comm.def(3)"\ 6union_comm\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/union_empty_r.def(3)"\ 6union_empty_r\ 5/a\ 6.
 275 qed.
 276
 277 (*
 278 \ 5h2\ 6Lifted Operators\ 5/h2\ 6
 279
 280 Plus and bullet have been already lifted from items to pres. We can now
 281 do a similar job for concatenation ⊙ and Kleene's star ⊛.*)
 282
 283 definition lifted_cat ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
 284   \ 5a href="cic:/matita/tutorial/chapter8/lift.def(2)"\ 6lift\ 5/a\ 6 S (\ 5a href="cic:/matita/tutorial/chapter8/pre_concat_l.def(3)"\ 6pre_concat_l\ 5/a\ 6 S \ 5a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"\ 6eclose\ 5/a\ 6 e).
 285
 286 notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
 287
 288 interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
 289
 290 lemma odot_true_b : ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀b.
 291   \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i2,b〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2)),\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b〉.
 292 #S #i1 #i2 #b normalize in ⊢ (??%?); cases (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i2) //
 293 qed.
 294
 295 lemma odot_false_b : ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀b.
 296   \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i2,b〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2 ,b〉.
 297 //
 298 qed.
 299
 300 lemma erase_odot:∀S.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
 301   \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 e2)| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e1| \ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e2|).
 302 #S * #i1 * * #i2 #b2 // >\ 5a href="cic:/matita/tutorial/chapter8/odot_true_b.def(6)"\ 6odot_true_b\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/erase_dot.def(4)"\ 6erase_dot\ 5/a\ 6 //
 303 qed.
 304
 305 (* Let us come to the star operation: *)
 306
 307 definition lk ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
 308   match e with
 309   [ mk_Prod i1 b1 ⇒
 310     match b1 with
 311     [true ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter8/eclose.fix(0,1,4)"\ 6eclose\ 5/a\ 6 ? i1))\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*, \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉
 312     |false ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉
 313     ]
 314   ].
 315
 316 (* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
 317 interpretation "lk" 'lk a = (lk ? a).
 318 notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
 319
 320 lemma ostar_true: ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 321   \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛ \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a title="eclose" href="cic:/fakeuri.def(1)"\ 6•\ 5/a\ 6i))\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*, \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉.
 322 // qed.
 323
 324 lemma ostar_false: ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 325   \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛ \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉.
 326 // qed.
 327
 328 lemma erase_ostar: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
 329   \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (e\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛)| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e|\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
 330 #S * #i * // qed.
 331
 332 lemma sem_odot_true: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e1:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.∀i.
 333   \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i} \ 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="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] }.
 334 #S #e1 #i
 335 cut (e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i), \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6(e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉) [//]
 336 #H >H cases (e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i) #i1 #b1 cases b1
 337   [>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6]
 338    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 339   |/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 340   ]
 341 qed.
 342
 343 lemma eq_odot_false: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e1:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.∀i.
 344   e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i.
 345 #S #e1 #i
 346 cut (e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i), \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6(e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉) [//]
 347 cases (e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i) #i1 #b1 cases b1 #H @H
 348 qed.
 349
 350 (* We conclude this section with the proof of the main semantic properties
 351 of ⊙ and ⊛. *)
 352
 353 lemma sem_odot:
 354   ∀S.∀e1,e2: \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 e2} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1}\ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e2|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2}.
 355 #S #e1 * #i2 *
 356   [>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6
 357    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/sem_odot_true.def(10)"\ 6sem_odot_true\ 5/a\ 6]
 358    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter8/sem_pcl_aux.def(11)"\ 6sem_pcl_aux\ 5/a\ 6 //
 359   |>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter8/eq_odot_false.def(6)"\ 6eq_odot_false\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter8/sem_pcl_aux.def(11)"\ 6sem_pcl_aux\ 5/a\ 6 //
 360   ]
 361 qed.
 362
 363 theorem sem_ostar: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
 364   \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61  \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e|}\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
 365 #S * #i #b cases b
 366   [>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter8/erase_bull.def(6)"\ 6erase_bull\ 5/a\ 6
 367    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6[|@\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter8/minus_eps_pre_aux.def(11)"\ 6minus_eps_pre_aux\ 5/a\ 6 //]]]
 368    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_r.def(3)"\ 6eqP_union_r\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6]]
 369    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6]
 370    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter4/union_assoc.def(3)"\ 6union_assoc\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6
 371    @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/epsilon_cat_l.def(5)"\ 6epsilon_cat_l\ 5/a\ 6] @\ 5a href="cic:/matita/tutorial/chapter4/eqP_sym.def(3)"\ 6eqP_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/star_fix_eps.def(7)"\ 6star_fix_eps\ 5/a\ 6
 372   |>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star.def(8)"\ 6sem_star\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter8/eq_to_ex_eq.def(4)"\ 6eq_to_ex_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 373   ]
 374 qed.