the transition was not parallel, now it is.
+ partial commit: component "rt_transition" corrected and minor bugs ficed
+ some additions in static_2 to support the correction
| cpg_cast : ∀cU,cT,G,L,U1,U2,T1,T2. Rt cU cT →
cpg Rt h cU G L U1 U2 → cpg Rt h cT G L T1 T2 →
cpg Rt h (cU∨cT) G L (ⓝU1.T1) (ⓝU2.T2)
-| cpg_zeta : ∀c,G,L,V,T1,T,T2. cpg Rt h c G (L.ⓓV) T1 T →
- ⬆*[1] T2 ≘ T → cpg Rt h (c+𝟙𝟘) G L (+ⓓV.T1) T2
+| cpg_zeta : ∀c,G,L,V,T1,T,T2. ⬆*[1] T ≘ T1 → cpg Rt h c G L T T2 →
+ cpg Rt h (c+𝟙𝟘) G L (+ⓓV.T1) T2
| cpg_eps : ∀c,G,L,V,T1,T2. cpg Rt h c G L T1 T2 → cpg Rt h (c+𝟙𝟘) G L (ⓝV.T1) T2
| cpg_ee : ∀c,G,L,V1,V2,T. cpg Rt h c G L V1 V2 → cpg Rt h (c+𝟘𝟙) G L (ⓝV1.T) V2
| cpg_beta : ∀cV,cW,cT,p,G,L,V1,V2,W1,W2,T1,T2.
∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 →
∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
U2 = ⓑ{p,J}V2.T2 & c = ((↕*cV)∨cT)
- | â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ U1 â¬\88[Rt, cT, h] T & â¬\86*[1] U2 â\89\98 T &
+ | â\88\83â\88\83cT,T. â¬\86*[1] T â\89\98 U1 & â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[Rt, cT, h] U2 &
p = true & J = Abbr & c = cT+𝟙𝟘.
#Rt #c #h #G #L #U #U2 * -c -G -L -U -U2
[ #I #G #L #q #J #W #U1 #H destruct
lemma cpg_inv_bind1: ∀Rt,c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[Rt, c, h] U2 →
∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
U2 = ⓑ{p,I}V2.T2 & c = ((↕*cV)∨cT)
- | â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[Rt, cT, h] T & â¬\86*[1] U2 â\89\98 T &
+ | â\88\83â\88\83cT,T. â¬\86*[1] T â\89\98 T1 & â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[Rt, cT, h] U2 &
p = true & I = Abbr & c = cT+𝟙𝟘.
/2 width=3 by cpg_inv_bind1_aux/ qed-.
lemma cpg_inv_abbr1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[Rt, c, h] U2 →
∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
U2 = ⓓ{p}V2.T2 & c = ((↕*cV)∨cT)
- | â\88\83â\88\83cT,T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[Rt, cT, h] T & â¬\86*[1] U2 â\89\98 T &
+ | â\88\83â\88\83cT,T. â¬\86*[1] T â\89\98 T1 & â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[Rt, cT, h] U2 &
p = true & c = cT+𝟙𝟘.
#Rt #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
/3 width=8 by ex4_4_intro, ex4_2_intro, or_introl, or_intror/
elim (IH … HV12 … HLK … HVW1) -HV12 //
elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip, ext2_pair/ ]
/3 width=5 by cpg_bind, lifts_bind, ex2_intro/
- | #cT #T2 #HT12 #HXT2 #H1 #H2 #H3 destruct
- elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip, ext2_pair/ ] #U2 #HTU2 #HU12
- lapply (lifts_trans … HXT2 … HTU2 ??) -T2 [3: |*: // ] #HXU2
- elim (lifts_split_trans … HXU2 f (𝐔❴↑O❵)) [2: /2 width=1 by after_uni_one_dx/ ]
+ | #cT #T2 #HT21 #HTX2 #H1 #H2 #H3 destruct
+ elim (lifts_trans4_one … HT21 … HTU1) -HTU1 #U2 #HTU2 #HU21
+ elim (IH … HTX2 … HLK … HTU2) [| /3 width=1 by fqup_zeta/ ] -K -V1 -T1 -T2
/3 width=5 by cpg_zeta, ex2_intro/
]
| * #V1 #T1 #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct
elim (IH … HW12 … HLK … HVW1) -HW12 //
elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip, ext2_pair/ ]
/3 width=5 by cpg_bind, lifts_bind, ex2_intro/
- | #cU #U2 #HU12 #HXU2 #H1 #H2 #H3 destruct
- elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip, ext2_pair/ ] #T2 #HTU2 #HT12
- elim (lifts_div4_one … HTU2 … HXU2) -U2 /3 width=5 by cpg_zeta, ex2_intro/
+ | #cU #U2 #HU21 #HUX2 #H1 #H2 #H3 destruct
+ elim (lifts_div4_one … HTU1 … HU21) -HTU1 #T2 #HT21 #HTU2
+ elim (IH … HUX2 … HLK … HTU2) [| /3 width=1 by fqup_zeta/ ] -L -W1 -U1 -U2
+ /3 width=5 by cpg_zeta, ex2_intro/
]
| * #W1 #U1 #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct
elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #HVW1 #HTU1 #H destruct
qed.
(* Basic_2A1: includes: cpr_zeta *)
-lemma cpm_zeta: ∀n,h,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[n, h] T →
- ⬆*[1] T2 ≘ T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡[n, h] T2.
-#n #h #G #L #V #T1 #T #T2 *
+lemma cpm_zeta (n) (h) (G) (L):
+ ∀T1,T. ⬆*[1] T ≘ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[n,h] T2 →
+ ∀V. ⦃G, L⦄ ⊢ +ⓓV.T1 ➡[n, h] T2.
+#n #h #G #L #T1 #T #HT1 #T2 *
/3 width=5 by cpg_zeta, isrt_plus_O2, ex2_intro/
qed.
qed-.
lemma cpm_inv_sort1: ∀n,h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡[n,h] T2 →
- â\88¨â\88¨ T2 = â\8b\86s â\88§ n = 0
- | T2 = ⋆(next h s) ∧ n = 1.
-#n #h #G #L #T2 #s * #c #Hc #H elim (cpg_inv_sort1 … H) -H *
-#H1 #H2 destruct
-/4 width=1 by isrt_inv_01, isrt_inv_00, or_introl, or_intror, conj/
+ â\88§â\88§ T2 = â\8b\86(((next h)^n) s) & n â\89¤ 1.
+#n #h #G #L #T2 #s * #c #Hc #H
+elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct
+[ lapply (isrt_inv_00 … Hc) | lapply (isrt_inv_01 … Hc) ] -Hc
+#H destruct /2 width=1 by conj/
qed-.
lemma cpm_inv_zero1: ∀n,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[n, h] T2 →
lemma cpm_inv_bind1: ∀n,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] U2 →
∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 &
U2 = ⓑ{p,I}V2.T2
- | â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡[n, h] T & â¬\86*[1] U2 â\89\98 T &
+ | â\88\83â\88\83T. â¬\86*[1] T â\89\98 T1 & â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡[n, h] U2 &
p = true & I = Abbr.
#n #h #p #I #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_bind1 … H) -H *
[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
/4 width=5 by ex3_2_intro, ex2_intro, or_introl/
-| #cT #T2 #HT12 #HUT2 #H1 #H2 #H3 destruct
- /5 width=3 by isrt_inv_plus_O_dx, ex4_intro, ex2_intro, or_intror/
+| #cT #T2 #HT21 #HTU2 #H1 #H2 #H3 destruct
+ /5 width=5 by isrt_inv_plus_O_dx, ex4_intro, ex2_intro, or_intror/
]
qed-.
lemma cpm_inv_abbr1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡[n, h] U2 →
∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T2 &
U2 = ⓓ{p}V2.T2
- | ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≘ T & p = true.
-#n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abbr1 … H) -H *
-[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
- elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
- elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
- /4 width=5 by ex3_2_intro, ex2_intro, or_introl/
-| #cT #T2 #HT12 #HUT2 #H1 #H2 destruct
- /5 width=3 by isrt_inv_plus_O_dx, ex3_intro, ex2_intro, or_intror/
+ | ∃∃T. ⬆*[1] T ≘ T1 & ⦃G, L⦄ ⊢ T ➡[n, h] U2 & p = true.
+#n #h #p #G #L #V1 #T1 #U2 #H
+elim (cpm_inv_bind1 … H) -H
+[ /3 width=1 by or_introl/
+| * /3 width=3 by ex3_intro, or_intror/
]
qed-.
lemma cpm_inv_abst1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡[n, h] U2 →
∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡[n, h] T2 &
U2 = ⓛ{p}V2.T2.
-#n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abst1 … H) -H
-#cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
-elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
-elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
-/3 width=5 by ex3_2_intro, ex2_intro/
+#n #h #p #G #L #V1 #T1 #U2 #H
+elim (cpm_inv_bind1 … H) -H
+[ /3 width=1 by or_introl/
+| * #T #_ #_ #_ #H destruct
+]
qed-.
(* Basic_1: includes: pr0_gen_appl pr2_gen_appl *)
Q 0 G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓐV1.T1) (ⓐV2.T2)
) → (∀n,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
Q n G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓝV1.T1) (ⓝV2.T2)
- ) â\86\92 (â\88\80n,G,L,V,T1,T,T2. â¦\83G, L.â\93\93Vâ¦\84 â\8a¢ T1 â\9e¡[n, h] T â\86\92 Q n G (L.â\93\93V) T1 T →
- ⬆*[1] T2 ≘ T → Q n G L (+ⓓV.T1) T2
+ ) â\86\92 (â\88\80n,G,L,V,T1,T,T2. â¬\86*[1] T â\89\98 T1 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡[n, h] T2 →
+ Q n G L T T2 → Q n G L (+ⓓV.T1) T2
) → (∀n,G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
Q n G L T1 T2 → Q n G L (ⓝV.T1) T2
) → (∀n,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 →
| #cU #cT #G #L #U1 #U2 #T1 #T2 #HUT #HU12 #HT12 #IHU #IHT #n #H
elim (isrt_inv_max_eq_t … H) -H // #HcV #HcT
/3 width=3 by ex2_intro/
-| #c #G #L #V #T1 #T2 #T #HT12 #HT2 #IH #n #H
+| #c #G #L #V #T1 #T #T2 #HT1 #HT2 #IH #n #H
lapply (isrt_inv_plus_O_dx … H ?) -H // #Hc
/3 width=4 by ex2_intro/
| #c #G #L #U #T1 #T2 #HT12 #IH #n #H
elim IHU [|*: // ] -IHU #U #HU1 #HU2
elim IHT [|*: // ] -IHT #T #HT1 #HT2
/3 width=5 by cpm_cast, ex2_intro/
-| #n #G #K #V #T1 #T2 #V2 #_ #IH #HVT2 #n1 #n2 #H destruct
+| #n #G #K #V #U1 #T1 #T2 #HTU1 #_ #IH #n1 #n2 #H destruct
elim IH [|*: // ] -IH #T #HT1 #HT2
- /3 width=6 by cpm_zeta, cpm_bind, ex2_intro/
+ /3 width=3 by cpm_zeta, ex2_intro/
| #n #G #L #U #T1 #T2 #_ #IH #n1 #n2 #H destruct
elim IH [|*: // ] -IH #T #HT1 #HT2
/3 width=3 by cpm_eps, ex2_intro/
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/syntax/tdeq.ma".
+include "basic_2/rt_transition/cpm_drops.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Inversion lemmas with degree-based equivalence for terms *****************)
+
+lemma cpm_tdeq_inv_lref (n) (h) (o) (G) (L) (i):
+ ∀X. ⦃G, L⦄ ⊢ #i ➡[n,h] X → #i ≛[h,o] X →
+ ∧∧ X = #i & n = 0.
+#n #h #o #G #L #i #X #H1 #H2
+lapply (tdeq_inv_lref1 … H2) -H2 #H destruct
+elim (cpm_inv_lref1_drops … H1) -H1 // * [| #m ]
+#K #V1 #V2 #_ #_ #H -V1
+elim (lifts_inv_lref2_uni_lt … H) -H //
+qed-.
(* Basic_1: includes: pr0_gen_sort pr2_gen_sort *)
lemma cpr_inv_sort1: ∀h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡[h] T2 → T2 = ⋆s.
-#h #G #L #T2 #s #H elim (cpm_inv_sort1 … H) -H * [ // ] #_ #H destruct
+#h #G #L #T2 #s #H elim (cpm_inv_sort1 … H) -H //
qed-.
lemma cpr_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[h] T2 →
Q G L V1 V2 → Q G (L.ⓑ{I}V1) T1 T2 → Q G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 →
Q G L V1 V2 → Q G L T1 T2 → Q G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
- ) â\86\92 (â\88\80G,L,V,T1,T,T2. â¦\83G, L.â\93\93Vâ¦\84 â\8a¢ T1 â\9e¡[h] T â\86\92 Q G (L.â\93\93V) T1 T →
- ⬆*[1] T2 ≘ T → Q G L (+ⓓV.T1) T2
+ ) â\86\92 (â\88\80G,L,V,T1,T,T2. â¬\86*[1] T â\89\98 T1 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡[h] T2 →
+ Q G L T T2 → Q G L (+ⓓV.T1) T2
) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → Q G L T1 T2 →
Q G L (ⓝV.T1) T2
) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h] T2 →
/3 width=5 by cpg_appl, cpg_cast, ex_intro/
qed.
-lemma cpx_zeta: ∀h,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T →
- ⬆*[1] T2 ≘ T → ⦃G, L⦄ ⊢ +ⓓV.T1 ⬈[h] T2.
-#h #G #L #V #T1 #T #T2 *
+lemma cpx_zeta (h) (G) (L):
+ ∀T1,T. ⬆*[1] T ≘ T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬈[h] T2 →
+ ∀V. ⦃G, L⦄ ⊢ +ⓓV.T1 ⬈[h] T2.
+#h #G #L #T1 #T #HT1 #T2 *
/3 width=4 by cpg_zeta, ex_intro/
qed.
lemma cpx_inv_bind1: ∀h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] U2 →
∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 &
U2 = ⓑ{p,I}V2.T2
- | â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[h] T & â¬\86*[1] U2 â\89\98 T &
+ | â\88\83â\88\83T. â¬\86*[1] T â\89\98 T1 & â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[h] U2 &
p = true & I = Abbr.
#h #p #I #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_bind1 … H) -H *
/4 width=5 by ex4_intro, ex3_2_intro, ex_intro, or_introl, or_intror/
lemma cpx_inv_abbr1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[h] U2 →
∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[h] T2 &
U2 = ⓓ{p}V2.T2
- | â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â¬\88[h] T & â¬\86*[1] U2 â\89\98 T & p = true.
+ | â\88\83â\88\83T. â¬\86*[1] T â\89\98 T1 & â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[h] U2 & p = true.
#h #p #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_abbr1 … H) -H *
/4 width=5 by ex3_2_intro, ex3_intro, ex_intro, or_introl, or_intror/
qed-.
Q G L V1 V2 → Q G (L.ⓑ{I}V1) T1 T2 → Q G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
Q G L V1 V2 → Q G L T1 T2 → Q G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
- ) â\86\92 (â\88\80G,L,V,T1,T,T2. â¦\83G, L.â\93\93Vâ¦\84 â\8a¢ T1 â¬\88[h] T â\86\92 Q G (L.â\93\93V) T1 T →
- ⬆*[1] T2 ≘ T → Q G L (+ⓓV.T1) T2
+ ) â\86\92 (â\88\80G,L,V,T1,T,T2. â¬\86*[1] T â\89\98 T1 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T â¬\88[h] T2 â\86\92 Q G L T T2 →
+ Q G L (+ⓓV.T1) T2
) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → Q G L T1 T2 →
Q G L (ⓝV.T1) T2
) → (∀G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → Q G L V1 V2 →
(* *)
(**************************************************************************)
-include "static_2/static/req.ma".
+include "static_2/static/req_drops.ma".
include "basic_2/rt_transition/rpx_fsle.ma".
(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
elim (req_inv_bind … H) -H /3 width=1 by cpx_bind/
| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H
elim (req_inv_flat … H) -H /3 width=1 by cpx_flat/
-| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IH #L1 #H
- elim (req_inv_bind … H) -H /3 width=3 by cpx_zeta/
+| #G #L2 #V2 #T1 #T #T2 #HT1 #_ #IH #L1 #H
+ elim (req_inv_bind … H) -H #HV2 #H
+ lapply (req_inv_lifts_bi … H (Ⓣ) … HT1) -H [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #HT
+ /3 width=3 by cpx_zeta/
| #G #L2 #W1 #T1 #T2 #_ #IH #L1 #H
elim (req_inv_flat … H) -H /3 width=1 by cpx_eps/
| #G #L2 #W1 #W2 #T1 #_ #IH #L1 #H
(* PARALLEL R-TRANSITION FOR FULL LOCAL ENVIRONMENTS ************************)
+definition IH_cpr_conf_lpr (h): relation3 genv lenv term ≝ λG,L,T.
+ ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
+ ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
+ ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0.
+
(* Main properties with context-sensitive parallel reduction for terms ******)
fact cpr_conf_lpr_atom_atom (h):
/2 width=3 by cpr_refl, ex2_intro/ qed-.
fact cpr_conf_lpr_atom_delta (h):
- ∀G,L0,i. (
- ∀L,T. ⦃G, L0, #i⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀G0,L0,i. (
+ ∀G,L,T. ⦃G0, L0, #i⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
∀K0,V0. ⬇*[i] L0 ≘ K0.ⓓV0 →
- ∀V2. ⦃G, K0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⬆*[↑i] V2 ≘ T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ #i ➡[h] T & ⦃G, L2⦄ ⊢ T2 ➡[h] T.
+ ∀V2. ⦃G0, K0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⬆*[↑i] V2 ≘ T2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ #i ➡[h] T & ⦃G0, L2⦄ ⊢ T2 ➡[h] T.
#h #G0 #L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
elim (lpr_drops_conf … HLK0 … HL01) -HL01 // #X1 #H1 #HLK1
elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
(* Basic_1: includes: pr0_delta_delta pr2_delta_delta *)
fact cpr_conf_lpr_delta_delta (h):
- ∀G,L0,i. (
- ∀L,T. ⦃G, L0, #i⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀G0,L0,i. (
+ ∀G,L,T. ⦃G0, L0, #i⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
∀K0,V0. ⬇*[i] L0 ≘ K0.ⓓV0 →
- ∀V1. ⦃G, K0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⬆*[↑i] V1 ≘ T1 →
+ ∀V1. ⦃G0, K0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⬆*[↑i] V1 ≘ T1 →
∀KX,VX. ⬇*[i] L0 ≘ KX.ⓓVX →
- ∀V2. ⦃G, KX⦄ ⊢ VX ➡[h] V2 → ∀T2. ⬆*[↑i] V2 ≘ T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[h] T & ⦃G, L2⦄ ⊢ T2 ➡[h] T.
+ ∀V2. ⦃G0, KX⦄ ⊢ VX ➡[h] V2 → ∀T2. ⬆*[↑i] V2 ≘ T2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ T1 ➡[h] T & ⦃G0, L2⦄ ⊢ T2 ➡[h] T.
#h #G0 #L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1
#KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
lapply (drops_mono … H … HLK0) -H #H destruct
qed-.
fact cpr_conf_lpr_bind_bind (h):
- ∀p,I,G,L0,V0,T0. (
- ∀L,T. ⦃G, L0, ⓑ{p,I}V0.T0⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀p,I,G0,L0,V0,T0. (
+ ∀G,L,T. ⦃G0, L0, ⓑ{p,I}V0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
- ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡[h] T1 →
- ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡[h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ ⓑ{p,I}V1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓑ{p,I}V2.T2 ➡[h] T.
+ ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0, L0.ⓑ{I}V0⦄ ⊢ T0 ➡[h] T1 →
+ ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⦃G0, L0.ⓑ{I}V0⦄ ⊢ T0 ➡[h] T2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ ⓑ{p,I}V1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓑ{p,I}V2.T2 ➡[h] T.
#h #p #I #G0 #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02
elim (IH … HV01 … HV02 … HL01 … HL02) //
qed-.
fact cpr_conf_lpr_bind_zeta (h):
- ∀G,L0,V0,T0. (
- ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀G0,L0,V0,T0. (
+ ∀G,L,T. ⦃G0, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
- ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡[h] T1 →
- â\88\80T2. â¦\83G, L0.â\93\93V0â¦\84 â\8a¢ T0 â\9e¡[h] T2 â\86\92 â\88\80X2. â¬\86*[1] X2 â\89\98 T2 â\86\92
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ +ⓓV1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ X2 ➡[h] T.
+ ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0, L0.ⓓV0⦄ ⊢ T0 ➡[h] T1 →
+ â\88\80T2. â¬\86*[1]T2 â\89\98 T0 â\86\92 â\88\80X2. â¦\83G0, L0â¦\84 â\8a¢ T2 â\9e¡[h] X2 â\86\92
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ +ⓓV1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ X2 ➡[h] T.
#h #G0 #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
-#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
-elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -V0 -T0 #T #HT1 #HT2
-elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … L2 … HXT2) -T2
-/3 width=3 by cpm_zeta, drops_refl, drops_drop, ex2_intro/
+#T2 #HT20 #X2 #HTX2 #L1 #HL01 #L2 #HL02
+elim (cpm_inv_lifts_sn … HT01 (Ⓣ) … L0 … HT20) -HT01 [| /3 width=1 by drops_refl, drops_drop/ ] #T #HT1 #HT2
+elim (IH … HT2 … HTX2 … HL01 … HL02) [| /2 width=1 by fqup_zeta/ ] -L0 -V0 -T0 -T2 #T2 #HT2 #HXT2
+/3 width=3 by cpm_zeta, ex2_intro/
qed-.
fact cpr_conf_lpr_zeta_zeta (h):
- ∀G,L0,V0,T0. (
- ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀G0,L0,V0,T0. (
+ ∀G,L,T. ⦃G0, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
- ∀T1. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡[h] T1 → ∀X1. ⬆*[1] X1 ≘ T1 →
- ∀T2. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡[h] T2 → ∀X2. ⬆*[1] X2 ≘ T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ X1 ➡[h] T & ⦃G, L2⦄ ⊢ X2 ➡[h] T.
-#h #G0 #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1
-#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
-elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -T0 #T #HT1 #HT2
-elim (cpm_inv_lifts_sn … HT1 (Ⓣ) … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1
-elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2
-lapply (lifts_inj … HT2 … HT1) -T #H destruct
+ ∀T1. ⬆*[1] T1 ≘ T0 → ∀X1. ⦃G0, L0⦄ ⊢ T1 ➡[h] X1 →
+ ∀T2. ⬆*[1] T2 ≘ T0 → ∀X2. ⦃G0, L0⦄ ⊢ T2 ➡[h] X2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ X1 ➡[h] T & ⦃G0, L2⦄ ⊢ X2 ➡[h] T.
+#h #G0 #L0 #V0 #T0 #IH #T1 #HT10 #X1 #HTX1
+#T2 #HT20 #X2 #HTX2 #L1 #HL01 #L2 #HL02
+lapply (lifts_inj … HT20 … HT10) -HT20 #H destruct
+elim (IH … HTX1 … HTX2 … HL01 … HL02) [| /2 width=1 by fqup_zeta/ ] -L0 -V0 -T0 -T1 #X #HX1 #HX2
/2 width=3 by ex2_intro/
qed-.
fact cpr_conf_lpr_flat_flat (h):
- ∀I,G,L0,V0,T0. (
- ∀L,T. ⦃G, L0, ⓕ{I}V0.T0⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀I,G0,L0,V0,T0. (
+ ∀G,L,T. ⦃G0, L0, ⓕ{I}V0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
- ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 →
- ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡[h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ ⓕ{I}V1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓕ{I}V2.T2 ➡[h] T.
+ ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0, L0⦄ ⊢ T0 ➡[h] T1 →
+ ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⦃G0, L0⦄ ⊢ T0 ➡[h] T2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ ⓕ{I}V1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓕ{I}V2.T2 ➡[h] T.
#h #I #G0 #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02
elim (IH … HV01 … HV02 … HL01 … HL02) //
qed-.
fact cpr_conf_lpr_flat_eps (h):
- ∀G,L0,V0,T0. (
- ∀L,T. ⦃G, L0, ⓝV0.T0⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀G0,L0,V0,T0. (
+ ∀G,L,T. ⦃G0, L0, ⓝV0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
- ∀V1,T1. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡[h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ ⓝV1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ T2 ➡[h] T.
+ ∀V1,T1. ⦃G0, L0⦄ ⊢ T0 ➡[h] T1 → ∀T2. ⦃G0, L0⦄ ⊢ T0 ➡[h] T2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ ⓝV1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ T2 ➡[h] T.
#h #G0 #L0 #V0 #T0 #IH #V1 #T1 #HT01
#T2 #HT02 #L1 #HL01 #L2 #HL02
elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0
qed-.
fact cpr_conf_lpr_eps_eps (h):
- ∀G,L0,V0,T0. (
- ∀L,T. ⦃G, L0, ⓝV0.T0⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀G0,L0,V0,T0. (
+ ∀G,L,T. ⦃G0, L0, ⓝV0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
- ∀T1. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡[h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[h] T & ⦃G, L2⦄ ⊢ T2 ➡[h] T.
+ ∀T1. ⦃G0, L0⦄ ⊢ T0 ➡[h] T1 → ∀T2. ⦃G0, L0⦄ ⊢ T0 ➡[h] T2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ T1 ➡[h] T & ⦃G0, L2⦄ ⊢ T2 ➡[h] T.
#h #G0 #L0 #V0 #T0 #IH #T1 #HT01
#T2 #HT02 #L1 #HL01 #L2 #HL02
elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0
qed-.
fact cpr_conf_lpr_flat_beta (h):
- ∀p,G,L0,V0,W0,T0. (
- ∀L,T. ⦃G, L0, ⓐV0.ⓛ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀p,G0,L0,V0,W0,T0. (
+ ∀G,L,T. ⦃G0, L0, ⓐV0.ⓛ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
- ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G, L0⦄ ⊢ ⓛ{p}W0.T0 ➡[h] T1 →
- ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀W2. ⦃G, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡[h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ ⓐV1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[h] T.
+ ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0, L0⦄ ⊢ ⓛ{p}W0.T0 ➡[h] T1 →
+ ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀W2. ⦃G0, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G0, L0.ⓛW0⦄ ⊢ T0 ➡[h] T2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ ⓐV1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[h] T.
#h #p #G0 #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H
#V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
elim (cpm_inv_abst1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
pr0_cong_upsilon_cong pr0_cong_upsilon_delta
*)
fact cpr_conf_lpr_flat_theta (h):
- ∀p,G,L0,V0,W0,T0. (
- ∀L,T. ⦃G, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀p,G0,L0,V0,W0,T0. (
+ ∀G,L,T. ⦃G0, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
- ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G, L0⦄ ⊢ ⓓ{p}W0.T0 ➡[h] T1 →
- ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀U2. ⬆*[1] V2 ≘ U2 →
- ∀W2. ⦃G, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡[h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ ⓐV1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[h] T.
+ ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0, L0⦄ ⊢ ⓓ{p}W0.T0 ➡[h] T1 →
+ ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀U2. ⬆*[1] V2 ≘ U2 →
+ ∀W2. ⦃G0, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G0, L0.ⓓW0⦄ ⊢ T0 ➡[h] T2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ ⓐV1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[h] T.
#h #p #G0 #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H
#V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
-elim (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #U #HVU #HU2
elim (cpm_inv_abbr1 … H) -H *
[ #W1 #T1 #HW01 #HT01 #H destruct
+ elim (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HVU2 [| /3 width=2 by drops_refl, drops_drop/ ] #U #HVU #HU2
elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/
elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0
/4 width=7 by cpm_bind, cpm_appl, cpm_theta, ex2_intro/
-| #T1 #HT01 #HXT1 #H destruct
- elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
- elim (cpm_inv_lifts_sn … HT1 (Ⓣ) … L1 … HXT1) -HXT1 /3 width=2 by drops_refl, drops_drop/
- /4 width=9 by cpm_appl, cpm_zeta, lifts_flat, ex2_intro/
+| #X0 #HXT0 #HX0 #H destruct
+ elim (cpm_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02 [| /3 width=2 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02
+ elim (IH … HX0 … HX02 … HL01 … HL02) [| /3 width=5 by fqup_strap1, fqu_drop/ ] -L0 -V0 -W0 -T0 #T #H1T #H2T
+ /4 width=8 by cpm_appl, cpm_zeta, lifts_flat, ex2_intro/
]
qed-.
fact cpr_conf_lpr_beta_beta (h):
- ∀p,G,L0,V0,W0,T0. (
- ∀L,T. ⦃G, L0, ⓐV0.ⓛ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀p,G0,L0,V0,W0,T0. (
+ ∀G,L,T. ⦃G0, L0, ⓐV0.ⓛ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
- ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀W1. ⦃G, L0⦄ ⊢ W0 ➡[h] W1 → ∀T1. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡[h] T1 →
- ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀W2. ⦃G, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡[h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{p}ⓝW1.V1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[h] T.
+ ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀W1. ⦃G0, L0⦄ ⊢ W0 ➡[h] W1 → ∀T1. ⦃G0, L0.ⓛW0⦄ ⊢ T0 ➡[h] T1 →
+ ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀W2. ⦃G0, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G0, L0.ⓛW0⦄ ⊢ T0 ➡[h] T2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ ⓓ{p}ⓝW1.V1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[h] T.
#h #p #G0 #L0 #V0 #W0 #T0 #IH #V1 #HV01 #W1 #HW01 #T1 #HT01
#V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
(* Basic_1: was: pr0_upsilon_upsilon *)
fact cpr_conf_lpr_theta_theta (h):
- ∀p,G,L0,V0,W0,T0. (
- ∀L,T. ⦃G, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ →
- ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
- ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 →
- ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0
+ ∀p,G0,L0,V0,W0,T0. (
+ ∀G,L,T. ⦃G0, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T
) →
- ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀U1. ⬆*[1] V1 ≘ U1 →
- ∀W1. ⦃G, L0⦄ ⊢ W0 ➡[h] W1 → ∀T1. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡[h] T1 →
- ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀U2. ⬆*[1] V2 ≘ U2 →
- ∀W2. ⦃G, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡[h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{p}W1.ⓐU1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[h] T.
+ ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀U1. ⬆*[1] V1 ≘ U1 →
+ ∀W1. ⦃G0, L0⦄ ⊢ W0 ➡[h] W1 → ∀T1. ⦃G0, L0.ⓓW0⦄ ⊢ T0 ➡[h] T1 →
+ ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀U2. ⬆*[1] V2 ≘ U2 →
+ ∀W2. ⦃G0, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G0, L0.ⓓW0⦄ ⊢ T0 ➡[h] T2 →
+ ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G0, L1⦄ ⊢ ⓓ{p}W1.ⓐU1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[h] T.
#h #p #G0 #L0 #V0 #W0 #T0 #IH #V1 #HV01 #U1 #HVU1 #W1 #HW01 #T1 #HT01
#V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
elim (cpr_inv_atom1_drops … H1) -H1
elim (cpr_inv_atom1_drops … H2) -H2
[ #H2 #H1 destruct
- /2 width=1 by cpr_conf_lpr_atom_atom/
+ @cpr_conf_lpr_atom_atom
| * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct
- /3 width=10 by cpr_conf_lpr_atom_delta/
+ @(cpr_conf_lpr_atom_delta … IH) -IH /width=6 by/
| #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct
- /4 width=10 by ex2_commute, cpr_conf_lpr_atom_delta/
+ @ex2_commute @(cpr_conf_lpr_atom_delta … IH) -IH /width=6 by/
| * #X #Y #V2 #z #H #HV02 #HVT2 #H2
* #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
- /3 width=17 by cpr_conf_lpr_delta_delta/
+ @(cpr_conf_lpr_delta_delta … IH) -IH /width=6 by/
]
| #p #I #V0 #T0 #HG #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
elim (cpm_inv_bind1 … H1) -H1 *
[ #V1 #T1 #HV01 #HT01 #H1
- | #T1 #HT01 #HXT1 #H11 #H12
+ | #T1 #HT10 #HTX1 #H11 #H12
]
elim (cpm_inv_bind1 … H2) -H2 *
[1,3: #V2 #T2 #HV02 #HT02 #H2
- |2,4: #T2 #HT02 #HXT2 #H21 #H22
+ |2,4: #T2 #HT20 #HTX2 #H21 #H22
] destruct
- [ /3 width=10 by cpr_conf_lpr_bind_bind/
- | /4 width=11 by ex2_commute, cpr_conf_lpr_bind_zeta/
- | /3 width=11 by cpr_conf_lpr_bind_zeta/
- | /3 width=12 by cpr_conf_lpr_zeta_zeta/
+ [ @(cpr_conf_lpr_bind_bind … IH) -IH /width=1 by/
+ | @ex2_commute @(cpr_conf_lpr_bind_zeta … IH) -IH /width=3 by/
+ | @(cpr_conf_lpr_bind_zeta … IH) -IH /width=3 by/
+ | @(cpr_conf_lpr_zeta_zeta … IH) -IH /width=3 by/
]
| #I #V0 #T0 #HG #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
elim (cpr_inv_flat1 … H1) -H1 *
|3,7,11,15: #p2 #V2 #Y2 #W2 #Z2 #T2 #HV02 #HYW2 #HZT2 #H21 #H22 #H23
|4,8,12,16: #p2 #V2 #U2 #Y2 #W2 #Z2 #T2 #HV02 #HVU2 #HYW2 #HZT2 #H21 #H22 #H23
] destruct
- [ /3 width=10 by cpr_conf_lpr_flat_flat/
- | /4 width=8 by ex2_commute, cpr_conf_lpr_flat_eps/
- | /4 width=12 by ex2_commute, cpr_conf_lpr_flat_beta/
- | /4 width=14 by ex2_commute, cpr_conf_lpr_flat_theta/
- | /3 width=8 by cpr_conf_lpr_flat_eps/
- | /3 width=7 by cpr_conf_lpr_eps_eps/
- | /3 width=12 by cpr_conf_lpr_flat_beta/
- | /3 width=13 by cpr_conf_lpr_beta_beta/
- | /3 width=14 by cpr_conf_lpr_flat_theta/
- | /3 width=17 by cpr_conf_lpr_theta_theta/
+ [ @(cpr_conf_lpr_flat_flat … IH) -IH /width=1 by/
+ | @ex2_commute @(cpr_conf_lpr_flat_eps … IH) -IH /width=1 by/
+ | @ex2_commute @(cpr_conf_lpr_flat_beta … IH) -IH /width=1 by/
+ | @ex2_commute @(cpr_conf_lpr_flat_theta … IH) -IH /width=3 by/
+ | @(cpr_conf_lpr_flat_eps … IH) -IH /width=1 by/
+ | @(cpr_conf_lpr_eps_eps … IH) -IH /width=1 by/
+ | @(cpr_conf_lpr_flat_beta … IH) -IH /width=1 by/
+ | @(cpr_conf_lpr_beta_beta … IH) -IH /width=1 by/
+ | @(cpr_conf_lpr_flat_theta … IH) -IH /width=3 by/
+ | @(cpr_conf_lpr_theta_theta … IH) -IH /width=3 by/
]
]
qed-.
| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
elim (cpx_inv_abbr1 … H) -H *
[ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/
- | #T2 #HT12 #HT2 #H destruct -IHV1
- /4 width=8 by lpx_pair, aaa_inv_lifts, drops_refl, drops_drop/
+ | #X1 #HXT1 #HX1 #H destruct -IHV1
+ elim (cpx_lifts_sn … HX1 (Ⓣ) … (L1.ⓓV1) … HXT1) -X1
+ /4 width=7 by lpx_pair, aaa_inv_lifts, drops_refl, drops_drop/
]
| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/static/rex_drops.ma".
+include "basic_2/rt_transition/cpx_drops.ma".
+include "basic_2/rt_transition/rpx.ma".
+
+(* UNBOUND PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS ***********)
+
+(* Properties with generic slicing for local environments *******************)
+
+lemma rpx_lifts_sn (h) (G): f_dedropable_sn (cpx h G).
+/3 width=6 by rex_liftable_dedropable_sn, cpx_lifts_sn/ qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+lemma rpx_inv_lifts_sn (h) (G): f_dropable_sn (cpx h G).
+/2 width=5 by rex_dropable_sn/ qed-.
+
+lemma rpx_inv_lifts_dx (h) (G): f_dropable_dx (cpx h G).
+/2 width=5 by rex_dropable_dx/ qed-.
+
+lemma rpx_inv_lifts_bi (h) (G):
+ ∀L1,L2,U. ⦃G,L1⦄ ⊢ ⬈[h,U] L2 → ∀b,f. 𝐔⦃f⦄ →
+ ∀K1,K2. ⬇*[b,f] L1 ≘ K1 → ⬇*[b,f] L2 ≘ K2 →
+ ∀T. ⬆*[f]T ≘ U → ⦃G,K1⦄ ⊢ ⬈[h,T] K2.
+/2 width=10 by rex_inv_lifts_bi/ qed-.
include "static_2/static/fsle_drops.ma".
include "static_2/static/rex_fsle.ma".
include "basic_2/rt_transition/rpx_length.ma".
+include "basic_2/rt_transition/rpx_drops.ma".
include "basic_2/rt_transition/rpx_fqup.ma".
(* UNBOUND PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS ***********)
[ #V1 #T1 #HV01 #HT01 #H destruct
lapply (rpx_fwd_length … HV0) #H0
/4 width=6 by fsle_bind_eq, fsle_fwd_pair_sn/
- | #T #HT #HXT #H1 #H2 destruct
+ | #T #H2T0 #HTX #H1 #H2 destruct
+ lapply (rpx_inv_lifts_bi … HT0 (Ⓣ) … H2T0) -HT0 [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #HT
lapply (rpx_fwd_length … HV0) #H0
- /3 width=8 by fsle_inv_lifts_sn/
+ /5 width=6 by fsle_bind_dx_dx, fsle_lifts_dx, fqup_zeta/
]
| #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct
elim (rex_inv_flat … HY) -HY #HV0 #HX0
(* *)
(**************************************************************************)
+include "static_2/static/rdeq_drops.ma".
include "static_2/static/rdeq_fqup.ma".
include "static_2/static/rdeq_rdeq.ma".
include "basic_2/rt_transition/rpx_fsle.ma".
elim (IHV … HV02 … HL01 … HL02) -IHV -HV02 -HL01 -HL02
elim (IHT … HT02 … H1 … H2) -L0 -V0 -T0
/3 width=5 by cpx_flat, tdeq_pair, ex2_intro/
-| #G #L0 #V0 #T0 #T1 #U1 #_ #IH #HUT1 #X0 #H0 #L1 #H1 #L2 #H2
- elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct
+| #G #L0 #V0 #U0 #T0 #T1 #HTU0 #_ #IH #X0 #H0 #L1 #H1 #L2 #H2
+ elim (tdeq_inv_pair1 … H0) -H0 #V2 #U2 #HV02 #HU02 #H destruct
elim (rpx_inv_bind … H1) -H1 #HL01 #H1
elim (rdeq_inv_bind … H2) -H2 #HL02 #H2
- lapply (rdeq_bind_repl_dx … H2 (BPair Abbr V2) ?) -H2 /2 width=1 by ext2_pair/ -HV02 #H2
+ lapply (rpx_inv_lifts_bi … H1 (Ⓣ) … HTU0) -H1 [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #H1
+ lapply (rdeq_inv_lifts_bi … H2 (Ⓣ) … HTU0) -H2 [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #H2
+ elim (tdeq_inv_lifts_sn … HU02 … HTU0) -U0 #T2 #HTU2 #HT02
elim (IH … HT02 … H1 … H2) -L0 -T0 #T #HT1
- elim (tdeq_inv_lifts_sn … HT1 … HUT1) -T1
/3 width=5 by cpx_zeta, ex2_intro/
| #G #L0 #V0 #T0 #T1 #_ #IH #X0 #H0 #L1 #H1 #L2 #H2
elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #_ #HT02 #H destruct
}
]
[ { "t-bound context-sensitive parallel rt-transition" * } {
- [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ]
+ [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_tdeq" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ]
}
]
[ { "unbound context-sensitive parallel rt-transition" * } {
[ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
- [ [ "for lenvs on referred entries" ] "rpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_fqup" + "rpx_fsle" + "rpx_rdeq" + "rpx_lpx" + "rpx_rpx" * ]
+ [ [ "for lenvs on referred entries" ] "rpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_drops" + "rpx_fqup" + "rpx_fsle" + "rpx_rdeq" + "rpx_lpx" + "rpx_rpx" * ]
[ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" "lpx_length" + "lpx_drops" + "lpx_fquq" + "lpx_fsle" + "lpx_rdeq" + "lpx_aaa" * ]
[ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
[ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_req" + "cpx_rdeq" + "cpx_fdeq" * ]
]
qed-.
+lemma lifts_trans4_one (f) (T1) (T2):
+ ∀T. ⬆*[1]T1 ≘ T → ⬆*[⫯f]T ≘ T2 →
+ ∃∃T0. ⬆*[f]T1 ≘ T0 & ⬆*[1]T0 ≘ T2.
+/4 width=6 by lifts_trans, lifts_split_trans, after_uni_one_dx/ qed-.
+
(* Basic_2A1: includes: lift_conf_O1 lift_conf_be *)
theorem lifts_conf: ∀f1,T,T1. ⬆*[f1] T ≘ T1 → ∀f,T2. ⬆*[f] T ≘ T2 →
∀f2. f2 ⊚ f1 ≘ f → ⬆*[f2] T1 ≘ T2.
lemma tdeq_inv_lifts_bi: ∀h,o. deliftable2_bi (tdeq h o).
/3 width=6 by tdeq_inv_lifts_sn, deliftable2_sn_bi/ qed-.
+
+lemma tdeq_lifts_inv_pair_sn (h) (o) (I) (f:rtmap):
+ ∀X,T. ⬆*[f]X ≘ T → ∀V. ②{I}V.T ≛[h,o] X → ⊥.
+#h #o #I #f #X #T #H elim H -f -X -T
+[ #f #s #V #H
+ elim (tdeq_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct
+| #f #i #j #_ #V #H
+ elim (tdeq_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct
+| #f #l #V #H
+ elim (tdeq_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct
+| #f #p #J #X1 #T1 #X2 #T2 #_ #_ #_ #IH2 #V #H
+ elim (tdeq_inv_pair1 … H) -H #Z1 #Z2 #_ #HZ2 #H destruct
+ /2 width=2 by/
+| #f #J #X1 #T1 #X2 #T2 #_ #_ #_ #IH2 #V #H
+ elim (tdeq_inv_pair1 … H) -H #Z1 #Z2 #_ #HZ2 #H destruct
+ /2 width=2 by/
+]
+qed-.
@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
qed-.
+(* Advanced properties ******************************************************)
+
+lemma fqup_zeta (b) (p) (I) (G) (K) (V):
+ ∀T1,T2. ⬆*[1]T2 ≘ T1 → ⦃G,K,ⓑ{p,I}V.T1⦄ ⊐+[b] ⦃G,K,T2⦄.
+/4 width=5 by fqup_strap2, fqu_fqup, fqu_drop/ qed.
+
(* Basic_2A1: removed theorems 1: fqup_drop *)
@(ex4_4_intro … Hf Hg) /2 width=4 by lveq_void_sn/ (**) (* explict constructor *)
qed-.
+lemma fsle_lifts_dx (L1) (L2):
+ |L1| ≤ |L2| → ∀T2,U2. ⬆*[1]T2 ≘ U2 →
+ ∀T1. ⦃L1,T1⦄ ⊆ ⦃L2,T2⦄ → ⦃L1,T1⦄ ⊆ ⦃L2.ⓧ,U2⦄.
+#L1 #L2 #HL21 #T2 #U2 #HTU2 #T1
+* #n #m #f #g #Hf #Hg #H2L #Hfg
+lapply (lveq_length_fwd_sn … H2L ?) // -HL21 #H destruct
+lapply (frees_lifts_SO (Ⓣ) (L2.ⓧ) … HTU2 … Hg)
+[ /3 width=4 by drops_refl, drops_drop/ ] -T2 #Hg
+@(ex4_4_intro … Hf Hg) /2 width=4 by lveq_void_dx/ (**) (* explict constructor *)
+qed-.
+
lemma fsle_lifts_SO_sn: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, V2⦄ →
∀W1. ⬆*[1] V1 ≘ W1 → ∀I1,I2. ⦃K1.ⓘ{I1}, W1⦄ ⊆ ⦃K2.ⓑ{I2}V2, #O⦄.
#K1 #K2 #HK #V1 #V2
lemma rdeq_inv_lifts_sn: ∀h,o. f_dropable_sn (cdeq h o).
/2 width=5 by rex_dropable_sn/ qed-.
-(* Note: missing in basic_2A1 *)
lemma rdeq_inv_lifts_dx: ∀h,o. f_dropable_dx (cdeq h o).
/2 width=5 by rex_dropable_dx/ qed-.
-(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
lemma rdeq_inv_lifts_bi: ∀h,o,L1,L2,U. L1 ≛[h, o, U] L2 → ∀b,f. 𝐔⦃f⦄ →
∀K1,K2. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 →
∀T. ⬆*[f] T ≘ U → K1 ≛[h, o, T] K2.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/static/rex_drops.ma".
+include "static_2/static/req.ma".
+
+(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
+
+(* Note: req_inv_lifts_dx missing in basic_2A1 *)
+
+(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
+lemma req_inv_lifts_bi: ∀L1,L2,U. L1 ≡[U] L2 → ∀b,f. 𝐔⦃f⦄ →
+ ∀K1,K2. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 →
+ ∀T. ⬆*[f] T ≘ U → K1 ≡[T] K2.
+/2 width=10 by rex_inv_lifts_bi/ qed-.
}
]
[ { "syntactic equivalence" * } {
- [ [ "for lenvs on referred entries" ] "req" + "( ? ≡[?] ? )" "req_fqup" + "req_fsle" * ]
+ [ [ "for lenvs on referred entries" ] "req" + "( ? ≡[?] ? )" "req_drops" + "req_fqup" + "req_fsle" * ]
}
]
[ { "generic extension of a context-sensitive relation" * } {
projects / helm.git / commitdiff