nlet rec eq_list (A : setoid) (l1, l2 : list A) on l1 : CProp[0] ≝
match l1 with
-[ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ ? | _ ⇒ ? ]
-| cons x xs ⇒ match l2 with [ nil ⇒ ? | cons y ys ⇒ x = y ∧ eq_list ? xs ys]].
-##[ napply True|napply False|napply False]nqed.
+[ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ True | _ ⇒ False ]
+| cons x xs ⇒ match l2 with [ nil ⇒ False | cons y ys ⇒ x = y ∧ eq_list ? xs ys]].
ndefinition LIST : setoid → setoid.
#S; @(list S); @(eq_list S); ncases admit; nqed.
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
unification hint 0 ≔ S : setoid;
P1 ≟ refl ? (eq0 (LIST S)),
P2 ≟ sym ? (eq0 (LIST S)),
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ list T.
+unification hint 0 ≔ S,a,b;
+ R ≟ LIST S,
+ L ≟ (list S)
+(* -------------------------------------------- *) ⊢
+ eq_list S a b ≡ eq_rel L (eq0 R) a b.
+
notation "hvbox(hd break :: tl)"
right associative with precedence 47
for @{'cons $hd $tl}.
ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) = f (f x y) z.
-ninductive one : Type[0] ≝ unit : one.
-
-ndefinition force ≝
- λS:Type[2].λs:S.λT:Type[2].λt:T.λlock:one.
- match lock return λ_.Type[2] with [ unit ⇒ T].
-
-nlet rec lift (S:Type[2]) (s:S) (T:Type[2]) (t:T) (lock:one) on lock : force S s T t lock ≝
- match lock return λlock.force S s T t lock with [ unit ⇒ t ].
-
-ncoercion lift1 : ∀S:Type[1].∀s:S.∀T:Type[1].∀t:T.∀lock:one. force S s T t lock ≝ lift
- on s : ? to force ?????.
-
-ncoercion lift2 : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock ≝ lift
- on s : ? to force ?????.
-
-unification hint 0 ≔ R : setoid;
- TR ≟ setoid, MR ≟ (carr R), lock ≟ unit
-(* ---------------------------------------- *) ⊢
- setoid ≡ force ?(*Type[0]*) MR TR R lock.
-
-unification hint 0 ≔ R : setoid1;
- TR ≟ setoid1, MR ≟ (carr1 R), lock ≟ unit
-(* ---------------------------------------- *) ⊢
- setoid1 ≡ force ? MR TR R lock.
ntheorem associative_append: ∀A:setoid.associative (list A) (append A).
-#A;#x;#y;#z;nelim x[//|#a;#x1;#H;nnormalize;/2/]nqed.
+#A;#x;#y;#z;nelim x[ napply # |#a;#x1;#H;nnormalize;/2/]nqed.
interpretation "iff" 'iff a b = (iff a b).
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ bool.
+unification hint 0 ≔ a,b;
+ R ≟ BOOL,
+ L ≟ bool
+(* -------------------------------------------- *) ⊢
+ eq bool a b ≡ eq_rel L (eq0 R) a b.
+
nrecord Alpha : Type[1] ≝ {
acarr :> setoid;
eqb: acarr → acarr → bool;
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ (re T).
+unification hint 0 ≔ A,a,b;
+ R ≟ RE A,
+ L ≟ re A
+(* -------------------------------------------- *) ⊢
+ eq_re A a b ≡ eq_rel L (eq0 R) a b.
+
notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
-notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
+notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
interpretation "star" 'pk a = (k ? a).
interpretation "or" 'plus a b = (o ? a b).
notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
interpretation "epsilon" 'epsilon = (e ?).
-notation "0" non associative with precedence 90 for @{ 'empty }.
-interpretation "empty" 'empty = (z ?).
+notation "0" non associative with precedence 90 for @{ 'empty_r }.
+interpretation "empty" 'empty_r = (z ?).
notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }.
notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }.
nlet rec conjunct S (l : list (list S)) (L : lang S) on l: CProp[0] ≝
match l with [ nil ⇒ True | cons w tl ⇒ w ∈ L ∧ conjunct ? tl L ].
-
-ndefinition empty_set : ∀A.Ω^A ≝ λA.{ w | False }.
-notation "∅" non associative with precedence 90 for @{'emptyset}.
-interpretation "empty set" 'emptyset = (empty_set ?).
-
-(*
-notation "{}" non associative with precedence 90 for @{'empty_lang}.
-interpretation "empty lang" 'empty_lang = (empty_lang ?).
-*)
-
ndefinition sing_lang : ∀A:setoid.∀x:A.Ω^A ≝ λS.λx.{ w | x = w }.
interpretation "sing lang" 'singl x = (sing_lang ? x).
ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S ≝ pc on _p : pitem ? to ∀_:?.?.
interpretation "patom" 'ps a = (ps ? a).
interpretation "pepsilon" 'epsilon = (pe ?).
-interpretation "pempty" 'empty = (pz ?).
+interpretation "pempty" 'empty_r = (pz ?).
notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}.
nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi $E}.
interpretation "in_pl" 'L_pi E = (L_pi ? E).
-unification hint 0 ≔ S,a,b;
- R ≟ LIST S
-(* -------------------------------------------- *) ⊢
- eq_list S a b ≡ eq_rel (list S) (eq0 R) a b.
-
-notation > "B ⇒_0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
-notation > "B ⇒_1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
-notation "B ⇒\sub 0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
-notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
+(* The caml, as some patches for it *)
+ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
+unification hint 0 ≔ S : setoid, x,y;
+ SS ≟ LIST S,
+ TT ≟ setoid1_of_setoid SS
+(*-----------------------------------------*) ⊢
+ eq_list S x y ≡ eq_rel1 ? (eq1 TT) x y.
+
+unification hint 0 ≔ SS : setoid;
+ S ≟ carr SS,
+ TT ≟ setoid1_of_setoid (LIST SS)
+(*-----------------------------------------------------------------*) ⊢
+ list S ≡ carr1 TT.
-interpretation "unary morphism 0" 'umorph0 A B = (unary_morphism A B).
-interpretation "unary morphism 1" 'umorph1 A B = (unary_morphism1 A B).
+(* Ex setoid support *)
+nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP).
+ ∀y,z:T.y = z → (∀x.y=z → P x y = P x z) → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)).
+#S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed.
-ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
+notation "∑" non associative with precedence 90 for @{Sig ?????}.
-nlemma exists_is_morph: (* BUG *) ∀S,T:setoid.∀P: S ⇒_1 (T ⇒_1 (CProp[0]:?)).
- ∀y,z:S.y =_0 z → (Ex T (P y)) = (Ex T (P z)).
-#S T P y z E; @;
-##[ *; #x Px; @x; alias symbol "refl" (instance 4) = "refl".
- alias symbol "prop2" (instance 2) = "prop21".
- napply (. E^-1‡#); napply Px;
-##| *; #x Px; @x; napply (. E‡#); napply Px;##]
+nlemma test : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y → (Ex S (λw.ee x w ∧ True)) =_1 (Ex S (λw.ee y w ∧ True)).
+#S m x y E;
+napply (.=_1 (∑ E (λw,H.(H ╪_1 #)╪_1 #))).
+napply #.
nqed.
-ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
-#S; @; ##[ #P; napply (Ex ? P); ##| #P1 P2 E; @;
-*; #x; #H; @ x; nlapply (E x x ?); //; *; /2/;
-nqed.
-
-nlemma d : ∀S:Alpha.
- ∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.
- ∀x,y:list S.x = y →
- let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
- form x = form y.
- #S ee x y E;
- nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
-
- nnormalize;
- nlapply (exists_is_morph (list S) (list S) ? ?? E);
-
- nchange with (F x = F y);
- nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
- napply (.= † E);
- napply #.
+nlemma test2 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y →
+ (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
+#S m x y E;
+napply (.=_1 #╪_1(∑ E (λw,H.(H ╪_1 #) ╪_1 #))).
+napply #.
nqed.
-
-E : w = w2
-
-
- Σ(λx.(#‡E)‡#) : ∃x.x = w ∧ m → ∃x.x = w2 ∧ m
- λx.(#‡E)‡# : ∀x.x = w ∧ m → x = w2 ∧ m
-
-
-w;
-F ≟ ex_moprh ∘ G
-g ≟ fun11 G
-------------------------------
-ex (λx.g w x) ==?== fun11 F w
-
-x ⊢ fun11 ?h ≟ λw. ?g w x
-?G ≟ morphism_leibniz (T → S) ∘ ?h
-------------------------------
-(λw. (λx:T.?g w x)) ==?== fun11 ?G
-
-...
-x ⊢ fun11 ?h ==?== λw. eq x w ∧ m [w]
-(λw,x.eq x w ∧ m[w]) ==?== fun11 ?G
-ex (λx.?g w x) ==?== ex (λx.x = w ∧ m[w])
-
-ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
-#S; @; ##[ #P; napply (Ex ? P); ##| ncases admit. ##] nqed.
-
-ndefinition ex_morph1 : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
-#S; @; ##[ #P; napply (Ex ? (λx.P); ##| ncases admit. ##] nqed.
-
-
-nlemma d : ∀S:Alpha.
- ∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.
- ∀x,y:list S.x = y →
- let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
- form x = form y.
- #S ee x y E;
- nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
-
- nnormalize;
-
- nchange with (F x = F y);
- nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
- napply (.= † E);
- napply #.
+nlemma ex_setoid : ∀S:setoid.(S ⇒_1 CPROP) → setoid.
+#T P; @ (Ex T (λx:T.P x)); @;
+##[ #H1 H2; napply True |##*: //; ##]
nqed.
+unification hint 0 ≔ T,P ; S ≟ (ex_setoid T P) ⊢
+ Ex T (λx:T.P x) ≡ carr S.
-nlemma d : ∀S:Alpha.∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.∀x,y:list S.x = y →
- let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
- form x = form y.
- #S ee x y E;
- nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
-
- nnormalize;
-
- nchange with (F x = F y);
- nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
- napply (.= † E);
- napply #.
+nlemma test3 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y →
+ ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
+#S m x y E;
+napply (.=_1 (∑ E (λw,H.(H ╪_1 #) ╪_1 #)) ╪_1 #).
+napply #.
nqed.
-
-
-nlemma d : ∀S:Alpha.(setoid1_of_setoid (list S)) ⇒_1 CPROP.
- #S; napply (comp1_unary_morphisms ??? (ex_morph (list S)) ?);
- napply (eq1).
-
-
-
-(*
-ndefinition comp_ex : ∀X,S,T,K.∀P:X ⇒_1 (S ⇒_1 T).∀Pc : (S ⇒_1 T) ⇒_1 K. X ⇒_1 K.
- *)
+(* Ex setoid support end *)
ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
-#S r; @(𝐋\p r); #w1 w2 E; nelim r; /2/;
-##[ #x; @; #H; ##[ nchange in H ⊢ % with ([?]=?); napply ((.= H) E)]
- nchange in H ⊢ % with ([?]=?); napply ((.= H) E^-1);
+#S r; @(𝐋\p r); #w1 w2 E; nelim r;
+##[ /2/;
+##| /2/;
+##| #x; @; *;
+##| #x; @; #H; nchange in H with ([?] =_0 ?); ##[ napply ((.=_0 H) E); ##]
+ napply ((.=_0 H) E^-1);
##| #e1 e2 H1 H2;
nchange in match (w1 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
+ nchange in match (w2 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
napply (.= (#‡H2));
- napply (.= (Eexists ?? ? w1 w2 E)‡#);
-
-
- nchange in match (w2 ∈ 𝐋\p (?·?)) with (?∨?);
- napply (.=
-
-
- //; napply (trans ?? ??? H E);
- napply (trans (list S) (eq0 (LIST S)) ? [?] ?(*w1 [x] w2*) H E);
- nlapply (trans (list S) (eq0 (LIST S))).
-
-napply (.= H); nnormalize; nlapply (trans ? [x] w1 w2 E H); napply (.= ?) [napply (w1 = [x])] ##[##2: napply #; napply sym1; napply refl1 ]
-
+ napply (.=_1 (∑ E (λx1,H1.∑ E (λx2,H2.?)))╪_1 #); ##[
+ ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
+ @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
+ napply ( (X‡#)‡#); ##]
+ napply #;
+##| #e1 e2 H1 H2;
+ nnormalize in ⊢ (???%%);
+ napply (H1‡H2);
+##| #e H; nnormalize in ⊢ (???%%);
+ napply (.=_1 (∑ E (λx1,H1.∑ E (λx2,H2.?)))); ##[
+ ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
+ @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
+ napply ((X‡#)‡#); ##]
+ napply #;##]
+nqed.
+
+unification hint 0 ≔ S : Alpha,e : pitem S;
+ SS ≟ (list S),
+ X ≟ (mk_ext_powerclass SS (𝐋\p e) (ext_prop SS (L_pi_ext S e)))
+(*-----------------------------------------------------------------*)⊢
+ ext_carr SS X ≡ 𝐋\p e.
+
ndefinition epsilon ≝
λS:Alpha.λb.match b return λ_.lang S with [ true ⇒ { [ ] } | _ ⇒ ∅ ].
interpretation "L_pr" 'L_pi E = (L_pr ? E).
-nlemma append_eq_nil : ∀S:setoid.∀w1,w2:list S. w1 @ w2 = [ ] → w1 = [ ].
+nlemma append_eq_nil : ∀S:setoid.∀w1,w2:list S. [ ] = w1 @ w2 → w1 = [ ].
#S w1; ncases w1; //. nqed.
-
+
(* lemma 12 *)
nlemma epsilon_in_true : ∀S:Alpha.∀e:pre S. [ ] ∈ 𝐋\p e = (\snd e = true).
#S r; ncases r; #e b; @; ##[##2: #H; nrewrite > H; @2; /2/; ##] ncases b;//;
##| #r1 r2 H G; *; ##[##2: nassumption; ##]
##| #r1 r2 H1 H2; *; /2/ by {}]
*; #w1; *; #w2; *; *;
-##[ #defw1 H1 foo; napply H; napply (. #‡#); (append_eq_nil … defw1)^-1‡#);
-
- nrewrite > (append_eq_nil ? … w1 w2 …); /3/ by {};//;
+##[ #defw1 H1 foo; napply H;
+ napply (. (append_eq_nil ? ?? defw1)^-1╪_1#);
+ nassumption;
+##| #defw1 H1 foo; napply H;
+ napply (. (append_eq_nil ? ?? defw1)^-1╪_1#);
+ nassumption;
+##]
nqed.
-nlemma not_epsilon_lp : ∀S.∀e:pitem S. ¬ (𝐋\p e [ ]).
-#S e; nelim e; nnormalize; /2/ by nmk;
-##[ #; @; #; ndestruct;
-##| #r1 r2 n1 n2; @; *; /2/; *; #w1; *; #w2; *; *; #H;
- nrewrite > (append_eq_nil …H…); /2/;
-##| #r1 r2 n1 n2; @; *; /2/;
-##| #r n; @; *; #w1; *; #w2; *; *; #H;
- nrewrite > (append_eq_nil …H…); /2/;##]
+nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ([ ] ∈ (𝐋\p e)).
+#S e; nelim e; ##[##1,2,3,4: nnormalize;/2/]
+##[ #p1 p2 np1 np2; *; ##[##2: napply np2] *; #w1; *; #w2; *; *; #abs;
+ nlapply (append_eq_nil ??? abs); # defw1; #; napply np1;
+ napply (. defw1^-1╪_1#);
+ nassumption;
+##| #p1 p2 np1 np2; *; nchange with (¬?); //;
+##| #r n; *; #w1; *; #w2; *; *; #abs; #; napply n;
+ nlapply (append_eq_nil ??? abs); # defw1; #;
+ napply (. defw1^-1╪_1#);
+ nassumption;##]
nqed.
ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.
interpretation "lk" 'lk op a = (lk ? op a).
-notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
+notation > "a ^ ⊛" non associative with precedence 75 for @{'lk eclose $a}.
notation > "•" non associative with precedence 60 for @{eclose ?}.
nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
match E with
- [ pz ⇒ 〈 ∅, false 〉
+ [ pz ⇒ 〈 0, false 〉
| pe ⇒ 〈 ϵ, true 〉
| ps x ⇒ 〈 `.x, false 〉
| pp x ⇒ 〈 `.x, false 〉
ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
interpretation "reclose" 'eclose x = (reclose ? x).
-ndefinition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w.
-notation > "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
-notation "A =\sub 1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
-interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b).
-
-naxiom extP : ∀S.∀p,q:word S → Prop.(p =1 q) → p = q.
-
nlemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) = ϵ b1 ∪ ϵ b2. ##[##2: napply S]
-#S b1 b2; ncases b1; ncases b2; napply extP; #w; nnormalize; @; /2/; *; //; *;
+#S b1 b2; ncases b1; ncases b2;
+nchange in match (true || true) with true;
+nchange in match (true || false) with true;
+nchange in match (ϵ true) with {[]};
+nchange in match (ϵ false) with ∅;
+##[##1,4: napply ((cupID…)^-1);
+##| napply ((cup0 ? {[]})^-1);
+##| napply (.= (cup0 ? {[]})^-1); napply cupC; ##]
nqed.
-nlemma cupA : ∀S.∀a,b,c:word S → Prop.a ∪ b ∪ c = a ∪ (b ∪ c).
-#S a b c; napply extP; #w; nnormalize; @; *; /3/; *; /3/; nqed.
+(* XXX move somewere else *)
+ndefinition if': ∀A,B:CPROP. A = B → A → B.
+#A B; *; /2/. nqed.
-nlemma cupC : ∀S. ∀a,b:word S → Prop.a ∪ b = b ∪ a.
-#S a b; napply extP; #w; @; *; nnormalize; /2/; nqed.
+ncoercion if : ∀A,B:CPROP. ∀p:A = B. A → B ≝ if' on _p : eq_rel1 ???? to ∀_:?.?.
(* theorem 16: 2 *)
nlemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.𝐋\p (e1 ⊕ e2) = 𝐋\p e1 ∪ 𝐋\p e2.
#S r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2;
-nwhd in ⊢ (??(??%)?);
-nchange in ⊢(??%?) with (𝐋\p (e1 + e2) ∪ ϵ (b1 || b2));
-nchange in ⊢(??(??%?)?) with (𝐋\p (e1) ∪ 𝐋\p (e2));
-nrewrite > (epsilon_or S …); nrewrite > (cupA S (𝐋\p e1) …);
-nrewrite > (cupC ? (ϵ b1) …); nrewrite < (cupA S (𝐋\p e2) …);
-nrewrite > (cupC ? ? (ϵ b1) …); nrewrite < (cupA …); //;
+nwhd in ⊢ (???(??%)?);
+nchange in ⊢(???%?) with (𝐋\p (e1 + e2) ∪ ϵ (b1 || b2));
+nchange in ⊢(???(??%?)?) with (𝐋\p (e1) ∪ 𝐋\p (e2));
+napply (.=_1 #╪_1 (epsilon_or ???));
+napply (.=_1 (cupA…)^-1);
+napply (.=_1 (cupA…)╪_1#);
+napply (.=_1 (#╪_1(cupC…))╪_1#);
+napply (.=_1 (cupA…)^-1╪_1#);
+napply (.=_1 (cupA…));
+//;
nqed.
+FINQUI
+
+manca setoide per pair (e pre)
+
nlemma odotEt :
- ∀S.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = 〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
+ ∀S:Alpha.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = ?.〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
#S e1 e2 b2; nnormalize; ncases (•e2); //; nqed.
nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) = 𝐋\p e1 · 𝐋 .|e2| ∪ 𝐋\p e2. //; nqed.
-nlemma cup_dotD : ∀S.∀p,q,r:word S → Prop.(p ∪ q) · r = (p · r) ∪ (q · r).
+nlemma cup_dotD : ∀S.∀p,q,r:lang S.(p ∪ q) · r = (p · r) ∪ (q · r).
#S p q r; napply extP; #w; nnormalize; @;
##[ *; #x; *; #y; *; *; #defw; *; /7/ by or_introl, or_intror, ex_intro, conj;
##| *; *; #x; *; #y; *; *; /7/ by or_introl, or_intror, ex_intro, conj; ##]
nqed.
-nlemma cup0 :∀S.∀p:word S → Prop.p ∪ {} = p.
-#S p; napply extP; #w; nnormalize; @; /2/; *; //; *; nqed.
nlemma erase_dot : ∀S.∀e1,e2:pitem S.𝐋 .|e1 · e2| = 𝐋 .|e1| · 𝐋 .|e2|.
#S e1 e2; napply extP; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj;
projects / helm.git / blobdiff