(* 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⦄ ⊢ ⋆(next 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] →
- â\88\80K,V. â¬\87*[i]L ≘ K.ⓓV →
+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] →
+ â\88\80K,V. â\87©*[i]L ≘ K.ⓓV →
∀n,XV. ⦃G,K⦄ ⊢ V ➡[n,h] XV →
- â\88\80X. â¬\86*[↑i]XV ≘ X →
+ â\88\80X. â\87§*[↑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
+#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
/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] →
- â\88\80K,W. â¬\87*[i]L ≘ K.ⓛW →
+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] →
+ â\88\80K,W. â\87©*[i]L ≘ K.ⓛW →
∀n,XW. ⦃G,K⦄ ⊢ W ➡[n,h] XW →
- â\88\80X. â¬\86*[↑i]XW ≘ X →
+ â\88\80X. â\87§*[↑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
+#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
/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] →
- â\88\80K1,V1. â¬\87*[i]L â\89\98 K1.â\93\91{I}V1 â\86\92 â\88\80K2,V2. â¬\87*[i]L ≘ K2.ⓑ{I}V2 →
+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] →
+ â\88\80K1,V1. â\87©*[i]L â\89\98 K1.â\93\91{I}V1 â\86\92 â\88\80K2,V2. â\87©*[i]L ≘ K2.ⓑ{I}V2 →
∀n1,XV1. ⦃G,K1⦄ ⊢ V1 ➡[n1,h] XV1 → ∀n2,XV2. ⦃G,K2⦄ ⊢ V2 ➡[n2,h] XV2 →
- â\88\80X1. â¬\86*[â\86\91i]XV1 â\89\98 X1 â\86\92 â\88\80X2. â¬\86*[↑i]XV2 ≘ X2 →
+ â\88\80X1. â\87§*[â\86\91i]XV1 â\89\98 X1 â\86\92 â\88\80X2. â\87§*[↑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
+#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
qed-.
fact cnv_cpm_conf_lpr_delta_ell_aux (L) (K1) (K2) (V) (W) (i):
- â¬\87*[i]L â\89\98 K1.â\93\93V â\86\92 â¬\87*[i]L ≘ K2.ⓛW → ⊥.
+ â\87©*[i]L â\89\98 K1.â\93\93V â\86\92 â\87©*[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] →
+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.
-#a #h #p #I #G0 #L0 #V0 #T0 #IH #H0
+#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
/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] →
+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 →
- â\88\80T2. â¬\86*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 →
+ â\88\80T2. â\87§*[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
+#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
/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] →
- â\88\80T1. â¬\86*[1]T1 â\89\98 T â\86\92 â\88\80T2. â¬\86*[1]T2 ≘ T →
+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] →
+ â\88\80T1. â\87§*[1]T1 â\89\98 T â\86\92 â\88\80T2. â\87§*[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
+#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
/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] →
+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.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+#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
/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] →
+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.
-#a #h #p #G0 #L0 #V0 #W0 #T0 #IH #H0
+#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
/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] →
+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 →
- â\88\80U2. â¬\86*[1]V2 ≘ U2 →
+ â\88\80U2. â\87§*[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
+#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
]
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] →
+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.
-#a #h #p #G0 #L0 #V0 #W0 #T0 #IH #H0
+#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
/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] →
+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 →
- â\88\80U1. â¬\86*[1]V1 â\89\98 U1 â\86\92 â\88\80U2. â¬\86*[1]V2 ≘ U2 →
+ â\88\80U1. â\87§*[1]V1 â\89\98 U1 â\86\92 â\88\80U2. â\87§*[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
+#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
/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] →
+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.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+#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
/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] →
+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.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+#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
/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] →
+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.
-#a #h #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
+#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
/3 width=3 by cpms_eps, ex2_intro/
qed-.
-fact cnv_cpm_conf_lpr_epsilon_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] →
+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.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+#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
/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] →
+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.
-#a #h #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
+#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
/2 width=3 by ex2_intro/
qed-.
-fact cnv_cpm_conf_lpr_ee_ee_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] →
+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.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+#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
/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 *