(* Sub diamond propery with t-bound rt-transition for terms *****************)
fact cnv_cpm_conf_lpr_atom_atom_aux (h) (G) (L1) (L2) (I):
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93ª{I} â\9e¡*[0,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93ª{I} ➡*[O,h] T.
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93ª[I] â\9e¡*[0,h] T & â\9dªG,L2â\9d« â\8a¢ â\93ª[I] ➡*[O,h] T.
/2 width=3 by ex2_intro/ qed-.
fact cnv_cpm_conf_lpr_atom_ess_aux (h) (G) (L1) (L2) (s):
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\8b\86s â\9e¡*[1,h] T & â¦\83G,L2â¦\84 ⊢ ⋆(⫯[h]s) ➡*[h] T.
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\8b\86s â\9e¡*[1,h] T & â\9dªG,L2â\9d« ⊢ ⋆(⫯[h]s) ➡*[h] T.
/3 width=3 by cpm_cpms, ex2_intro/ qed-.
fact cnv_cpm_conf_lpr_atom_delta_aux (h) (a) (G) (L) (i):
- (â\88\80G0,L0,T0. â¦\83G,L,#iâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84⊢#i![h,a] →
- ∀K,V. ⇩*[i]L ≘ K.ⓓV →
- â\88\80n,XV. â¦\83G,Kâ¦\84 ⊢ V ➡[n,h] XV →
- ∀X. ⇧*[↑i]XV ≘ X →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ #i â\9e¡*[n,h] T & â¦\83G,L2â¦\84 ⊢ X ➡*[h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,#iâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d«⊢#i![h,a] →
+ ∀K,V. ⇩[i]L ≘ K.ⓓV →
+ â\88\80n,XV. â\9dªG,Kâ\9d« ⊢ V ➡[n,h] XV →
+ ∀X. ⇧[↑i]XV ≘ X →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ #i â\9e¡*[n,h] T & â\9dªG,L2â\9d« ⊢ 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
qed-.
fact cnv_cpm_conf_lpr_atom_ell_aux (h) (a) (G) (L) (i):
- (â\88\80G0,L0,T0. â¦\83G,L,#iâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84⊢#i![h,a] →
- ∀K,W. ⇩*[i]L ≘ K.ⓛW →
- â\88\80n,XW. â¦\83G,Kâ¦\84 ⊢ W ➡[n,h] XW →
- ∀X. ⇧*[↑i]XW ≘ X →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ #i â\9e¡*[â\86\91n,h] T & â¦\83G,L2â¦\84 ⊢ X ➡*[h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,#iâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d«⊢#i![h,a] →
+ ∀K,W. ⇩[i]L ≘ K.ⓛW →
+ â\88\80n,XW. â\9dªG,Kâ\9d« ⊢ W ➡[n,h] XW →
+ ∀X. ⇧[↑i]XW ≘ X →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ #i â\9e¡*[â\86\91n,h] T & â\9dªG,L2â\9d« ⊢ 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
qed-.
fact cnv_cpm_conf_lpr_delta_delta_aux (h) (a) (I) (G) (L) (i):
- (â\88\80G0,L0,T0. â¦\83G,L,#iâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84⊢#i![h,a] →
- ∀K1,V1. ⇩*[i]L ≘ K1.ⓑ{I}V1 → ∀K2,V2. ⇩*[i]L ≘ K2.ⓑ{I}V2 →
- â\88\80n1,XV1. â¦\83G,K1â¦\84 â\8a¢ V1 â\9e¡[n1,h] XV1 â\86\92 â\88\80n2,XV2. â¦\83G,K2â¦\84 ⊢ V2 ➡[n2,h] XV2 →
- ∀X1. ⇧*[↑i]XV1 ≘ X1 → ∀X2. ⇧*[↑i]XV2 ≘ X2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ X1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 ⊢ X2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,#iâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d«⊢#i![h,a] →
+ ∀K1,V1. ⇩[i]L ≘ K1.ⓑ[I]V1 → ∀K2,V2. ⇩[i]L ≘ K2.ⓑ[I]V2 →
+ â\88\80n1,XV1. â\9dªG,K1â\9d« â\8a¢ V1 â\9e¡[n1,h] XV1 â\86\92 â\88\80n2,XV2. â\9dªG,K2â\9d« ⊢ V2 ➡[n2,h] XV2 →
+ ∀X1. ⇧[↑i]XV1 ≘ X1 → ∀X2. ⇧[↑i]XV2 ≘ X2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ X1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« ⊢ 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
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 (h) (a) (p) (I) (G) (L) (V) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\91{p,I}V.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 â\8a¢ â\93\91{p,I}V.T ![h,a] →
- â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 ⊢ V ➡[h] V2 →
- â\88\80n1,T1. â¦\83G,L.â\93\91{I}Vâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,L.â\93\91{I}Vâ¦\84 ⊢ T ➡[n2,h] T2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\91{p,I}V2.T2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\91[p,I]V.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« â\8a¢ â\93\91[p,I]V.T ![h,a] →
+ â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h] V2 →
+ â\88\80n1,T1. â\9dªG,L.â\93\91[I]Vâ\9d« â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\91[I]Vâ\9d« ⊢ T ➡[n2,h] T2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\91[p,I]V1.T1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« â\8a¢ â\93\91[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 (h) (a) (G) (L) (V) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,+â\93\93V.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 ⊢ +ⓓV.T ![h,a] →
- â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢V â\9e¡[h] V1 â\86\92 â\88\80n1,T1. â¦\83G,L.â\93\93Vâ¦\84 ⊢ T ➡[n1,h] T1 →
- ∀T2. ⇧*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ +â\93\93V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 ⊢ XT2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,+â\93\93V.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« ⊢ +ⓓV.T ![h,a] →
+ â\88\80V1. â\9dªG,Lâ\9d« â\8a¢V â\9e¡[h] V1 â\86\92 â\88\80n1,T1. â\9dªG,L.â\93\93Vâ\9d« ⊢ T ➡[n1,h] T1 →
+ ∀T2. ⇧[1]T2 ≘ T → ∀n2,XT2. ❪G,L❫ ⊢ T2 ➡[n2,h] XT2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ +â\93\93V1.T1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« ⊢ 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
qed-.
fact cnv_cpm_conf_lpr_zeta_zeta_aux (h) (a) (G) (L) (V) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,+â\93\93V.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 ⊢ +ⓓV.T ![h,a] →
- ∀T1. ⇧*[1]T1 ≘ T → ∀T2. ⇧*[1]T2 ≘ T →
- â\88\80n1,XT1. â¦\83G,Lâ¦\84 â\8a¢ T1 â\9e¡[n1,h] XT1 â\86\92 â\88\80n2,XT2. â¦\83G,Lâ¦\84 ⊢ T2 ➡[n2,h] XT2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ XT1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 ⊢ XT2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,+â\93\93V.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« ⊢ +ⓓV.T ![h,a] →
+ ∀T1. ⇧[1]T1 ≘ T → ∀T2. ⇧[1]T2 ≘ T →
+ â\88\80n1,XT1. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[n1,h] XT1 â\86\92 â\88\80n2,XT2. â\9dªG,Lâ\9d« ⊢ T2 ➡[n2,h] XT2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ XT1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« ⊢ 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
qed-.
fact cnv_cpm_conf_lpr_appl_appl_aux (h) (a) (G) (L) (V) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\90V.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 ⊢ ⓐV.T ![h,a] →
- â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 ⊢ V ➡[h] V2 →
- â\88\80n1,T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,Lâ¦\84 ⊢ T ➡[n2,h] T2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\90V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 ⊢ ⓐV2.T2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« ⊢ ⓐV.T ![h,a] →
+ â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h] V2 →
+ â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â\9dªG,Lâ\9d« ⊢ T ➡[n2,h] T2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\90V1.T1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« ⊢ ⓐ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
qed-.
fact cnv_cpm_conf_lpr_appl_beta_aux (h) (a) (p) (G) (L) (V) (W) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\90V.â\93\9b{p}W.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.T ![h,a] →
- â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 ⊢ V ➡[h] V2 →
- â\88\80W2. â¦\83G,Lâ¦\84 ⊢ W ➡[h] W2 →
- â\88\80n1,T1. â¦\83G,Lâ¦\84 â\8a¢ â\93\9b{p}W.T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,L.â\93\9bWâ¦\84 ⊢ T ➡[n2,h] T2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\90V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\93{p}ⓝW2.V2.T2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\9b[p]W.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.T ![h,a] →
+ â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h] V2 →
+ â\88\80W2. â\9dªG,Lâ\9d« ⊢ W ➡[h] W2 →
+ â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ â\93\9b[p]W.T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\9bWâ\9d« ⊢ T ➡[n2,h] T2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\90V1.T1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« â\8a¢ â\93\93[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
qed-.
fact cnv_cpm_conf_lpr_appl_theta_aux (h) (a) (p) (G) (L) (V) (W) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\90V.â\93\93{p}W.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\93{p}W.T ![h,a] →
- â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 ⊢ V ➡[h] V2 →
- â\88\80W2. â¦\83G,Lâ¦\84 ⊢ W ➡[h] W2 →
- â\88\80n1,T1. â¦\83G,Lâ¦\84 â\8a¢ â\93\93{p}W.T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,L.â\93\93Wâ¦\84 ⊢ T ➡[n2,h] T2 →
- ∀U2. ⇧*[1]V2 ≘ U2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\90V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\93{p}W2.ⓐU2.T2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\93[p]W.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\93[p]W.T ![h,a] →
+ â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h] V2 →
+ â\88\80W2. â\9dªG,Lâ\9d« ⊢ W ➡[h] W2 →
+ â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ â\93\93[p]W.T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\93Wâ\9d« ⊢ T ➡[n2,h] T2 →
+ ∀U2. ⇧[1]V2 ≘ U2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\90V1.T1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« â\8a¢ â\93\93[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
qed-.
fact cnv_cpm_conf_lpr_beta_beta_aux (h) (a) (p) (G) (L) (V) (W) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\90V.â\93\9b{p}W.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.T ![h,a] →
- â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 ⊢ V ➡[h] V2 →
- â\88\80W1. â¦\83G,Lâ¦\84 â\8a¢ W â\9e¡[h] W1 â\86\92 â\88\80W2. â¦\83G,Lâ¦\84 ⊢ W ➡[h] W2 →
- â\88\80n1,T1. â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,L.â\93\9bWâ¦\84 ⊢ T ➡[n2,h] T2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\93{p}â\93\9dW1.V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\93{p}ⓝW2.V2.T2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\9b[p]W.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.T ![h,a] →
+ â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h] V2 →
+ â\88\80W1. â\9dªG,Lâ\9d« â\8a¢ W â\9e¡[h] W1 â\86\92 â\88\80W2. â\9dªG,Lâ\9d« ⊢ W ➡[h] W2 →
+ â\88\80n1,T1. â\9dªG,L.â\93\9bWâ\9d« â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\9bWâ\9d« ⊢ T ➡[n2,h] T2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\93[p]â\93\9dW1.V1.T1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« â\8a¢ â\93\93[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
qed-.
fact cnv_cpm_conf_lpr_theta_theta_aux (h) (a) (p) (G) (L) (V) (W) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\90V.â\93\93{p}W.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\93{p}W.T ![h,a] →
- â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 ⊢ V ➡[h] V2 →
- â\88\80W1. â¦\83G,Lâ¦\84 â\8a¢ W â\9e¡[h] W1 â\86\92 â\88\80W2. â¦\83G,Lâ¦\84 ⊢ W ➡[h] W2 →
- â\88\80n1,T1. â¦\83G,L.â\93\93Wâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,L.â\93\93Wâ¦\84 ⊢ T ➡[n2,h] T2 →
- ∀U1. ⇧*[1]V1 ≘ U1 → ∀U2. ⇧*[1]V2 ≘ U2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\93{p}W1.â\93\90U1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\93{p}W2.ⓐU2.T2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\93[p]W.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\93[p]W.T ![h,a] →
+ â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h] V2 →
+ â\88\80W1. â\9dªG,Lâ\9d« â\8a¢ W â\9e¡[h] W1 â\86\92 â\88\80W2. â\9dªG,Lâ\9d« ⊢ W ➡[h] W2 →
+ â\88\80n1,T1. â\9dªG,L.â\93\93Wâ\9d« â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\93Wâ\9d« ⊢ T ➡[n2,h] T2 →
+ ∀U1. ⇧[1]V1 ≘ U1 → ∀U2. ⇧[1]V2 ≘ U2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\93[p]W1.â\93\90U1.T1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« â\8a¢ â\93\93[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
qed-.
fact cnv_cpm_conf_lpr_cast_cast_aux (h) (a) (G) (L) (V) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 ⊢ ⓝV.T ![h,a] →
- â\88\80n1,V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n1,h] V1 â\86\92 â\88\80n2,V2. â¦\83G,Lâ¦\84 ⊢ V ➡[n2,h] V2 →
- â\88\80T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80T2. â¦\83G,Lâ¦\84 ⊢ T ➡[n2,h] T2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\9dV1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 ⊢ ⓝV2.T2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« ⊢ ⓝV.T ![h,a] →
+ â\88\80n1,V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[n1,h] V1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« ⊢ V ➡[n2,h] V2 →
+ â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80T2. â\9dªG,Lâ\9d« ⊢ T ➡[n2,h] T2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\9dV1.T1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« ⊢ ⓝ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
qed-.
fact cnv_cpm_conf_lpr_cast_epsilon_aux (h) (a) (G) (L) (V) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 ⊢ ⓝV.T ![h,a] →
- â\88\80n1,V1. â¦\83G,Lâ¦\84 ⊢ V ➡[n1,h] V1 →
- â\88\80T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,Lâ¦\84 ⊢ T ➡[n2,h] T2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\9dV1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 ⊢ T2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« ⊢ ⓝV.T ![h,a] →
+ â\88\80n1,V1. â\9dªG,Lâ\9d« ⊢ V ➡[n1,h] V1 →
+ â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â\9dªG,Lâ\9d« ⊢ T ➡[n2,h] T2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\9dV1.T1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« ⊢ 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
qed-.
fact cnv_cpm_conf_lpr_cast_ee_aux (h) (a) (G) (L) (V) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 ⊢ ⓝV.T ![h,a] →
- â\88\80n1,V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n1,h] V1 â\86\92 â\88\80n2,V2. â¦\83G,Lâ¦\84 ⊢ V ➡[n2,h] V2 →
- â\88\80T1. â¦\83G,Lâ¦\84 ⊢ T ➡[n1,h] T1 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\9dV1.T1 â\9e¡*[â\86\91n2-n1,h] T & â¦\83G,L2â¦\84 ⊢ V2 ➡*[n1-↑n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« ⊢ ⓝV.T ![h,a] →
+ â\88\80n1,V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[n1,h] V1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« ⊢ V ➡[n2,h] V2 →
+ â\88\80T1. â\9dªG,Lâ\9d« ⊢ T ➡[n1,h] T1 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\9dV1.T1 â\9e¡*[â\86\91n2-n1,h] T & â\9dªG,L2â\9d« ⊢ 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
qed-.
fact cnv_cpm_conf_lpr_epsilon_epsilon_aux (h) (a) (G) (L) (V) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 ⊢ ⓝV.T ![h,a] →
- â\88\80n1,T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,Lâ¦\84 ⊢ T ➡[n2,h] T2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 ⊢ T2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« ⊢ ⓝV.T ![h,a] →
+ â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â\9dªG,Lâ\9d« ⊢ T ➡[n2,h] T2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ T1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« ⊢ T2 ➡*[n1-n2,h] T.
#h #a #G0 #L0 #V0 #T0 #IH #H0
#n1 #T1 #HT01 #n2 #T2 #HT02
#L1 #HL01 #L2 #HL02
qed-.
fact cnv_cpm_conf_lpr_epsilon_ee_aux (h) (a) (G) (L) (V) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 ⊢ ⓝV.T ![h,a] →
- â\88\80n1,T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,V2. â¦\83G,Lâ¦\84 ⊢ V ➡[n2,h] V2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ T1 â\9e¡*[â\86\91n2-n1,h] T & â¦\83G,L2â¦\84 ⊢ V2 ➡*[n1-↑n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« ⊢ ⓝV.T ![h,a] →
+ â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« ⊢ V ➡[n2,h] V2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ T1 â\9e¡*[â\86\91n2-n1,h] T & â\9dªG,L2â\9d« ⊢ V2 ➡*[n1-↑n2,h] T.
#h #a #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
#n1 #T1 #HT01 #n2 #V2 #HV02
#L1 #HL01 #L2 #HL02
qed-.
fact cnv_cpm_conf_lpr_ee_ee_aux (h) (a) (G) (L) (V) (T):
- (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â¦\83G,Lâ¦\84 ⊢ ⓝV.T ![h,a] →
- â\88\80n1,V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n1,h] V1 â\86\92 â\88\80n2,V2. â¦\83G,Lâ¦\84 ⊢ V ➡[n2,h] V2 →
- â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 ⊢ ➡[h] L2 →
- â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ V1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 ⊢ V2 ➡*[n1-n2,h] T.
+ (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« >[h] â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9dªG,Lâ\9d« ⊢ ⓝV.T ![h,a] →
+ â\88\80n1,V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[n1,h] V1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« ⊢ V ➡[n2,h] V2 →
+ â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h] L2 →
+ â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ V1 â\9e¡*[n2-n1,h] T & â\9dªG,L2â\9d« ⊢ V2 ➡*[n1-n2,h] T.
#h #a #G0 #L0 #V0 #T0 #IH #H0
#n1 #V1 #HV01 #n2 #V2 #HV02
#L1 #HL01 #L2 #HL02
fact cnv_cpm_conf_lpr_aux (h) (a):
∀G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G1,L1,T1â¦\84 → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G1,L1,T1â¦\84 → IH_cnv_cpms_conf_lpr h a G1 L1 T1) →
+ (â\88\80G1,L1,T1. â\9dªG0,L0,T0â\9d« >[h] â\9dªG1,L1,T1â\9d« → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
+ (â\88\80G1,L1,T1. â\9dªG0,L0,T0â\9d« >[h] â\9dªG1,L1,T1â\9d« → 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