- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93ª[I] â\9e¡*[h,0] T & â\9dªG,L2â\9d« ⊢ ⓪[I] ➡*[h,0] T.
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\93ª[I] â\9e¡*[h,0] T & â\9d¨G,L2â\9d© ⊢ ⓪[I] ➡*[h,0] T.
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\8b\86s â\9e¡*[h,1] T & â\9dªG,L2â\9d« ⊢ ⋆(⫯[h]s) ➡*[h,0] T.
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\8b\86s â\9e¡*[h,1] T & â\9d¨G,L2â\9d© ⊢ ⋆(⫯[h]s) ➡*[h,0] T.
- (â\88\80G0,L0,T0. â\9dªG,L,#iâ\9d« > â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â\9dªG,Lâ\9d«⊢#i![h,a] →
+ (â\88\80G0,L0,T0. â\9d¨G,L,#iâ\9d© > â\9d¨G0,L0,T0â\9d© → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9d¨G,Lâ\9d©⊢#i![h,a] →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ #i â\9e¡*[h,n] T & â\9dªG,L2â\9d« ⊢ X ➡*[h,0] T.
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ #i â\9e¡*[h,n] T & â\9d¨G,L2â\9d© ⊢ X ➡*[h,0] 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
#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
- (â\88\80G0,L0,T0. â\9dªG,L,#iâ\9d« > â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â\9dªG,Lâ\9d«⊢#i![h,a] →
+ (â\88\80G0,L0,T0. â\9d¨G,L,#iâ\9d© > â\9d¨G0,L0,T0â\9d© → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9d¨G,Lâ\9d©⊢#i![h,a] →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ #i â\9e¡*[h,â\86\91n] T & â\9dªG,L2â\9d« ⊢ X ➡*[h,0] T.
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ #i â\9e¡*[h,â\86\91n] T & â\9d¨G,L2â\9d© ⊢ X ➡*[h,0] 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
#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
- (â\88\80G0,L0,T0. â\9dªG,L,#iâ\9d« > â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â\9dªG,Lâ\9d«⊢#i![h,a] →
+ (â\88\80G0,L0,T0. â\9d¨G,L,#iâ\9d© > â\9d¨G0,L0,T0â\9d© → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9d¨G,Lâ\9d©⊢#i![h,a] →
- â\88\80n1,XV1. â\9dªG,K1â\9d« â\8a¢ V1 â\9e¡[h,n1] XV1 â\86\92 â\88\80n2,XV2. â\9dªG,K2â\9d« ⊢ V2 ➡[h,n2] XV2 →
+ â\88\80n1,XV1. â\9d¨G,K1â\9d© â\8a¢ V1 â\9e¡[h,n1] XV1 â\86\92 â\88\80n2,XV2. â\9d¨G,K2â\9d© ⊢ V2 ➡[h,n2] XV2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ X1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ X2 ➡*[h,n1-n2] T.
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ X1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ X2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\91[p,I]V.Tâ\9d« > â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â\9dªG,Lâ\9d« ⊢ ⓑ[p,I]V.T ![h,a] →
- â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h,0] V2 →
- â\88\80n1,T1. â\9dªG,L.â\93\91[I]Vâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\91[I]Vâ\9d« ⊢ T ➡[h,n2] T2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\91[p,I]V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ ⓑ[p,I]V2.T2 ➡*[h,n1-n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\91[p,I]V.Tâ\9d© > â\9d¨G0,L0,T0â\9d© → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9d¨G,Lâ\9d© ⊢ ⓑ[p,I]V.T ![h,a] →
+ â\88\80V1. â\9d¨G,Lâ\9d© â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9d¨G,Lâ\9d© ⊢ V ➡[h,0] V2 →
+ â\88\80n1,T1. â\9d¨G,L.â\93\91[I]Vâ\9d© â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9d¨G,L.â\93\91[I]Vâ\9d© ⊢ T ➡[h,n2] T2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\93\91[p,I]V1.T1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ ⓑ[p,I]V2.T2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,+â\93\93V.Tâ\9d« > â\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,0] V1 â\86\92 â\88\80n1,T1. â\9dªG,L.â\93\93Vâ\9d« ⊢ T ➡[h,n1] T1 →
- â\88\80T2. â\87§[1]T2 â\89\98 T â\86\92 â\88\80n2,XT2. â\9dªG,Lâ\9d« ⊢ T2 ➡[h,n2] XT2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ +â\93\93V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ XT2 ➡*[h,n1-n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,+â\93\93V.Tâ\9d© > â\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,0] V1 â\86\92 â\88\80n1,T1. â\9d¨G,L.â\93\93Vâ\9d© ⊢ T ➡[h,n1] T1 →
+ â\88\80T2. â\87§[1]T2 â\89\98 T â\86\92 â\88\80n2,XT2. â\9d¨G,Lâ\9d© ⊢ T2 ➡[h,n2] XT2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ +â\93\93V1.T1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ XT2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,+â\93\93V.Tâ\9d« > â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â\9dªG,Lâ\9d« ⊢ +ⓓV.T ![h,a] →
+ (â\88\80G0,L0,T0. â\9d¨G,L,+â\93\93V.Tâ\9d© > â\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,XT1. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n1] XT1 â\86\92 â\88\80n2,XT2. â\9dªG,Lâ\9d« ⊢ T2 ➡[h,n2] XT2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ XT1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ XT2 ➡*[h,n1-n2] T.
+ â\88\80n1,XT1. â\9d¨G,Lâ\9d© â\8a¢ T1 â\9e¡[h,n1] XT1 â\86\92 â\88\80n2,XT2. â\9d¨G,Lâ\9d© ⊢ T2 ➡[h,n2] XT2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ XT1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ XT2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.Tâ\9d« > â\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,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h,0] V2 →
- â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,Lâ\9d« ⊢ T ➡[h,n2] T2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\90V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ ⓐV2.T2 ➡*[h,n1-n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\90V.Tâ\9d© > â\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,0] V1 â\86\92 â\88\80V2. â\9d¨G,Lâ\9d© ⊢ V ➡[h,0] V2 →
+ â\88\80n1,T1. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9d¨G,Lâ\9d© ⊢ T ➡[h,n2] T2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\93\90V1.T1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ ⓐV2.T2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\9b[p]W.Tâ\9d« > â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â\9dªG,Lâ\9d« ⊢ ⓐV.ⓛ[p]W.T ![h,a] →
- â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h,0] V2 →
- â\88\80W2. â\9dªG,Lâ\9d« ⊢ W ➡[h,0] W2 →
- â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ â\93\9b[p]W.T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\9bWâ\9d« ⊢ T ➡[h,n2] T2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\90V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ ⓓ[p]ⓝW2.V2.T2 ➡*[h,n1-n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\90V.â\93\9b[p]W.Tâ\9d© > â\9d¨G0,L0,T0â\9d© → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9d¨G,Lâ\9d© ⊢ ⓐV.ⓛ[p]W.T ![h,a] →
+ â\88\80V1. â\9d¨G,Lâ\9d© â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9d¨G,Lâ\9d© ⊢ V ➡[h,0] V2 →
+ â\88\80W2. â\9d¨G,Lâ\9d© ⊢ W ➡[h,0] W2 →
+ â\88\80n1,T1. â\9d¨G,Lâ\9d© â\8a¢ â\93\9b[p]W.T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9d¨G,L.â\93\9bWâ\9d© ⊢ T ➡[h,n2] T2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\93\90V1.T1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ ⓓ[p]ⓝW2.V2.T2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\93[p]W.Tâ\9d« > â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â\9dªG,Lâ\9d« ⊢ ⓐV.ⓓ[p]W.T ![h,a] →
- â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h,0] V2 →
- â\88\80W2. â\9dªG,Lâ\9d« ⊢ W ➡[h,0] W2 →
- â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ â\93\93[p]W.T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\93Wâ\9d« ⊢ T ➡[h,n2] T2 →
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\90V.â\93\93[p]W.Tâ\9d© > â\9d¨G0,L0,T0â\9d© → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9d¨G,Lâ\9d© ⊢ ⓐV.ⓓ[p]W.T ![h,a] →
+ â\88\80V1. â\9d¨G,Lâ\9d© â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9d¨G,Lâ\9d© ⊢ V ➡[h,0] V2 →
+ â\88\80W2. â\9d¨G,Lâ\9d© ⊢ W ➡[h,0] W2 →
+ â\88\80n1,T1. â\9d¨G,Lâ\9d© â\8a¢ â\93\93[p]W.T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9d¨G,L.â\93\93Wâ\9d© ⊢ T ➡[h,n2] T2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\90V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ ⓓ[p]W2.ⓐU2.T2 ➡*[h,n1-n2] T.
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\93\90V1.T1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ ⓓ[p]W2.ⓐU2.T2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\9b[p]W.Tâ\9d« > â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â\9dªG,Lâ\9d« ⊢ ⓐV.ⓛ[p]W.T ![h,a] →
- â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h,0] V2 →
- â\88\80W1. â\9dªG,Lâ\9d« â\8a¢ W â\9e¡[h,0] W1 â\86\92 â\88\80W2. â\9dªG,Lâ\9d« ⊢ W ➡[h,0] W2 →
- â\88\80n1,T1. â\9dªG,L.â\93\9bWâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\9bWâ\9d« ⊢ T ➡[h,n2] T2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\93[p]â\93\9dW1.V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ ⓓ[p]ⓝW2.V2.T2 ➡*[h,n1-n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\90V.â\93\9b[p]W.Tâ\9d© > â\9d¨G0,L0,T0â\9d© → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9d¨G,Lâ\9d© ⊢ ⓐV.ⓛ[p]W.T ![h,a] →
+ â\88\80V1. â\9d¨G,Lâ\9d© â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9d¨G,Lâ\9d© ⊢ V ➡[h,0] V2 →
+ â\88\80W1. â\9d¨G,Lâ\9d© â\8a¢ W â\9e¡[h,0] W1 â\86\92 â\88\80W2. â\9d¨G,Lâ\9d© ⊢ W ➡[h,0] W2 →
+ â\88\80n1,T1. â\9d¨G,L.â\93\9bWâ\9d© â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9d¨G,L.â\93\9bWâ\9d© ⊢ T ➡[h,n2] T2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\93\93[p]â\93\9dW1.V1.T1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ ⓓ[p]ⓝW2.V2.T2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\93[p]W.Tâ\9d« > â\9dªG0,L0,T0â\9d« → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
- â\9dªG,Lâ\9d« ⊢ ⓐV.ⓓ[p]W.T ![h,a] →
- â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« ⊢ V ➡[h,0] V2 →
- â\88\80W1. â\9dªG,Lâ\9d« â\8a¢ W â\9e¡[h,0] W1 â\86\92 â\88\80W2. â\9dªG,Lâ\9d« ⊢ W ➡[h,0] W2 →
- â\88\80n1,T1. â\9dªG,L.â\93\93Wâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\93Wâ\9d« ⊢ T ➡[h,n2] T2 →
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\90V.â\93\93[p]W.Tâ\9d© > â\9d¨G0,L0,T0â\9d© → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+ â\9d¨G,Lâ\9d© ⊢ ⓐV.ⓓ[p]W.T ![h,a] →
+ â\88\80V1. â\9d¨G,Lâ\9d© â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9d¨G,Lâ\9d© ⊢ V ➡[h,0] V2 →
+ â\88\80W1. â\9d¨G,Lâ\9d© â\8a¢ W â\9e¡[h,0] W1 â\86\92 â\88\80W2. â\9d¨G,Lâ\9d© ⊢ W ➡[h,0] W2 →
+ â\88\80n1,T1. â\9d¨G,L.â\93\93Wâ\9d© â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9d¨G,L.â\93\93Wâ\9d© ⊢ T ➡[h,n2] T2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\93[p]W1.â\93\90U1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ ⓓ[p]W2.ⓐU2.T2 ➡*[h,n1-n2] T.
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\93\93[p]W1.â\93\90U1.T1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ ⓓ[p]W2.ⓐU2.T2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\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¡[h,n1] V1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« ⊢ V ➡[h,n2] V2 →
- â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80T2. â\9dªG,Lâ\9d« ⊢ T ➡[h,n2] T2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\9dV1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ ⓝV2.T2 ➡*[h,n1-n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\9dV.Tâ\9d© > â\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¡[h,n1] V1 â\86\92 â\88\80n2,V2. â\9d¨G,Lâ\9d© ⊢ V ➡[h,n2] V2 →
+ â\88\80T1. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80T2. â\9d¨G,Lâ\9d© ⊢ T ➡[h,n2] T2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\93\9dV1.T1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ ⓝV2.T2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\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 ➡[h,n1] V1 →
- â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,Lâ\9d« ⊢ T ➡[h,n2] T2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\9dV1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ T2 ➡*[h,n1-n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\9dV.Tâ\9d© > â\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 ➡[h,n1] V1 →
+ â\88\80T1. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9d¨G,Lâ\9d© ⊢ T ➡[h,n2] T2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\93\9dV1.T1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ T2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\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« > â\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¡[h,n1] V1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« ⊢ V ➡[h,n2] V2 →
- â\88\80T1. â\9dªG,Lâ\9d« ⊢ T ➡[h,n1] T1 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\9dV1.T1 â\9e¡*[h,â\86\91n2-n1] T & â\9dªG,L2â\9d« ⊢ V2 ➡*[h,n1-↑n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\9dV.Tâ\9d© > â\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© > â\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¡[h,n1] V1 â\86\92 â\88\80n2,V2. â\9d¨G,Lâ\9d© ⊢ V ➡[h,n2] V2 →
+ â\88\80T1. â\9d¨G,Lâ\9d© ⊢ T ➡[h,n1] T1 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ â\93\9dV1.T1 â\9e¡*[h,â\86\91n2-n1] T & â\9d¨G,L2â\9d© ⊢ V2 ➡*[h,n1-↑n2] T.
#h #a #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
#n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01
#L1 #HL01 #L2 #HL02 -HV01
#h #a #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
#n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01
#L1 #HL01 #L2 #HL02 -HV01
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\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¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,Lâ\9d« ⊢ T ➡[h,n2] T2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ T2 ➡*[h,n1-n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\9dV.Tâ\9d© > â\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¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9d¨G,Lâ\9d© ⊢ T ➡[h,n2] T2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ T1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ T2 ➡*[h,n1-n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\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« > â\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¡[h,n1] T1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« ⊢ V ➡[h,n2] V2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ T1 â\9e¡*[h,â\86\91n2-n1] T & â\9dªG,L2â\9d« ⊢ V2 ➡*[h,n1-↑n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\9dV.Tâ\9d© > â\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© > â\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¡[h,n1] T1 â\86\92 â\88\80n2,V2. â\9d¨G,Lâ\9d© ⊢ V ➡[h,n2] V2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ T1 â\9e¡*[h,â\86\91n2-n1] T & â\9d¨G,L2â\9d© ⊢ V2 ➡*[h,n1-↑n2] T.
- (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\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¡[h,n1] V1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« ⊢ V ➡[h,n2] V2 →
- â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ V1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« ⊢ V2 ➡*[h,n1-n2] T.
+ (â\88\80G0,L0,T0. â\9d¨G,L,â\93\9dV.Tâ\9d© > â\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¡[h,n1] V1 â\86\92 â\88\80n2,V2. â\9d¨G,Lâ\9d© ⊢ V ➡[h,n2] V2 →
+ â\88\80L1. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G,Lâ\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G,L1â\9d© â\8a¢ V1 â\9e¡*[h,n2-n1] T & â\9d¨G,L2â\9d© ⊢ V2 ➡*[h,n1-n2] T.
- (â\88\80G1,L1,T1. â\9dªG0,L0,T0â\9d« > â\9dªG1,L1,T1â\9d« → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
- (â\88\80G1,L1,T1. â\9dªG0,L0,T0â\9d« > â\9dªG1,L1,T1â\9d« → IH_cnv_cpms_conf_lpr h a G1 L1 T1) →
+ (â\88\80G1,L1,T1. â\9d¨G0,L0,T0â\9d© > â\9d¨G1,L1,T1â\9d© → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
+ (â\88\80G1,L1,T1. â\9d¨G0,L0,T0â\9d© > â\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
∀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