(* The language sem{e} associated with the regular expression e is inductively
defined by the following function: *)
-let rec in_l (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝
+let rec in_l (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '≝' expected (in [let_defs])"\ 6\ 5/span\ 6 S → Prop ≝
match r with
[ z ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
| e ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6}
-| s x ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) }
+| s x ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5span class="error" title="Parse error: [ident] or [term level 19] expected after [sym{] (in [term])"\ 6\ 5/span\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) }
| c r1 r2 ⇒ (in_l ? r1) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (in_l ? r2)
| o r1 r2 ⇒ (in_l ? r1) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (in_l ? r2)
| k r1 ⇒ (in_l ? r1) \ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*].
| ps x ⇒ \ 5a title="atom" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6x
| pp x ⇒ \ 5a title="atom" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6x
| pc E1 E2 ⇒ (forget ? E1) \ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (forget ? E2)
- | po E1 E2 ⇒ (forget ? E1) \ 5a title="re or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (forget ? E2)
+ | po E1 E2 ⇒ (forget ? E1) \ 5a title="re or" 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 (forget ? E2)
| pk E ⇒ (forget ? E)\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* ].
(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
| pp y1 ⇒ match i2 with [ pp y2 ⇒ y1\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=y2 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
| po i11 i12 ⇒ match i2 with
[ po i21 i22 ⇒ beqitem S i11 i21 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 beqitem S i12 i22
- | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
+ | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '|' or SYMBOL ']' expected (in [term])"\ 6\ 5/span\ 6]
| pc i11 i12 ⇒ match i2 with
[ pc i21 i22 ⇒ beqitem S i11 i21 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 beqitem S i12 i22
| _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i1 i2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X i1 i2.
(*
-\ 5h2\ 6Semantics of pointed regular expression\ 5/h2\ 6
+\ 5h2\ 6Semantics of pointed regular expressions\ 5/h2\ 6
The intuitive semantic of a point is to mark the position where
we should start reading the regular expression. The language associated
to a pre is the union of the languages associated with its points. *)
| pe ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
| ps _ ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
| pp x ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) }
-| pc r1 r2 ⇒ (in_pl ? r1) \ 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 href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"\ 6forget\ 5/a\ 6 ? r2} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (in_pl ? r2)
+| pc r1 r2 ⇒ (in_pl ? r1) \ 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 href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"\ 6forget\ 5/a\ 6 ? r2} \ 5a title="union" 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 (in_pl ? r2)
| po r1 r2 ⇒ (in_pl ? r1) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (in_pl ? r2)
| pk r1 ⇒ (in_pl ? r1) \ 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 href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"\ 6forget\ 5/a\ 6 ? r1}\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* ].
]
qed.
-lemma minus_eps_pre: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 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_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e}\ 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 ]}.
+lemma minus_eps_pre: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6\ 5span class="error" title="Parse error: [sym{] expected after [sym\sem ] (in [term])"\ 6\ 5/span\ 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_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e}\ 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 ]}.
#S * #i *
[>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 normalize in ⊢ (??%?); #w %
[/\ 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/And.con(0,1,2)"\ 6conj\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * // #H1 #H2 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 …H1 H2)]