X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpm_conf.ma;h=ed24744dac49bc9a9d7557208bdd68f9f6e6e694;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hp=c10e470dd3976498d84cb22e26449c73445d52dc;hpb=647b419e96770d90a82d7a9e5e8843566a9f93ee;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma index c10e470dd..ed24744da 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma @@ -24,22 +24,22 @@ include "basic_2/dynamic/cnv_preserve_sub.ma". (* Sub 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. + ∃∃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⦄ ⊢ ⋆(⫯[h]s) ➡*[h] T. + ∃∃T. ❪G,L1❫ ⊢ ⋆s ➡*[1,h] T & ❪G,L2❫ ⊢ ⋆(⫯[h]s) ➡*[h] T. /3 width=3 by cpm_cpms, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_atom_delta_aux (a) (h) (G) (L) (i): - (∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃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 #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2 +fact cnv_cpm_conf_lpr_atom_delta_aux (h) (a) (G) (L) (i): + (∀G0,L0,T0. ❪G,L,#i❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫⊢#i![h,a] → + ∀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. +#h #a #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2 lapply (cnv_inv_lref_pair … 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 @@ -53,15 +53,15 @@ 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) (G) (L) (i): - (∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃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 #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2 +fact cnv_cpm_conf_lpr_atom_ell_aux (h) (a) (G) (L) (i): + (∀G0,L0,T0. ❪G,L,#i❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫⊢#i![h,a] → + ∀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. +#h #a #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2 lapply (cnv_inv_lref_pair … 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 @@ -75,15 +75,15 @@ 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) (I) (G) (L) (i): - (∀G0,L0,T0. ⦃G,L,#i⦄ >[h] ⦃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 #I #G #L #i #IH #HT +fact cnv_cpm_conf_lpr_delta_delta_aux (h) (a) (I) (G) (L) (i): + (∀G0,L0,T0. ❪G,L,#i❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫⊢#i![h,a] → + ∀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. +#h #a #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 @@ -102,41 +102,41 @@ elim (cpms_lifts_sn … HVX1 … HLK1 … HXV1) -XV1 -HLK1 #W1 #HVW1 #HXW1 qed-. fact cnv_cpm_conf_lpr_delta_ell_aux (L) (K1) (K2) (V) (W) (i): - ⬇*[i]L ≘ K1.ⓓV → ⬇*[i]L ≘ K2.ⓛW → ⊥. + ⇩*[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) (p) (I) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓑ{p,I}V.T⦄ >[h] ⦃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 #p #I #G0 #L0 #V0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_bind_bind_aux (h) (a) (p) (I) (G) (L) (V) (T): + (∀G0,L0,T0. ❪G,L,ⓑ[p,I]V.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓑ[p,I]V.T ![h,a] → + ∀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. +#h #a #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_sub … IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ] +elim (cnv_cpm_conf_lpr_sub … 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) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h] ⦃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 → - ∀T2. ⬆*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 → - ∀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 #G0 #L0 #V0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_bind_zeta_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ❪G,L,+ⓓV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ +ⓓV.T ![h,a] → + ∀V1. ❪G,L❫ ⊢V ➡[h] V1 → ∀n1,T1. ❪G,L.ⓓV❫ ⊢ T ➡[n1,h] T1 → + ∀T2. ⇧*[1]T2 ≘ T → ∀n2,XT2. ❪G,L❫ ⊢ T2 ➡[n2,h] XT2 → + ∀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. +#h #a #G0 #L0 #V0 #T0 #IH #H0 #V1 #HV01 #n1 #T1 #HT01 #T2 #HT20 #n2 #XT2 #HXT2 #L1 #HL01 #L2 #HL02 elim (cnv_inv_bind … H0) -H0 #_ #HT0 lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0 -[ /3 width=3 by drops_refl, drops_drop/ ] #HT2 +[ /3 width=3 by drops_refl, drops_drop/ ] #HT2 elim (cpm_inv_lifts_sn … HT01 (Ⓣ) … L0 … HT20) -HT01 [| /3 width=1 by drops_refl, drops_drop/ ] #XT1 #HXT1 #HXT12 elim (cnv_cpm_conf_lpr_sub … IH … HXT12 … HXT2 … HL01 … HL02) @@ -144,14 +144,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HXT12 … HXT2 … HL01 … HL02) /3 width=3 by cpms_zeta, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_zeta_zeta_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) → - ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] → - ∀T1. ⬆*[1]T1 ≘ T → ∀T2. ⬆*[1]T2 ≘ T → - ∀n1,XT1. ⦃G,L⦄ ⊢ T1 ➡[n1,h] XT1 → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 → - ∀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 #G0 #L0 #V0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_zeta_zeta_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ❪G,L,+ⓓV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ +ⓓV.T ![h,a] → + ∀T1. ⇧*[1]T1 ≘ T → ∀T2. ⇧*[1]T2 ≘ T → + ∀n1,XT1. ❪G,L❫ ⊢ T1 ➡[n1,h] XT1 → ∀n2,XT2. ❪G,L❫ ⊢ T2 ➡[n2,h] XT2 → + ∀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. +#h #a #G0 #L0 #V0 #T0 #IH #H0 #T1 #HT10 #T2 #HT20 #n1 #XT1 #HXT1 #n2 #XT2 #HXT2 #L1 #HL01 #L2 #HL02 elim (cnv_inv_bind … H0) -H0 #_ #HT0 @@ -163,14 +163,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HXT1 … HXT2 … HL01 … HL02) /2 width=3 by ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_appl_appl_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓐV.T⦄ >[h] ⦃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 #G0 #L0 #V0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_appl_appl_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ❪G,L,ⓐV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓐV.T ![h,a] → + ∀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. +#h #a #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 @@ -180,15 +180,15 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w /3 width=5 by cpms_appl_dx, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_appl_beta_aux (a) (h) (p) (G) (L) (V) (W) (T): - (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h] ⦃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 #p #G0 #L0 #V0 #W0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_appl_beta_aux (h) (a) (p) (G) (L) (V) (W) (T): + (∀G0,L0,T0. ❪G,L,ⓐV.ⓛ[p]W.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓐV.ⓛ[p]W.T ![h,a] → + ∀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. +#h #a #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 @@ -202,16 +202,16 @@ lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 [ /2 width=1 by lsubr_ /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) (p) (G) (L) (V) (W) (T): - (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h] ⦃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 #p #G0 #L0 #V0 #W0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_appl_theta_aux (h) (a) (p) (G) (L) (V) (W) (T): + (∀G0,L0,T0. ❪G,L,ⓐV.ⓓ[p]W.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓐV.ⓓ[p]W.T ![h,a] → + ∀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. +#h #a #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 @@ -225,7 +225,7 @@ elim (cpm_inv_abbr1 … HX) -HX * #T #HT1 #HT2 -L0 -V0 -W0 -T0 /4 width=7 by cpms_theta_dx, cpms_appl_dx, cpms_bind_dx, ex2_intro/ | #X0 #HXT0 #H1X0 #H destruct - lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0 [ /3 width=3 by drops_refl, drops_drop/ ] #H2X0 + lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0 [ /3 width=3 by drops_refl, drops_drop/ ] #H2X0 elim (cpm_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02 [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02 elim (cnv_cpm_conf_lpr_sub … IH … H1X0 … HX02 … HL01 … HL02) [|*: /4 width=5 by fqup_fpbg, fqup_strap1, fqu_drop/ ] #T #HT1 #HT2 -L0 -V0 -W0 -T0 @@ -233,15 +233,15 @@ elim (cpm_inv_abbr1 … HX) -HX * ] qed-. -fact cnv_cpm_conf_lpr_beta_beta_aux (a) (h) (p) (G) (L) (V) (W) (T): - (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h] ⦃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 #p #G0 #L0 #V0 #W0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_beta_beta_aux (h) (a) (p) (G) (L) (V) (W) (T): + (∀G0,L0,T0. ❪G,L,ⓐV.ⓛ[p]W.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓐV.ⓛ[p]W.T ![h,a] → + ∀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. +#h #a #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 @@ -255,16 +255,16 @@ lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_be /4 width=5 by cpms_bind_dx, cpm_eps, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_theta_theta_aux (a) (h) (p) (G) (L) (V) (W) (T): - (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h] ⦃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 #p #G0 #L0 #V0 #W0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_theta_theta_aux (h) (a) (p) (G) (L) (V) (W) (T): + (∀G0,L0,T0. ❪G,L,ⓐV.ⓓ[p]W.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓐV.ⓓ[p]W.T ![h,a] → + ∀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. +#h #a #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 @@ -278,14 +278,14 @@ lapply (cpm_lifts_bi … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2 … HVU) -V2 -V [ /3 /4 width=7 by cpms_appl_dx, cpms_bind_dx, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_cast_cast_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃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 #G0 #L0 #V0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_cast_cast_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓝV.T ![h,a] → + ∀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. +#h #a #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 @@ -295,14 +295,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w /3 width=5 by cpms_cast, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_cast_epsilon_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃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 #G0 #L0 #V0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_cast_epsilon_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓝV.T ![h,a] → + ∀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. +#h #a #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 @@ -311,15 +311,15 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w /3 width=3 by cpms_eps, ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_cast_ee_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃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 #G0 #L0 #V0 #T0 #IH2 #IH1 #H0 +fact cnv_cpm_conf_lpr_cast_ee_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) → + (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓝV.T ![h,a] → + ∀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. +#h #a #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 @@ -334,13 +334,13 @@ lapply (cpms_trans … HT1 … HTU) -T [h] ⦃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 #G0 #L0 #V0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_epsilon_epsilon_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓝV.T ![h,a] → + ∀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. +#h #a #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 @@ -349,14 +349,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w /2 width=3 by ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_epsilon_ee_aux (a) (h) (G) (L) (V) (T): - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) → - (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h] ⦃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 #G0 #L0 #V0 #T0 #IH2 #IH1 #H0 +fact cnv_cpm_conf_lpr_epsilon_ee_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) → + (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓝV.T ![h,a] → + ∀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. +#h #a #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 @@ -371,13 +371,13 @@ lapply (cpms_trans … HT1 … HTU) -T [h] ⦃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 #G0 #L0 #V0 #T0 #IH #H0 +fact cnv_cpm_conf_lpr_ee_ee_aux (h) (a) (G) (L) (V) (T): + (∀G0,L0,T0. ❪G,L,ⓝV.T❫ >[h] ❪G0,L0,T0❫ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) → + ❪G,L❫ ⊢ ⓝV.T ![h,a] → + ∀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. +#h #a #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 @@ -386,12 +386,12 @@ elim (cnv_cpm_conf_lpr_sub … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 w /2 width=3 by ex2_intro/ qed-. -fact cnv_cpm_conf_lpr_aux (a) (h): - ∀G0,L0,T0. - (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → - (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃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 #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]] +fact cnv_cpm_conf_lpr_aux (h) (a): + ∀G0,L0,T0. + (∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) → + (∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_conf_lpr h a G1 L1 T1. +#h #a #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 * @@ -423,7 +423,7 @@ fact cnv_cpm_conf_lpr_aux (a) (h): @(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 -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 + | #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2