<page xmlns="http://lambdadelta.info/"
description = "BTM"
title = "BTM"
+ logo = "crux"
head = "cic:/matita/BTM/"
>
<section>Character classes</section>
<page xmlns="http://lambdadelta.info/"
description = "\lambda\delta home page"
title = "\lambda\delta home page"
+ logo = "crux"
head = "cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)"
>
<sitemap name="sitemap"/>
(* Inversion lemmas with test for uniformity ********************************)
lemma drops_inv_isuni: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐔⦃f⦄ →
- (𝐈⦃f⦄ ∧ L2 = L1) ∨
- ∃∃I,K,V,g. ⬇*[Ⓣ, g] K ≡ L2 & L1 = K.ⓑ{I}V & f = ⫯g.
+ (𝐈⦃f⦄ ∧ L1 = L2) ∨
+ ∃∃I,K,V,g. ⬇*[Ⓣ, g] K ≡ L2 & 𝐔⦃g⦄ & L1 = K.ⓑ{I}V & f = ⫯g.
#L1 #L2 #f * -L1 -L2 -f
[ /4 width=1 by or_introl, conj/
-| /4 width=7 by ex3_4_intro, or_intror/
+| /4 width=8 by isuni_inv_next, ex4_4_intro, or_intror/
| /7 width=6 by drops_fwd_isid, lifts_fwd_isid, isuni_inv_push, isid_push, or_introl, conj, eq_f3, sym_eq/
]
qed-.
(* Basic_2A1: was: drop_inv_O1_pair1 *)
lemma drops_inv_pair1_isuni: ∀I,K,L2,V,c,f. 𝐔⦃f⦄ → ⬇*[c, f] K.ⓑ{I}V ≡ L2 →
(𝐈⦃f⦄ ∧ L2 = K.ⓑ{I}V) ∨
- ∃∃g. ⬇*[c, g] K ≡ L2 & f = ⫯g.
+ ∃∃g. 𝐔⦃g⦄ & ⬇*[c, g] K ≡ L2 & f = ⫯g.
#I #K #L2 #V #c #f #Hf #H elim (isuni_split … Hf) -Hf * #g #Hg #H0 destruct
[ lapply (drops_inv_skip1 … H) -H * #Y #X #HY #HX #H destruct
<(drops_fwd_isid … HY Hg) -Y >(lifts_fwd_isid … HX Hg) -X
/4 width=3 by isid_push, or_introl, conj/
-| lapply (drops_inv_drop1 … H) -H /3 width=3 by ex2_intro, or_intror/
+| lapply (drops_inv_drop1 … H) -H /3 width=4 by ex3_intro, or_intror/
]
qed-.
(* Basic_2A1: was: drop_inv_O1_pair2 *)
lemma drops_inv_pair2_isuni: ∀I,K,V,c,f,L1. 𝐔⦃f⦄ → ⬇*[c, f] L1 ≡ K.ⓑ{I}V →
(𝐈⦃f⦄ ∧ L1 = K.ⓑ{I}V) ∨
- ∃∃I1,K1,V1,g. ⬇*[c, g] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & f = ⫯g.
+ ∃∃I1,K1,V1,g. 𝐔⦃g⦄ & ⬇*[c, g] K1 ≡ K.ⓑ{I}V & L1 = K1.ⓑ{I1}V1 & f = ⫯g.
#I #K #V #c #f *
[ #Hf #H elim (drops_inv_atom1 … H) -H #H destruct
| #L1 #I1 #V1 #Hf #H elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
[ #Hf #H destruct /3 width=1 by or_introl, conj/
- | /3 width=7 by ex3_4_intro, or_intror/
+ | /3 width=8 by ex4_4_intro, or_intror/
]
]
qed-.
(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************)
-(* Properties concerning atomic arity assignment ****************************)
+(* Properties with atomic arity assignment **********************************)
lemma lsuba_aaa_conf: ∀G,L1,V,A. ⦃G, L1⦄ ⊢ V ⁝ A →
∀L2. G ⊢ L1 ⫃⁝ L2 → ⦃G, L2⦄ ⊢ V ⁝ A.
#G #L1 #V #A #H elim H -G -L1 -V -A
[ //
-| #I #G #L1 #K1 #V #A #i #HLK1 #HV #IHV #L2 #HL12
- elim (lsuba_drop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
- elim (lsuba_inv_pair1 … H) -H * #K2
- [ #HK12 #H destruct /3 width=5 by aaa_lref/
- | #W0 #V0 #A0 #HV0 #HW0 #_ #H1 #H2 #H3 destruct
- lapply (aaa_mono … HV0 … HV) #H destruct -V0 /2 width=5 by aaa_lref/
- ]
+| #I #G #L1 #V #A #HA #IH #L2 #H
+ elim (lsuba_inv_pair1 … H) -H * /3 width=1 by aaa_zero/
+ #L0 #W0 #V0 #A0 #HV0 #HW0 #HL10 #H1 #H2 #H3 destruct
+ lapply (aaa_mono … HV0 … HA) #H destruct -V0 -L1 /2 width=1 by aaa_zero/
+| #I #G #K1 #V #A #i #_ #IH #L2 #H
+ elim (lsuba_inv_pair1 … H) -H * /3 width=1 by aaa_lref/
| /4 width=2 by lsuba_pair, aaa_abbr/
| /4 width=1 by lsuba_pair, aaa_abst/
| /3 width=3 by aaa_appl/
∀L1. G ⊢ L1 ⫃⁝ L2 → ⦃G, L1⦄ ⊢ V ⁝ A.
#G #L2 #V #A #H elim H -G -L2 -V -A
[ //
-| #I #G #L2 #K2 #V #A #i #HLK2 #H1V #IHV #L1 #HL12
- elim (lsuba_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsuba_inv_pair2 … H) -H * #K1
- [ #HK12 #H destruct /3 width=5 by aaa_lref/
- | #V0 #A0 #HV0 #H2V #_ #H1 #H2 destruct
- lapply (aaa_mono … H2V … H1V) #H destruct -K2 /2 width=5 by aaa_lref/
- ]
+| #I #G #L2 #V #A #HA #IH #L1 #H
+ elim (lsuba_inv_pair2 … H) -H * /3 width=1 by aaa_zero/
+ #L0 #V0 #A0 #HV0 #HV #HL02 #H1 #H2 destruct
+ lapply (aaa_mono … HV … HA) #H destruct -L2 /2 width=1 by aaa_zero/
+| #I #G #K2 #V #A #i #_ #IH #L1 #H
+ elim (lsuba_inv_pair2 … H) -H * /3 width=1 by aaa_lref/
| /4 width=2 by lsuba_pair, aaa_abbr/
| /4 width=1 by lsuba_pair, aaa_abst/
| /3 width=3 by aaa_appl/
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lrsubeqa_3.ma".
-include "basic_2/static/lsubr.ma".
-include "basic_2/static/aaa.ma".
+include "basic_2/relocation/drops.ma".
+include "basic_2/static/lsuba.ma".
(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************)
-(* Basic properties *********************************************************)
+(* Properties with generic slicing for local environments *******************)
-(* Note: the constant 0 cannot be generalized *)
-lemma lsuba_drop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K1,c,k. ⬇[c, 0, k] L1 ≡ K1 →
- ∃∃K2. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L2 ≡ K2.
+(* Note: the premise 𝐔⦃f⦄ cannot be removed *)
+(* Basic_2A1: includes: lsuba_drop_O1_conf *)
+lemma lsuba_drops_conf_isuni: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 →
+ ∀K1,c,f. 𝐔⦃f⦄ → ⬇*[c, f] L1 ≡ K1 →
+ ∃∃K2. G ⊢ K1 ⫃⁝ K2 & ⬇*[c, f] L2 ≡ K2.
#G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #_ #IHL12 #K1 #c #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
- [ destruct
- elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/
- | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
+| #I #L1 #L2 #V #HL12 #IH #K1 #c #f #Hf #H
+ elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by lsuba_pair, drops_refl, ex2_intro/
+ | #g #Hg #HLK1 #H destruct -HL12
+ elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
]
-| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K1 #c #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
- [ destruct
- elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/
- | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
+| #L1 #L2 #W #V #A #HV #HW #HL12 #IH #K1 #c #f #Hf #H
+ elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by drops_refl, lsuba_beta, ex2_intro/
+ | #g #Hg #HLK1 #H destruct -HL12
+ elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
]
]
qed-.
-(* Note: the constant 0 cannot be generalized *)
-lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 →
- ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L1 ≡ K1.
+(* Note: the premise 𝐔⦃f⦄ cannot be removed *)
+(* Basic_2A1: includes: lsuba_drop_O1_trans *)
+lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 →
+ ∀K2,c,f. 𝐔⦃f⦄ → ⬇*[c, f] L2 ≡ K2 →
+ ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇*[c, f] L1 ≡ K1.
#G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #_ #IHL12 #K2 #c #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
- [ destruct
- elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/
- | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
+| #I #L1 #L2 #V #HL12 #IH #K2 #c #f #Hf #H
+ elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by lsuba_pair, drops_refl, ex2_intro/
+ | #g #Hg #HLK2 #H destruct -HL12
+ elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
]
-| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K2 #c #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
- [ destruct
- elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/
- | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
+| #L1 #L2 #W #V #A #HV #HW #HL12 #IH #K2 #c #f #Hf #H
+ elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by drops_refl, lsuba_beta, ex2_intro/
+ | #g #Hg #HLK2 #H destruct -HL12
+ elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
]
]
qed-.
(* Main properties **********************************************************)
-theorem lsuba_trans: ∀G,L1,L. G ⊢ L1 ⫃⁝ L → ∀L2. G ⊢ L ⫃⁝ L2 → G ⊢ L1 ⫃⁝ L2.
+theorem lsuba_trans: ∀G. Transitive … (lsuba G).
#G #L1 #L #H elim H -L1 -L
[ #X #H >(lsuba_inv_atom1 … H) -H //
| #I #L1 #L #Y #HL1 #IHL1 #X #H
#L1 #L2 #H elim H -L1 -L2
[ #L #I #K2 #W #c #f #_ #H
elim (drops_inv_atom1 … H) -H #H destruct
-| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #c #f #Hf #H
- elim (drops_inv_pair1_isuni … Hf H) -H * #g #HLK2 try #H destruct [ -IHL12 | -HL12 ]
- [ /4 width=4 by drops_refl, ex2_intro, or_introl/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 /2 width=3 by isuni_inv_next/ *
+| #J #L1 #L2 #V #HL12 #IH #I #K2 #W #c #f #Hf #H
+ elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /4 width=4 by drops_refl, ex2_intro, or_introl/
+ | #g #Hg #HLK2 #H destruct -HL12
+ elim (IH … Hg HLK2) -IH -Hg -HLK2 *
/4 width=4 by drops_drop, ex3_2_intro, ex2_intro, or_introl, or_intror/
]
-| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #c #f #Hf #H
- elim (drops_inv_pair1_isuni … Hf H) -H * #g #HLK2 try #H destruct [ -IHL12 | -HL12 ]
- [ /4 width=4 by drops_refl, ex3_2_intro, or_intror/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 /2 width=3 by isuni_inv_next/ *
+| #L1 #L2 #V1 #V2 #HL12 #IH #I #K2 #W #c #f #Hf #H
+ elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /4 width=4 by drops_refl, ex3_2_intro, or_intror/
+ | #g #Hg #HLK2 #H destruct -HL12
+ elim (IH … Hg HLK2) -IH -Hg -HLK2 *
/4 width=4 by drops_drop, ex3_2_intro, ex2_intro, or_introl, or_intror/
]
]
<subsection name="A2">Stage "A2": "Extending the Applicability Condition"</subsection>
+ <news class="alpha" date="2016 April 16.">
+ Grammatical component reconstructed:
+ grammar, relocation, s_transition, s_computation, static
+ (anniversary milestone).
+ </news>
+
<news class="alpha" date="2016 March 25.">
Relocation with reference transforming maps (rtmap).
</news>
[ "sh" "sd" * ]
}
]
-(*
- [ { "local env. ref. for atomic arity assignment" * } {
- [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_aaa" + "lsuba_lsuba" * ]
+ [ { "restricted ref. for atomic arity assignment" * } {
+ [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
}
]
[ { "atomic arity assignment" * } {
- [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_fqus" + "aaa_lleq" + "aaa_aaa" * ]
+ [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + (* "aaa_lleq" + *) "aaa_aaa" * ]
}
]
-*)
[ { "restricted ref. for local env." * } {
[ "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ]
}
projects / helm.git / commitdiff