∃∃U0. ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
⦃G, L⦄ ⊢ U ➡*[h] U0 & ⦃G, L⦄ ⊢ T ➡*[1, h] U0.
/2 width=3 by cnv_inv_cast_aux/ qed-.
+
+(* Basic_2A1: removed theorems 6:
+ snv_fwd_da snv_fwd_lstas snv_cast_scpes
+ shnv_cast shnv_inv_cast snv_shnv_cast
+*)
--- /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 "basic_2/rt_transition/lpr_lpr.ma".
+include "basic_2/rt_computation/cpms_lsubr.ma".
+include "basic_2/rt_computation/cpms_fpbg.ma".
+include "basic_2/rt_computation/cpms_cpms.ma".
+include "basic_2/dynamic/cnv_drops.ma".
+include "basic_2/dynamic/cnv_preserve_far.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Far diamond propery with t-bound rt-transition for terms *****************)
+
+fact cnv_cpm_conf_lpr_atom_atom_aux (h) (G) (L1) (L2) (I):
+ ∃∃T. ⦃G,L1⦄ ⊢ ⓪{I} ➡*[0,h] T & ⦃G, L2⦄ ⊢ ⓪{I} ➡*[O,h] T.
+/2 width=3 by ex2_intro/ qed-.
+
+fact cnv_cpm_conf_lpr_atom_ess_aux (h) (G) (L1) (L2) (s):
+ ∃∃T. ⦃G,L1⦄ ⊢ ⋆s ➡*[1,h] T & ⦃G,L2⦄ ⊢ ⋆(next h s) ➡*[h] T.
+/3 width=3 by cpm_cpms, ex2_intro/ qed-.
+
+fact cnv_cpm_conf_lpr_atom_delta_aux (a) (h) (o) (G) (L) (i):
+ (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄⊢#i![a,h] →
+ ∀K,V. ⬇*[i]L ≘ K.ⓓV →
+ ∀n,XV. ⦃G,K⦄ ⊢ V ➡[n,h] XV →
+ ∀X. ⬆*[↑i]XV ≘ X →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T.
+#a #h #o #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2
+lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV
+elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
+elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK1 #HV1 #H destruct
+elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
+elim (lpr_inv_pair_sn … H2) -H2 #K2 #V2 #HK2 #_ #H destruct
+lapply (drops_isuni_fwd_drop2 … HLK2) -V2 // #HLK2
+lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
+elim (cnv_cpm_conf_lpr_far … IH … HV1 … HVX … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V
+<minus_O_n <minus_n_O #V #HV1 #HVX
+elim (cpms_lifts_sn … HVX … HLK2 … HXV) -XV -HLK2 #XV #HVX #HXV
+/3 width=6 by cpms_delta_drops, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_atom_ell_aux (a) (h) (o) (G) (L) (i):
+ (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄⊢#i![a,h] →
+ ∀K,W. ⬇*[i]L ≘ K.ⓛW →
+ ∀n,XW. ⦃G,K⦄ ⊢ W ➡[n,h] XW →
+ ∀X. ⬆*[↑i]XW ≘ X →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[↑n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T.
+#a #h #o #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2
+lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HW
+elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
+elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK1 #HW1 #H destruct
+elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
+elim (lpr_inv_pair_sn … H2) -H2 #K2 #W2 #HK2 #_ #H destruct
+lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2
+lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
+elim (cnv_cpm_conf_lpr_far … IH … HW1 … HWX … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -W
+<minus_O_n <minus_n_O #W #HW1 #HWX
+elim (cpms_lifts_sn … HWX … HLK2 … HXW) -XW -HLK2 #XW #HWX #HXW
+/3 width=6 by cpms_ell_drops, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_delta_delta_aux (a) (h) (o) (I) (G) (L) (i):
+ (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄⊢#i![a,h] →
+ ∀K1,V1. ⬇*[i]L ≘ K1.ⓑ{I}V1 → ∀K2,V2. ⬇*[i]L ≘ K2.ⓑ{I}V2 →
+ ∀n1,XV1. ⦃G,K1⦄ ⊢ V1 ➡[n1,h] XV1 → ∀n2,XV2. ⦃G,K2⦄ ⊢ V2 ➡[n2,h] XV2 →
+ ∀X1. ⬆*[↑i]XV1 ≘ X1 → ∀X2. ⬆*[↑i]XV2 ≘ X2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ X1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ X2 ➡*[n1-n2,h] T.
+#a #h #o #I #G #L #i #IH #HT
+#K #V #HLK #Y #X #HLY #n1 #XV1 #HVX1 #n2 #XV2 #HVX2 #X1 #HXV1 #X2 #HXV2
+#L1 #HL1 #L2 #HL2
+lapply (drops_mono … HLY … HLK) -HLY #H destruct
+lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV
+elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
+elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK1 #_ #H destruct
+lapply (drops_isuni_fwd_drop2 … HLK1) -V1 // #HLK1
+elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
+elim (lpr_inv_pair_sn … H2) -H2 #K2 #V2 #HK2 #_ #H destruct
+lapply (drops_isuni_fwd_drop2 … HLK2) -V2 // #HLK2
+lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
+elim (cnv_cpm_conf_lpr_far … IH … HVX1 … HVX2 … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V
+#V #HVX1 #HVX2
+elim (cpms_lifts_sn … HVX1 … HLK1 … HXV1) -XV1 -HLK1 #W1 #HVW1 #HXW1
+/3 width=11 by cpms_lifts_bi, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_delta_ell_aux (L) (K1) (K2) (V) (W) (i):
+ ⬇*[i]L ≘ K1.ⓓV → ⬇*[i]L ≘ K2.ⓛW → ⊥.
+#L #K1 #K2 #V #W #i #HLK1 #HLK2
+lapply (drops_mono … HLK2 … HLK1) -L -i #H destruct
+qed-.
+
+fact cnv_cpm_conf_lpr_bind_bind_aux (a) (h) (o) (p) (I) (G) (L) (V) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓑ{p,I}V.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓑ{p,I}V.T ![a,h] →
+ ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
+ ∀n1,T1. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n2,h] T2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ ⓑ{p,I}V1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓑ{p,I}V2.T2 ➡*[n1-n2,h] T.
+#a #h #o #p #I #G0 #L0 #V0 #T0 #IH #H0
+#V1 #HV01 #V2 #HV02 #n1 #T1 #HT01 #n2 #T2 #HT02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
+elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
+elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+#T #HT1 #HT2 -L0 -V0 -T0
+/3 width=5 by cpms_bind_dx, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_bind_zeta_aux (a) (h) (o) (G) (L) (V) (T):
+ (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] →
+ ∀V1. ⦃G,L⦄ ⊢V ➡[h] V1 →
+ ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓV⦄ ⊢ T ➡[n2,h] T2 →
+ ∀XT2. ⬆*[1]XT2 ≘ T2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ +ⓓV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T.
+#a #h #o #G0 #L0 #V0 #T0 #IH #H0
+#V1 #HV01 #n1 #T1 #HT01 #n2 #T2 #HT02 #XT2 #HXT2
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_bind … H0) -H0 #_ #HT0
+elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ] -L0 -T0 -V0
+#T #HT1 #HT2
+elim (cpms_inv_lifts_sn … HT2 (Ⓣ) … L2 … HXT2) -T2 [| /3 width=1 by drops_refl, drops_drop/ ] #XT #HXT #HXT2
+/3 width=3 by cpms_zeta, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_zeta_zeta_aux (a) (h) (o) (G) (L) (V) (T):
+ (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] →
+ ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓV⦄ ⊢ T ➡[n2,h] T2 →
+ ∀XT1. ⬆*[1]XT1 ≘ T1 → ∀XT2. ⬆*[1]XT2 ≘ T2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ XT1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T.
+#a #h #o #G0 #L0 #V0 #T0 #IH #H0
+#n1 #T1 #HT01 #n2 #T2 #HT02 #XT1 #HXT1 #XT2 #HXT2
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_bind … H0) -H0 #_ #HT0
+elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ] -L0 -T0
+#T #HT1 #HT2
+elim (cpms_inv_lifts_sn … HT1 (Ⓣ) … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #XT #HXT #HXT1
+elim (cpms_inv_lifts_sn … HT2 (Ⓣ) … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #X #H #HXT2
+lapply (lifts_inj … H … HXT) -T #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_appl_appl_aux (a) (h) (o) (G) (L) (V) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓐV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓐV.T ![a,h] →
+ ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
+ ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ ⓐV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓐV2.T2 ➡*[n1-n2,h] T.
+#a #h #o #G0 #L0 #V0 #T0 #IH #H0
+#V1 #HV01 #V2 #HV02 #n1 #T1 #HT01 #n2 #T2 #HT02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #HT0 #_ #_ -n0 -p0 -X01 -X02
+elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
+elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+#T #HT1 #HT2 -L0 -V0 -T0
+/3 width=5 by cpms_appl_dx, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_appl_beta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![a,h] →
+ ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
+ ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
+ ∀n1,T1. ⦃G,L⦄ ⊢ ⓛ{p}W.T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓛW⦄ ⊢ T ➡[n2,h] T2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ ⓐV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡*[n1-n2,h] T.
+#a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
+#V1 #HV01 #V2 #HV02 #W2 #HW02 #n1 #X #HX #n2 #T2 #HT02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
+elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
+elim (cpm_inv_abst1 … HX) -HX #W1 #T1 #HW01 #HT01 #H destruct
+elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
+elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
+elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+#T #HT1 #HT2 -L0 -V0 -W0 -T0
+lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 [ /2 width=1 by lsubr_beta/ ] #HT2
+/4 width=5 by cpms_beta_dx, cpms_bind_dx, cpm_cast, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_appl_theta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![a,h] →
+ ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
+ ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
+ ∀n1,T1. ⦃G,L⦄ ⊢ ⓓ{p}W.T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 →
+ ∀U2. ⬆*[1]V2 ≘ U2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ ⓐV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡*[n1-n2,h] T.
+#a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
+#V1 #HV01 #V2 #HV02 #W2 #HW02 #n1 #X #HX #n2 #T2 #HT02 #U2 #HVU2
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
+elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
+elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
+elim (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HVU2 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU2
+elim (cpm_inv_abbr1 … HX) -HX *
+[ #W1 #T1 #HW01 #HT01 #H destruct
+ elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
+ elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+ #T #HT1 #HT2 -L0 -V0 -W0 -T0
+ /4 width=7 by cpms_theta_dx, cpms_appl_dx, cpms_bind_dx, ex2_intro/
+| #T1 #HT01 #HX #H destruct
+ elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+ #T #HT1 #HT2 -L0 -V0 -W0 -T0
+ elim (cpms_inv_lifts_sn … HT1 (Ⓣ) … L1 … HX) -T1 [| /3 width=1 by drops_refl, drops_drop/ ] #X0 #HXT #HX0
+ /4 width=7 by cpms_zeta, cpms_appl_dx, lifts_flat, ex2_intro/
+]
+qed-.
+
+fact cnv_cpm_conf_lpr_beta_beta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![a,h] →
+ ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
+ ∀W1. ⦃G,L⦄ ⊢ W ➡[h] W1 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
+ ∀n1,T1. ⦃G,L.ⓛW⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓛW⦄ ⊢ T ➡[n2,h] T2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ ⓓ{p}ⓝW1.V1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡*[n1-n2,h] T.
+#a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
+#V1 #HV01 #V2 #HV02 #W1 #HW01 #W2 #HW02 #n1 #T1 #HT01 #n2 #T2 #HT02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
+elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
+elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
+elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
+elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+#T #HT1 #HT2 -L0 -V0 -W0 -T0
+lapply (lsubr_cpms_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/ #HT1
+lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/ #HT2
+/4 width=5 by cpms_bind_dx, cpm_eps, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_theta_theta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![a,h] →
+ ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
+ ∀W1. ⦃G,L⦄ ⊢ W ➡[h] W1 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
+ ∀n1,T1. ⦃G,L.ⓓW⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 →
+ ∀U1. ⬆*[1]V1 ≘ U1 → ∀U2. ⬆*[1]V2 ≘ U2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ ⓓ{p}W1.ⓐU1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡*[n1-n2,h] T.
+#a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
+#V1 #HV01 #V2 #HV02 #W1 #HW01 #W2 #HW02 #n1 #T1 #HT01 #n2 #T2 #HT02 #U1 #HVU1 #U2 #HVU2
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
+elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
+elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
+elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
+elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+#T #HT1 #HT2 -L0 -V0 -W0 -T0
+elim (cpm_lifts_sn … HV1 (Ⓣ) … (L1.ⓓW1) … HVU1) -V1 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU1
+lapply (cpm_lifts_bi … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2 … HVU) -V2 -V [ /3 width=1 by drops_refl, drops_drop/ ] #HU2
+/4 width=7 by cpms_appl_dx, cpms_bind_dx, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_cast_cast_aux (a) (h) (o) (G) (L) (V) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
+ ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
+ ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓝV2.T2 ➡*[n1-n2,h] T.
+#a #h #o #G0 #L0 #V0 #T0 #IH #H0
+#n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01 #T2 #HT02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
+elim (cnv_cpm_conf_lpr_far … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+#T #HT1 #HT2 #V #HV1 #HV2 -L0 -V0 -T0
+/3 width=5 by cpms_cast, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_cast_epsilon_aux (a) (h) (o) (G) (L) (V) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
+ ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 →
+ ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+#a #h #o #G0 #L0 #V0 #T0 #IH #H0
+#n1 #V1 #HV01 #T1 #HT01 #n2 #T2 #HT02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
+elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+#T #HT1 #HT2 -L0 -V0 -T0
+/3 width=3 by cpms_eps, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_cast_ee_aux (a) (h) (o) (G) (L) (V) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
+ (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
+ ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
+ ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡*[↑n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡*[n1-↑n2,h] T.
+#a #h #o #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
+#n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01
+#L1 #HL01 #L2 #HL02 -HV01
+elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
+lapply (cnv_cpms_trans_lpr_far … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
+elim (cnv_cpms_strip_lpr_far … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpms_strip_lpr_far … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
+-HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
+elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
+-L0 -V0 -T0 -X0 #U #HVU #HTU
+lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
+lapply (cpms_trans … HT1 … HTU) -T <arith_l #H1
+/3 width=3 by cpms_eps, ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_epsilon_epsilon_aux (a) (h) (o) (G) (L) (V) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
+ ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+#a #h #o #G0 #L0 #V0 #T0 #IH #H0
+#n1 #T1 #HT01 #n2 #T2 #HT02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_cast … H0) -H0 #X0 #_ #HT0 #_ #_ -X0
+elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+#T #HT1 #HT2 -L0 -V0 -T0
+/2 width=3 by ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_epsilon_ee_aux (a) (h) (o) (G) (L) (V) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
+ (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
+ ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ T1 ➡*[↑n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡*[n1-↑n2,h] T.
+#a #h #o #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
+#n1 #T1 #HT01 #n2 #V2 #HV02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
+lapply (cnv_cpms_trans_lpr_far … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
+elim (cnv_cpms_strip_lpr_far … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpms_strip_lpr_far … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
+-HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
+elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
+-L0 -V0 -T0 -X0 #U #HVU #HTU
+lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
+lapply (cpms_trans … HT1 … HTU) -T <arith_l #H1
+/2 width=3 by ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_ee_ee_aux (a) (h) (o) (G) (L) (V) (T):
+ (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
+ ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
+ ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ V1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡*[n1-n2,h] T.
+#a #h #o #G0 #L0 #V0 #T0 #IH #H0
+#n1 #V1 #HV01 #n2 #V2 #HV02
+#L1 #HL01 #L2 #HL02
+elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #_ #_ #_ -X0
+elim (cnv_cpm_conf_lpr_far … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+#V #HV1 #HV2 -L0 -V0 -T0
+/2 width=3 by ex2_intro/
+qed-.
+
+fact cnv_cpm_conf_lpr_aux (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_conf_lpr a h G1 L1 T1.
+#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
+[ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
+ elim (cpm_inv_atom1_drops … HX1) -HX1 *
+ elim (cpm_inv_atom1_drops … HX2) -HX2 *
+ [ #H21 #H22 #H11 #H12 destruct -L -a -o
+ <minus_O_n
+ /2 width=1 by cnv_cpm_conf_lpr_atom_atom_aux/
+ | #s2 #H21 #H22 #H23 #H11 #H12 destruct -L -a -o
+ <minus_O_n <minus_n_O
+ /2 width=1 by cnv_cpm_conf_lpr_atom_ess_aux/
+ | #K2 #V2 #XV2 #i #HLK2 #HVX2 #HXV2 #H21 #H11 #H12 destruct -IH2
+ <minus_O_n <minus_n_O
+ @(cnv_cpm_conf_lpr_atom_delta_aux … IH1) -IH1 /1 width=6 by/
+ | #m2 #K2 #W2 #XW2 #i #HLK2 #HWX2 #HXW2 #H21 #H22 #H11 #H12 destruct -IH2
+ <minus_O_n <minus_n_O
+ @(cnv_cpm_conf_lpr_atom_ell_aux … IH1) -IH1 /1 width=6 by/
+ | #H21 #H22 #s1 #H11 #H12 #H13 destruct -L -a -o
+ <minus_O_n <minus_n_O
+ /3 width=1 by cnv_cpm_conf_lpr_atom_ess_aux, ex2_commute/
+ | #s2 #H21 #H22 #H23 #s1 #H11 #H12 #H13 destruct -L -a -o
+ <minus_n_n
+ /2 width=1 by cnv_cpm_conf_lpr_atom_atom_aux/
+ | #K2 #V2 #XV2 #i2 #_ #_ #_ #H21 #s1 #H11 #H12 #H13 destruct
+ | #m2 #K2 #W2 #XW2 #i2 #_ #_ #_ #H21 #H22 #s1 #H11 #H12 #H13 destruct
+ | #H21 #H22 #K1 #V1 #XV1 #i1 #HLK1 #HVX1 #HXV1 #H11 destruct -IH2
+ <minus_O_n <minus_n_O
+ @ex2_commute @(cnv_cpm_conf_lpr_atom_delta_aux … IH1) -IH1 /1 width=6 by/
+ | #s2 #H21 #H22 #H23 #K1 #V1 #XV1 #i1 #_ #_ #_ #H11 destruct
+ | #K2 #V2 #XV2 #i2 #HLK2 #HVX2 #HXV2 #H21 #K1 #V1 #XV1 #i1 #HLK1 #HVX1 #HXV1 #H11 destruct -IH2
+ @(cnv_cpm_conf_lpr_delta_delta_aux … IH1) -IH1 /1 width=13 by/
+ | #m2 #K2 #W2 #XW2 #i2 #HLK2 #_ #_ #H21 #H22 #K1 #V1 #XV1 #i1 #HLK1 #_ #_ #H11 destruct -a -o -XW2 -XV1 -HL2 -HL1
+ elim cnv_cpm_conf_lpr_delta_ell_aux /1 width=8 by/
+ | #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2
+ <minus_O_n <minus_n_O
+ @ex2_commute @(cnv_cpm_conf_lpr_atom_ell_aux … IH1) -IH1 /1 width=6 by/
+ | #s2 #H21 #H22 #H23 #m1 #K1 #W1 #XW1 #i1 #_ #_ #_ #H11 #H12 destruct
+ | #K2 #V2 #XV2 #i2 #HLK2 #_ #_ #H21 #m1 #K1 #W1 #XW1 #i1 #HLK1 #_ #_ #H11 #H12 destruct -a -o -XV2 -XW1 -HL2 -HL1
+ elim cnv_cpm_conf_lpr_delta_ell_aux /1 width=8 by/
+ | #m2 #K2 #W2 #XW2 #i2 #HLK2 #HWX2 #HXW2 #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2
+ >minus_S_S >minus_S_S
+ @(cnv_cpm_conf_lpr_delta_delta_aux … IH1) -IH1 /1 width=13 by/
+ ]
+| #p #I #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
+ elim (cpm_inv_bind1 … HX1) -HX1 *
+ elim (cpm_inv_bind1 … HX2) -HX2 *
+ [ #V2 #T2 #HV2 #HT2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
+ @(cnv_cpm_conf_lpr_bind_bind_aux … IH1) -IH1 /1 width=1 by/
+ | #T2 #HT2 #HXT2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
+ @(cnv_cpm_conf_lpr_bind_zeta_aux … IH1) -IH1 /1 width=3 by/
+ | #V2 #T2 #HV2 #HT2 #H21 #T1 #HT1 #HXT1 #H11 #H12 destruct -IH2
+ @ex2_commute @(cnv_cpm_conf_lpr_bind_zeta_aux … IH1) -IH1 /1 width=3 by/
+ | #T2 #HT2 #HXT2 #H21 #H22 #T1 #HT1 #HXT1 #H11 #H12 destruct -IH2
+ @(cnv_cpm_conf_lpr_zeta_zeta_aux … IH1) -IH1 /1 width=3 by/
+ ]
+| #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
+ elim (cpm_inv_appl1 … HX1) -HX1 *
+ elim (cpm_inv_appl1 … HX2) -HX2 *
+ [ #V2 #T2 #HV2 #HT2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
+ @(cnv_cpm_conf_lpr_appl_appl_aux … IH1) -IH1 /1 width=1 by/
+ | #p2 #V2 #XW2 #W2 #XT2 #T2 #HV2 #HW2 #HT2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
+ @(cnv_cpm_conf_lpr_appl_beta_aux … IH1) -IH1 /1 width=1 by/
+ | #p2 #V2 #XV2 #XW2 #W2 #XT2 #T2 #HV2 #HXV2 #HW2 #HT2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
+ @(cnv_cpm_conf_lpr_appl_theta_aux … IH1) -IH1 /1 width=3 by/
+ | #V2 #T2 #HV2 #HT2 #H21 #p1 #V1 #XW1 #W1 #XT1 #T1 #HV1 #HW1 #HT1 #H11 #H12 destruct -IH2
+ @ex2_commute @(cnv_cpm_conf_lpr_appl_beta_aux … IH1) -IH1 /1 width=1 by/
+ | #p2 #V2 #XW2 #W2 #XT2 #T2 #HV2 #HW2 #HT2 #H21 #H22 #p1 #V1 #XW1 #W1 #XT1 #T1 #HV1 #HW1 #HT1 #H11 #H12 destruct -IH2
+ @(cnv_cpm_conf_lpr_beta_beta_aux … IH1) -IH1 /1 width=1 by/
+ | #p2 #V2 #XV2 #XW2 #W2 #XT2 #T2 #HV2 #HXV2 #HW2 #HT2 #H21 #H22 #p1 #V1 #XW1 #W1 #XT1 #T1 #HV1 #HW1 #HT1 #H11 #H12 destruct
+ | #V2 #T2 #HV2 #HT2 #H21 #p1 #V1 #XV1 #XW1 #W1 #XT1 #T1 #HV1 #HXV1 #HW1 #HT1 #H11 #H12 destruct -IH2
+ @ex2_commute @(cnv_cpm_conf_lpr_appl_theta_aux … IH1) -IH1 /1 width=3 by/
+ | #p2 #V2 #XW2 #W2 #XT2 #T2 #HV2 #HW2 #HT2 #H21 #H22 #p1 #V1 #XV1 #XW1 #W1 #XT1 #T1 #HV1 #HXV1 #HW1 #HT1 #H11 #H12 destruct
+ | #p2 #V2 #XV2 #XW2 #W2 #XT2 #T2 #HV2 #HXV2 #HW2 #HT2 #H21 #H22 #p1 #V1 #XV1 #XW1 #W1 #XT1 #T1 #HV1 #HXV1 #HW1 #HT1 #H11 #H12 destruct -IH2
+ @(cnv_cpm_conf_lpr_theta_theta_aux … IH1) -IH1 /1 width=3 by/
+ ]
+| #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
+ elim (cpm_inv_cast1 … HX1) -HX1 [ * || * ]
+ elim (cpm_inv_cast1 … HX2) -HX2 [ * || * | * || * | * || * ]
+ [ #V2 #T2 #HV2 #HT2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
+ @(cnv_cpm_conf_lpr_cast_cast_aux … IH1) -IH1 /1 width=1 by/
+ | #HT2 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
+ @(cnv_cpm_conf_lpr_cast_epsilon_aux … IH1) -IH1 /1 width=1 by/
+ | #m2 #HV2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct
+ @(cnv_cpm_conf_lpr_cast_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
+ | #V2 #T2 #HV2 #HT2 #H21 #HT1 destruct -IH2
+ @ex2_commute @(cnv_cpm_conf_lpr_cast_epsilon_aux … IH1) -IH1 /1 width=1 by/
+ | #HT2 #HT1 -IH2
+ @(cnv_cpm_conf_lpr_epsilon_epsilon_aux … IH1) -IH1 /1 width=1 by/
+ | #m2 #HV2 #H21 #HT1 destruct
+ @(cnv_cpm_conf_lpr_epsilon_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
+ | #V2 #T2 #HV2 #HT2 #H21 #m1 #HV1 #H11 destruct
+ @ex2_commute @(cnv_cpm_conf_lpr_cast_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
+ | #HT2 #m1 #HV1 #H11 destruct
+ @ex2_commute @(cnv_cpm_conf_lpr_epsilon_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
+ | #m2 #HV2 #H21 #m1 #HV1 #H11 destruct -IH2
+ >minus_S_S >minus_S_S
+ @(cnv_cpm_conf_lpr_ee_ee_aux … IH1) -IH1 /1 width=1 by/
+ ]
+]
+qed-.
include "basic_2/rt_computation/cprs_cprs.ma".
include "basic_2/rt_computation/lprs_cpms.ma".
include "basic_2/dynamic/cnv_drops.ma".
-include "basic_2/dynamic/cnv_etc.ma".
+include "basic_2/dynamic/cnv_preserve_far.ma".
include "basic_2/dynamic/lsubv_cnv.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-(* Properties with context-free parallel reduction for local environments *****)
+(* Far preservation propery with t-bound rt-transition for terms ************)
fact cnv_cpm_trans_lpr_aux (a) (h) (o):
∀G0,L0,T0.
elim (IH2 … HXUW1 … HXUT1 … HL12 … HL12) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ] -HXUW1 -HXUT1 -HWU1
>eq_minus_O // #W0 #H1 #H2 -IH2 -IH1 -L1 -W1 -T1 -U1
lapply (cprs_trans … HXW21 … H1) -XW1 #H1
- lapply (cpms_trans … HXT21 … H2) -XT1 <arith_l #H2
+ lapply (cpms_trans … HXT21 … H2) -XT1 <arith_l_eq #H2
/2 width=3 by cnv_cast/
| #HX -IH2 -HW1 -U1
lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
(* Basic_2A1: uses: snv_lref *)
lemma cnv_lref_drops (a) (h) (G): ∀I,K,V,i,L. ⦃G, K⦄ ⊢ V ![a, h] →
- ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G, L⦄ ⊢ #i ![a, h].
+ ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G, L⦄ ⊢ #i ![a, h].
#a #h #G #I #K #V #i elim i -i
[ #L #HV #H
lapply (drops_fwd_isid … H ?) -H // #H destruct
]
qed-.
+(* Advanced forward lemmas **************************************************)
+
+lemma cnv_lref_fwd_drops (a) (h) (G):
+ ∀i,L. ⦃G, L⦄ ⊢ #i ![a, h] →
+ ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ![a, h].
+#a #h #o #i #L #H #I #K #V #HLK
+elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #HX
+lapply (drops_mono … HLY … HLK) -L #H destruct //
+qed-.
+
(* Properties with generic slicing for local environments *******************)
(* Basic_2A1: uses: snv_lift *)
+++ /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 "basic_2/rt_computation/fpbg.ma".
-include "basic_2/rt_computation/cpms_fpbs.ma".
-include "basic_2/dynamic/cnv.ma".
-
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-(* Inductive premises for the preservation results **************************)
-
-definition IH_cnv_cpm_trans_lpr (a) (h): relation3 genv lenv term ≝
- λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] →
- ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡[n,h] T2 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h].
-
-definition IH_cnv_cpms_trans_lpr (a) (h): relation3 genv lenv term ≝
- λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] →
- ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡*[n,h] T2 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h].
-
-definition IH_cnv_cpm_conf_lpr (a) (h): relation3 genv lenv term ≝
- λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
- ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
-
-definition IH_cnv_cpms_strip_lpr (a) (h): relation3 genv lenv term ≝
- λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
- ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
-
-definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝
- λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
- ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
-
-(* Properties for preservation **********************************************)
-
-lemma cnv_cpms_trans_lpr_far (a) (h) (o):
- ∀G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
- ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
-#a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
-@(cpms_ind_dx … H) -n -T2
-/4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/
-qed-.
-
-lemma cnv_cpms_strip_lpr_far (a) (h) (o):
- ∀G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
- ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1.
-/3 width=8 by cpm_cpms/ qed-.
-
-(*
-fact cnv_cpms_strip_lpr_aux (a) (h) (o):
- ∀G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_conf_lpr a h G1 L1 T1) →
- ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1.
-#a #h #o #G0 #L0 #T0 #IH0 #G #L #T #H0 #HT #n1 #T1 #H
-generalize in match HT; generalize in match H0; -H0 -HT
-@(cpms_ind_sn … H) -n1 -T [ /2 width=8 by/ ]
-#n1 #n2 #T #X #HTX #HXT1 #IH #H0 #HT #n2 #T2 #HT2 #L1 #HL1 #L2 #HL2
-elim (IH0 … HTX … HT2 … HL1 … HL2) // -L -T #T0 #HXT0 #HT20
-
- @(IH … 0 T … HT2 … HL1 … HL2) // -L -IH
- #T0 #HT20 #HT0
-*)
--- /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 "basic_2/rt_computation/fpbg.ma".
+include "basic_2/rt_computation/cpms_fpbs.ma".
+include "basic_2/dynamic/cnv.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Inductive premises for the preservation results **************************)
+
+definition IH_cnv_cpm_trans_lpr (a) (h): relation3 genv lenv term ≝
+ λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] →
+ ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡[n,h] T2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h].
+
+definition IH_cnv_cpms_trans_lpr (a) (h): relation3 genv lenv term ≝
+ λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] →
+ ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡*[n,h] T2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h].
+
+definition IH_cnv_cpm_conf_lpr (a) (h): relation3 genv lenv term ≝
+ λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
+ ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+
+definition IH_cnv_cpms_strip_lpr (a) (h): relation3 genv lenv term ≝
+ λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
+ ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+
+definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝
+ λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
+ ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+
+(* Properties for preservation **********************************************)
+
+lemma cnv_cpms_trans_lpr_far (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
+#a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
+@(cpms_ind_dx … H) -n -T2
+/4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/
+qed-.
+
+lemma cnv_cpm_conf_lpr_far (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_conf_lpr a h G1 L1 T1.
+/3 width=8 by cpm_cpms/ qed-.
+
+lemma cnv_cpms_strip_lpr_far (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1.
+/3 width=8 by cpm_cpms/ qed-.
lemma lsubv_refl (a) (h) (G): reflexive … (lsubv a h G).
#a #h #G #L elim L -L /2 width=1 by lsubv_atom, lsubv_bind/
qed.
+
+(* Basic_2A1: removed theorems 3:
+ lsubsv_lstas_trans lsubsv_sta_trans
+ lsubsv_fwd_lsubd
+*)
cnv.ma cnv_drops.ma cnv_fqus.ma cnv_aaa.ma cnv_fsb.ma
-cnv_etc.ma cnv_cpm_trans.ma
+cnv_preserve_far.ma cnv_cpm_trans.ma cnv_cpm_conf.ma
lsubv.ma lsubv_drops.ma lsubv_lsubr.ma lsubv_lsuba.ma lsubv_cpms.ma lsubv_cpcs.ma lsubv_cnv.ma lsubv_lsubv.ma
+++ /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/lsubd_da.ma".
-include "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/snv_scpes.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Properties on degree assignment for terms ********************************)
-
-fact da_cpr_lpr_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h o G1 L1 T1.
-#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
-[ #s #_ #_ #_ #_ #d #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1
- lapply (da_inv_sort … H2) -H2
- lapply (cpr_inv_sort1 … H3) -H3 #H destruct /2 width=1 by da_sort/
-| #i #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
- elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #H #HX0
- elim (da_inv_lref … H2) -H2 * #K1 [ #V1 | #W1 #d1 ] #HLK1 [ #HV1 | #HW1 #H ] destruct
- lapply (drop_mono … H … HLK1) -H #H destruct
- elim (cpr_inv_lref1 … H3) -H3
- [1,3: #H destruct
- lapply (fqup_lref … G1 … HLK1)
- elim (lpr_drop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
- elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
- /4 width=10 by da_ldef, da_ldec, fqup_fpbg/
- |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
- lapply (drop_mono … H … HLK1) -H #H destruct
- lapply (fqup_lref … G1 … HLK1)
- elim (lpr_drop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
- elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct
- lapply (drop_fwd_drop2 … HLK2) -V2
- /4 width=8 by da_lift, fqup_fpbg/
- ]
-| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
- elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct -IH2
- elim (snv_inv_bind … H1) -H1 #_ #HT1
- lapply (da_inv_bind … H2) -H2
- elim (cpr_inv_bind1 … H3) -H3 *
- [ #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=9 by da_bind, fqup_fpbg, lpr_pair/
- | #T2 #HT12 #HT2 #H1 #H2 destruct
- /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, drop_drop/
- ]
-| #V1 #T1 #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct
- elim (snv_inv_appl … H1) -H1 #b1 #W1 #U1 #d1 #HV1 #HT1 #HVW1 #HTU1
- lapply (da_inv_flat … H2) -H2 #Hd
- elim (cpr_inv_appl1 … H3) -H3 *
- [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbg/
- | #b #V2 #W #W2 #U #U2 #HV12 #HW2 #HU2 #H1 #H2 destruct
- elim (snv_inv_bind … HT1) -HT1 #HW #HU
- lapply (da_inv_bind … Hd) -Hd #Hd
- elim (scpds_inv_abst1 … HTU1) -HTU1 #W3 #U3 #HW3 #_ #H destruct -U3 -d1
- elim (snv_fwd_da … HV1) #d1 #Hd1
- elim (snv_fwd_da … HW) #d0 #Hd0
- lapply (cprs_scpds_div … HW3 … Hd0 … 1 HVW1) -W3 #H
- elim (da_scpes_aux … IH3 IH2 IH1 … Hd0 … Hd1 … H) -IH3 -IH2 -H /2 width=1 by fqup_fpbg/ #_ #H1
- <minus_n_O #H destruct >(plus_minus_k_k d1 1) in Hd1; // -H1 #Hd1
- lapply (IH1 … HV1 … Hd1 … HV12 … HL12) -HV1 -Hd1 -HV12 [ /2 by fqup_fpbg/ ]
- lapply (IH1 … Hd0 … HW2 … HL12) -Hd0 /2 width=1 by fqup_fpbg/ -HW
- lapply (IH1 … HU … Hd … HU2 (L2.ⓛW2) ?) -IH1 -HU -Hd -HU2 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2
- /4 width=6 by da_bind, lsubd_da_trans, lsubd_beta/
- | #b #V0 #V2 #W #W2 #U #U2 #HV10 #HV02 #HW2 #HU2 #H1 #H2 destruct -IH3 -IH2 -b1 -V0 -W1 -U1 -d1 -HV1
- elim (snv_inv_bind … HT1) -HT1 #_
- lapply (da_inv_bind … Hd) -Hd
- /5 width=9 by da_bind, da_flat, fqup_fpbg, lpr_pair/
- ]
-| #W1 #T1 #HG0 #HL0 #HT0 #H1 #d #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
- elim (snv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
- lapply (da_inv_flat … H2) -H2 #Hd
- elim (cpr_inv_cast1 … H3) -H3
- [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/
- | /3 width=7 by fqup_fpbg/
- ]
-]
-qed-.
+++ /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 "basic_2/dynamic/snv_lift.ma".
-include "basic_2/dynamic/snv_scpes.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Properties on nat-iterated stratified static type assignment for terms ***)
-
-fact snv_lstas_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lstas h o G1 L1 T1.
-#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
-[ #s #HG0 #HL0 #HT0 #_ #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
- >(lstas_inv_sort1 … H2) -X //
-| #i #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #T #H2 destruct -IH4 -IH3 -IH2
- elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HLK0 #HX0
- elim (da_inv_lref … Hd1) -Hd1 * #K1 [ #V1 | #W1 #d0 ] #HLK1 [ #Hd1 | #Hd0 #H ]
- lapply (drop_mono … HLK0 … HLK1) -HLK0 #H0 destruct
- elim (lstas_inv_lref1 … H2) -H2 * #K #Y #X [3,6: #d ] #HLK #HYX [1,2: #HXT #H0 |3,5: #HXT |4,6: #H1 #H2 ]
- lapply (drop_mono … HLK … HLK1) -HLK #H destruct
- [ lapply (le_plus_to_le_c … Hd21) -Hd21 #Hd21 |3: -Hd21 ]
- lapply (fqup_lref … G1 … HLK1) #H
- lapply (drop_fwd_drop2 … HLK1) /4 width=8 by snv_lift, snv_lref, fqup_fpbg/
-| #p #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
- elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2
- elim (snv_inv_bind … H1) -H1 #HV1 #HT1
- lapply (da_inv_bind … Hd1) -Hd1 #Hd1
- elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, snv_bind/
-| #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct
- elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #d0 #HV1 #HT1 #HVW1 #HTU1
- lapply (da_inv_flat … Hd1) -Hd1 #Hd1
- elim (lstas_inv_appl1 … H2) -H2 #T0 #HT10 #H destruct
- lapply (IH1 … HT1 … Hd1 … HT10) /2 width=1 by fqup_fpbg/ #HT0
- lapply (lstas_scpds_aux … IH1 IH4 IH3 IH2 … Hd1 … HT10 … HTU1) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -d1 #H
- elim (scpes_inv_abst2 … H) -H /3 width=6 by snv_appl, scpds_cprs_trans/
-| #U1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2
- elim (snv_inv_cast … H1) -H1
- lapply (da_inv_flat … Hd1) -Hd1
- lapply (lstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/
-]
-qed-.
+++ /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 "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/snv_scpes.ma".
-include "basic_2/dynamic/lsubsv_lstas.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Properties on sn parallel reduction for local environments ***************)
-
-fact lstas_cpr_lpr_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lstas_cpr_lpr h o G1 L1 T1.
-#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
-[ #s #_ #_ #_ #_ #d1 #d2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH4 -IH3 -IH2 -IH1
- >(lstas_inv_sort1 … H2) -X2
- >(cpr_inv_sort1 … H3) -X3 /2 width=3 by ex2_intro/
-| #i #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3
- elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HK0 #HX0
- elim (da_inv_lref … Hd1) -Hd1 * #K1 [ #V1 | #W1 #d ] #HLK1 [ #HVd1 | #HWd1 #H destruct ]
- lapply (drop_mono … HK0 … HLK1) -HK0 #H destruct
- elim (lstas_inv_lref1 … H2) -H2 * #K0 #V0 #X0 [3,6: #d0 ] #HK0 #HVX0 [1,2: #HX02 #H |3,5: #HX02 |4,6: #H1 #H2 ] destruct
- lapply (drop_mono … HK0 … HLK1) -HK0 #H destruct
- [ lapply (le_plus_to_le_c … Hd21) -Hd21 #Hd21 |3: -Hd21 ]
- lapply (fqup_lref … G1 … HLK1) #HKV1
- elim (lpr_drop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
- elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #W2 | #V2 ] #HK12 [ #HW12 | #HW12 | #HV12 ] #H destruct
- lapply (drop_fwd_drop2 … HLK2) #H2
- elim (cpr_inv_lref1 … H3) -H3
- [1,3,5: #H destruct -HLK1
- |2,4,6: * #K #V #X #H #HVX #HX3
- lapply (drop_mono … H … HLK1) -H -HLK1 #H destruct
- ]
- [ lapply (IH2 … HWd1 … HW12 … HK12) /2 width=1 by fqup_fpbg/ -IH2 #H
- elim (da_lstas … H d0) -H
- elim (IH1 … HWd1 … HVX0 … HW12 … HK12) -IH1 -HVX0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2
- elim (lift_total V2 0 (i+1))
- /3 width=12 by cpcs_lift, lstas_succ, ex2_intro/
- | elim (IH1 … HWd1 … HVX0 … HW12 … HK12) -IH1 -HVX0
- /3 width=5 by fqup_fpbg, lstas_zero, ex2_intro/
- | elim (IH1 … HVd1 … HVX0 … HV12 … HK12) -IH1 -HVd1 -HVX0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02
- elim (lift_total W2 0 (i+1))
- /4 width=12 by cpcs_lift, lstas_ldef, ex2_intro/
- | elim (IH1 … HVd1 … HVX0 … HVX … HK12) -IH1 -HVd1 -HVX0 -HVX -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -d1 #W2 #HXW2 #HW02
- elim (lift_total W2 0 (i+1))
- /3 width=12 by cpcs_lift, lstas_lift, ex2_intro/
- ]
-| #p #_ #_ #HT0 #H1 destruct -IH4 -IH3 -IH2 -IH1
- elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 -IH2
- elim (snv_inv_bind … H1) -H1 #_ #HT1
- lapply (da_inv_bind … Hd1) -Hd1 #Hd1
- elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
- elim (cpr_inv_bind1 … H3) -H3 *
- [ #V2 #T2 #HV12 #HT12 #H destruct
- elim (IH1 … Hd1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hd1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, lpr_pair/ -T1
- /4 width=5 by cpcs_bind2, lpr_cpr_conf, lstas_bind, ex2_intro/
- | #T3 #HT13 #HXT3 #H1 #H2 destruct
- elim (IH1 … Hd1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hd1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
- elim (lstas_inv_lift1 … HTU3 L2 … HXT3) -T3
- /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, drop_drop, ex2_intro/
- ]
-| #V1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct
- elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #d0 #HV1 #HT1 #HVW1 #HTU1
- lapply (da_inv_flat … Hd1) -Hd1 #Hd1
- elim (lstas_inv_appl1 … H2) -H2 #X #HT1U #H destruct
- elim (cpr_inv_appl1 … H3) -H3 *
- [ #V2 #T2 #HV12 #HT12 #H destruct -a -d0 -W1 -U1 -HV1 -IH4 -IH3 -IH2
- elim (IH1 … Hd1 … HT1U … HT12 … HL12) -IH1 -Hd1 -HT1U
- /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lstas_appl, ex2_intro/
- | #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct
- elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2
- lapply (da_inv_bind … Hd1) -Hd1 #Hd1
- elim (lstas_inv_bind1 … HT1U) -HT1U #U #HT2U #H destruct
- elim (scpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -d0
- elim (snv_fwd_da … HW2) #d0 #HW2d
- lapply (cprs_scpds_div … HW20 … HW2d … HVW1) -W0 #H21
- elim (snv_fwd_da … HV1) #d #HV1d
- elim (da_scpes_aux … IH4 IH3 IH2 … HW2d … HV1d … H21) /2 width=1 by fqup_fpbg/ #_ #H
- <minus_n_O #H0 destruct >(plus_minus_k_k d 1) in HV1d; // -H #HV1d
- lapply (scpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32
- lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
- lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
- lapply (IH2 … HW2d … HW23 … HL12) /2 width=1 by fqup_fpbg/ -HW2 -HW2d #HW3d
- lapply (IH2 … HV1d … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV1d #HV2d
- elim (IH1 … Hd1 … HT2U … HT23 (L2.ⓛW3)) -HT2U /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23
- elim (lsubsv_lstas_trans … o … HTU3 … Hd21 … (L2.ⓓⓝW3.V2)) -HTU3
- [ #U4 #HT3U4 #HU43 -IH1 -IH2 -IH3 -IH4 -d -d1 -HW3 -HV2 -HT2
- @(ex2_intro … (ⓓ{b}ⓝW3.V2.U4)) /2 width=1 by lstas_bind/ -HT3U4
- @(cpcs_canc_dx … (ⓓ{b}ⓝW3.V2.U3)) /2 width=1 by cpcs_bind_dx/ -HU43
- @(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W3.U3)) /2 width=1 by cpr_beta/
- /4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
- | -U3
- @(lsubsv_beta … (d-1)) /3 width=7 by fqup_fpbg/
- @shnv_cast [1,2: // ] #d0 #Hd0
- lapply (scpes_le_aux … IH4 IH3 IH2 IH1 … HW3d … HV2d … d0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3d -HV2d -H32
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
- | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/
- ]
- | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -d0 -W1 -HV1 -IH4 -IH3 -IH2
- elim (snv_inv_bind … HT1) -HT1 #_ #HT0
- lapply (da_inv_bind … Hd1) -Hd1 #Hd1
- elim (lstas_inv_bind1 … HT1U) -HT1U #U0 #HTU0 #H destruct
- elim (IH1 … Hd1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hd1 -HTU0 /2 width=1 by fqup_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02
- lapply (lpr_cpr_conf … HL12 … HV10) -HV10 #HV10
- lapply (lpr_cpr_conf … HL12 … HW02) -L1 #HW02
- lapply (cpcs_bind2 b … HW02 … HU02) -HW02 -HU02 #HU02
- lapply (cpcs_flat … HV10 … HU02 Appl) -HV10 -HU02 #HU02
- lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?)
- /4 width=3 by lstas_appl, lstas_bind, cpr_theta, ex2_intro/
- ]
-| #W1 #T1 #HG0 #HL0 #HT0 #H1 #d1 #d2 #Hd21 #Hd1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 -IH2
- elim (snv_inv_cast … H1) -H1 #U1 #_ #HT1 #_ #_ -U1
- lapply (da_inv_flat … Hd1) -Hd1 #Hd1
- lapply (lstas_inv_cast1 … H2) -H2 #HTU1
- elim (cpr_inv_cast1 … H3) -H3
- [ * #U2 #T2 #_ #HT12 #H destruct
- elim (IH1 … Hd1 … HTU1 … HT12 … HL12) -IH1 -Hd1 -HTU1 -HL12
- /3 width=3 by fqup_fpbg, lstas_cast, ex2_intro/
- | #HT1X3 elim (IH1 … Hd1 … HTU1 … HT1X3 … HL12) -IH1 -Hd1 -HTU1 -HL12
- /2 width=3 by fqup_fpbg, ex2_intro/
- ]
-]
-qed-.
--- /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 "basic_2/computation/fsb_aaa.ma".
+include "basic_2/dynamic/snv_da_lpr.ma".
+include "basic_2/dynamic/snv_lstas.ma".
+include "basic_2/dynamic/snv_lstas_lpr.ma".
+include "basic_2/dynamic/snv_lpr.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Main preservation properties *********************************************)
+
+lemma snv_preserve: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] →
+ ∧∧ IH_da_cpr_lpr h o G L T
+ & IH_snv_cpr_lpr h o G L T
+ & IH_snv_lstas h o G L T
+ & IH_lstas_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_fwd_aaa … HT) -HT
+#A #HT @(aaa_ind_fpbg h o … HT) -G -L -T -A
+#G #L #T #A #_ #IH -A @and4_intro
+[ letin aux ≝ da_cpr_lpr_aux | letin aux ≝ snv_cpr_lpr_aux
+| letin aux ≝ snv_lstas_aux | letin aux ≝ lstas_cpr_lpr_aux
+]
+@(aux … G L T) // #G0 #L0 #T0 #H elim (IH … H) -IH -H //
+qed-.
+
+theorem da_cpr_lpr: ∀h,o,G,L,T. IH_da_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
+qed-.
+
+theorem snv_cpr_lpr: ∀h,o,G,L,T. IH_snv_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
+qed-.
+
+theorem snv_lstas: ∀h,o,G,L,T. IH_snv_lstas h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=5 by/
+qed-.
+
+theorem lstas_cpr_lpr: ∀h,o,G,L,T. IH_lstas_cpr_lpr h o G L T.
+#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=3 by/
+qed-.
+
+(* Advanced preservation properties *****************************************)
+
+lemma snv_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o].
+#h #o #G #L1 #T1 #HT1 #T2 #H
+@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
+qed-.
+
+lemma da_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d.
+#h #o #G #L1 #T1 #HT1 #d #Hd #T2 #H
+@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
+qed-.
+
+lemma lstas_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #o #G #L1 #T1 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
+#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
+elim (IHT1 L1) // -IHT1 #U #HTU #HU1
+elim (lstas_cpr_lpr … o … Hd21 … HTU … HTT2 … HL12) -HTU -HTT2
+[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -d1
+/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
+qed-.
+
+lemma lstas_cpcs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ ∀d,d1. d ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, o] →
+ ∀d2. d ≤ d2 → ⦃G, L1⦄ ⊢ T2 ▪[h, o] d2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, d] U2 →
+ ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #o #G #L1 #T1 #HT1 #d #d1 #Hd1 #HTd1 #U1 #HTU1 #T2 #HT2 #d2 #Hd2 #HTd2 #U2 #HTU2 #H #L2 #HL12
+elim (cpcs_inv_cprs … H) -H #T #H1 #H2
+elim (lstas_cprs_lpr … HT1 … Hd1 HTd1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
+elim (lstas_cprs_lpr … HT2 … Hd2 HTd2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
+lapply (lstas_mono … H1 … H2) -h -T -d #H destruct /2 width=3 by cpcs_canc_dx/
+qed-.
+++ /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 "basic_2/computation/fsb_aaa.ma".
-include "basic_2/dynamic/snv_da_lpr.ma".
-include "basic_2/dynamic/snv_lstas.ma".
-include "basic_2/dynamic/snv_lstas_lpr.ma".
-include "basic_2/dynamic/snv_lpr.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Main preservation properties *********************************************)
-
-lemma snv_preserve: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] →
- ∧∧ IH_da_cpr_lpr h o G L T
- & IH_snv_cpr_lpr h o G L T
- & IH_snv_lstas h o G L T
- & IH_lstas_cpr_lpr h o G L T.
-#h #o #G #L #T #HT elim (snv_fwd_aaa … HT) -HT
-#A #HT @(aaa_ind_fpbg h o … HT) -G -L -T -A
-#G #L #T #A #_ #IH -A @and4_intro
-[ letin aux ≝ da_cpr_lpr_aux | letin aux ≝ snv_cpr_lpr_aux
-| letin aux ≝ snv_lstas_aux | letin aux ≝ lstas_cpr_lpr_aux
-]
-@(aux … G L T) // #G0 #L0 #T0 #H elim (IH … H) -IH -H //
-qed-.
-
-theorem da_cpr_lpr: ∀h,o,G,L,T. IH_da_cpr_lpr h o G L T.
-#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
-qed-.
-
-theorem snv_cpr_lpr: ∀h,o,G,L,T. IH_snv_cpr_lpr h o G L T.
-#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=1 by/
-qed-.
-
-theorem snv_lstas: ∀h,o,G,L,T. IH_snv_lstas h o G L T.
-#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=5 by/
-qed-.
-
-theorem lstas_cpr_lpr: ∀h,o,G,L,T. IH_lstas_cpr_lpr h o G L T.
-#h #o #G #L #T #HT elim (snv_preserve … HT) /2 width=3 by/
-qed-.
-
-(* Advanced preservation properties *****************************************)
-
-lemma snv_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o].
-#h #o #G #L1 #T1 #HT1 #T2 #H
-@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
-qed-.
-
-lemma da_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d.
-#h #o #G #L1 #T1 #HT1 #d #Hd #T2 #H
-@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
-qed-.
-
-lemma lstas_cprs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #o #G #L1 #T1 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
-#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
-elim (IHT1 L1) // -IHT1 #U #HTU #HU1
-elim (lstas_cpr_lpr … o … Hd21 … HTU … HTT2 … HL12) -HTU -HTT2
-[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -d1
-/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
-qed-.
-
-lemma lstas_cpcs_lpr: ∀h,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀d,d1. d ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, o] →
- ∀d2. d ≤ d2 → ⦃G, L1⦄ ⊢ T2 ▪[h, o] d2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, d] U2 →
- ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #o #G #L1 #T1 #HT1 #d #d1 #Hd1 #HTd1 #U1 #HTU1 #T2 #HT2 #d2 #Hd2 #HTd2 #U2 #HTU2 #H #L2 #HL12
-elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (lstas_cprs_lpr … HT1 … Hd1 HTd1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
-elim (lstas_cprs_lpr … HT2 … Hd2 HTd2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
-lapply (lstas_mono … H1 … H2) -h -T -d #H destruct /2 width=3 by cpcs_canc_dx/
-qed-.
+++ /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 "basic_2/computation/fpbg_fpbs.ma".
-include "basic_2/equivalence/scpes_cpcs.ma".
-include "basic_2/equivalence/scpes_scpes.ma".
-include "basic_2/dynamic/snv.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Inductive premises for the preservation results **************************)
-
-definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
- λh,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o].
-
-definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
- λh,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ⦃G, L2⦄ ⊢ T2 ▪[h, o] d.
-
-definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
- λh,o,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-
-definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝
- λh,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] →
- ∀d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 →
- ∀U. ⦃G, L⦄ ⊢ T •*[h, d2] U → ⦃G, L⦄ ⊢ U ¡[h, o].
-
-(* Properties for the preservation results **********************************)
-
-fact snv_cprs_lpr_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o].
-#h #o #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
-@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/
-qed-.
-
-fact da_cprs_lpr_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d.
-#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d #Hd #T2 #H
-@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/
-qed-.
-
-fact da_scpds_lpr_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀d1. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
- ∀T2,d2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- d2 ≤ d1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, o] d1-d2.
-#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d1 #Hd1 #T2 #d2 * #T #d0 #Hd20 #H #HT1 #HT2 #L2 #HL12
-lapply (da_mono … H … Hd1) -H #H destruct
-lapply (lstas_da_conf … HT1 … Hd1) #Hd12
-lapply (da_cprs_lpr_aux … IH2 IH1 … Hd12 … HT2 … HL12) -IH2 -IH1 -HT2 -HL12
-/3 width=8 by fpbg_fpbs_trans, lstas_fpbs, conj/
-qed-.
-
-fact da_scpes_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
- ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →
- ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 →
- ∀d21,d22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 →
- ∧∧ d21 ≤ d11 & d22 ≤ d12 & d11 - d21 = d12 - d22.
-#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #d11 #Hd11 #d12 #Hd12 #d21 #d22 * #T #HT1 #HT2
-elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd11 … HT1 … L) -Hd11 -HT1 //
-elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hd12 … HT2 … L) -Hd12 -HT2 //
-/3 width=7 by da_mono, and3_intro/
-qed-.
-
-fact lstas_cprs_lpr_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, d2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #d1 #d2 #Hd21 #Hd1 #U1 #HTU1 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=10 by/ ]
-#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
-elim (IHT1 L1) // -IHT1 #U #HTU #HU1
-elim (IH1 … Hd21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
-[2: /3 width=12 by da_cprs_lpr_aux/
-|3: /3 width=10 by snv_cprs_lpr_aux/
-|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/
-] -G0 -L0 -T0 -T1 -T -d1
-/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
-qed-.
-
-fact scpds_cpr_lpr_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀U1,d. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, o, d] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
-#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #d2 * #W1 #d1 #Hd21 #HTd1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
-elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12
-lapply (IH2 … H01 … HTd1 … HT12 … HL12) -L0 -T0 // -T1
-lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
-lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
-elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/
-qed-.
-
-fact scpes_cpr_lpr_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- ∀G,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, o] →
- ∀d1,d2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
- ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ⦃G, L2⦄ ⊢ U1 •*⬌*[h, o, d1, d2] U2.
-#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #T2 #HT02 #HT2 #d1 #d2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12
-elim (scpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1
-elim (scpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2
-elim (cprs_conf … H1 … H2) -T0
-/3 width=5 by scpds_div, scpds_cprs_trans/
-qed-.
-
-fact lstas_scpds_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- ∀G,L,T. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, o] →
- ∀d,d1. d1 ≤ d → ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀T1. ⦃G, L⦄ ⊢ T •*[h, d1] T1 →
- ∀T2,d2. ⦃G, L⦄ ⊢ T •*➡*[h, o, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d2-d1, d1-d2] T2.
-#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #d #d1 #Hd1 #HTd #T1 #HT1 #T2 #d2 * #X #d0 #Hd20 #H #HTX #HXT2
-lapply (da_mono … H … HTd) -H #H destruct
-lapply (lstas_da_conf … HT1 … HTd) #HTd1
-lapply (lstas_da_conf … HTX … HTd) #HXd
-lapply (da_cprs_lpr_aux … IH3 IH2 … HXd … HXT2 L ?)
-[1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTd2
-elim (le_or_ge d1 d2) #Hd12 >(eq_minus_O … Hd12)
-[ elim (da_lstas … HTd2 0) #X2 #HTX2 #_ -IH4 -IH3 -IH2 -IH1 -H0 -HT -HTd -HXd
- /5 width=6 by lstas_scpds, scpds_div, cprs_strap1, lstas_cpr, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro/
-| elim (da_lstas … HTd1 0) #X1 #HTX1 #_
- lapply (lstas_conf_le … HTX … HT1) // #HXT1 -HT1
- elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … HXd … HXT1 … HXT2 L) -IH3 -IH2 -IH1 -HXd -HXT1 -HXT2
- /4 width=8 by cpcs_scpes, cpcs_cpr_conf, fpbg_fpbs_trans, lstas_fpbs, lstas_cpr, monotonic_le_minus_l/
-]
-qed-.
-
-fact scpes_le_aux: ∀h,o,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
- ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →
- ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 →
- ∀d21,d22,d. d21 + d ≤ d11 → d22 + d ≤ d12 →
- ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21+d, d22+d] T2.
-#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #d11 #Hd11 #Hd12 #Hd12 #d21 #d22 #d #H1 #H2 * #T0 #HT10 #HT20
-elim (da_lstas … Hd11 (d21+d)) #X1 #HTX1 #_
-elim (da_lstas … Hd12 (d22+d)) #X2 #HTX2 #_
-lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hd11 … HTX1 … HT10) -HT10
-[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_k_k_commutative #HX1 ]
-lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hd12 … HTX2 … HT20) -HT20
-[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_k_k_commutative #HX2 ]
-lapply (lstas_scpes_trans … Hd11 … HTX1 … HX1) [ // ] -Hd11 -HTX1 -HX1 -H1 #H1
-lapply (lstas_scpes_trans … Hd12 … HTX2 … HX2) [ // ] -Hd12 -HTX2 -HX2 -H2 #H2
-/2 width=4 by scpes_canc_dx/ (**) (* full auto fails *)
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma snv_cast_scpes: ∀h,o,G,L,U,T. ⦃G, L⦄ ⊢ U ¡[h, o] → ⦃G, L⦄ ⊢ T ¡[h, o] →
- ⦃G, L⦄ ⊢ U •*⬌*[h, o, 0, 1] T → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o].
-#h #o #G #L #U #T #HU #HT * /2 width=3 by snv_cast/
-qed.
]
qed.
+lemma cpms_ell_drops (n) (h) (G):
+ ∀L,K,W,i. ⬇*[i] L ≘ K.ⓛW →
+ ∀W2. ⦃G, K⦄ ⊢ W ➡*[n, h] W2 →
+ ∀V2. ⬆*[↑i] W2 ≘ V2 → ⦃G, L⦄ ⊢ #i ➡*[↑n, h] V2.
+#n #h #G #L #K #W #i #HLK #W2 #H @(cpms_ind_dx … H) -W2
+[ /3 width=6 by cpm_cpms, cpm_ell_drops/
+| #n1 #n2 #W1 #W2 #_ #IH #HW12 #V2 #HWV2
+ lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK
+ elim (lifts_total W1 (𝐔❴↑i❵)) #V1 #HWV1 >plus_S1
+ /3 width=11 by cpm_lifts_bi, cpms_step_dx/
+]
+qed.
+
(* Advanced inversion lemmas ************************************************)
lemma cpms_inv_lref1_drops (n) (h) (G):
*)
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" (* + "cnv_scpes" + "cnv_preserve" *) * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_preserve_far" (* + "cnv_preserve" *) * ]
}
]
}
../../matitac.opt `cat partial.txt`
-cd basic_2/dynamic/
-../../../../matitac.opt `cat partial.txt`
-cd ../../
lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
// qed.
-lemma arith_l: ∀x. 1 = 1-x+(x-(x-1)).
-* // #x >minus_S_S >minus_S_S <minus_O_n <minus_n_O //
-qed.
+lemma arith_l (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)).
+* // qed.
+
+lemma arith_l_eq: ∀x. 1 = 1-x+(x-(x-1)).
+// qed.
(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
basic_2/rt_computation
basic_2/rt_conversion
basic_2/rt_equivalence
+basic_2/dynamic/
apps_2/examples/ex_cpr_omega.ma
apps_2/functional/
apps_2/models/
projects / helm.git / commitdiff