- â\88\80V1,T1,X2. â\9dªG,Lâ\9d« ⊢ ⓐV1.T1 ➡*[h,n] X2 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â\9e¡*[h,0] V2 & â\9dªG,Lâ\9d« ⊢ T1 ➡*[h,n] T2 & X2 = ⓐV2.T2
- | â\88\83â\88\83n1,n2,p,W,T. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡*[h,n1] â\93\9b[p]W.T & â\9dªG,Lâ\9d« ⊢ ⓓ[p]ⓝW.V1.T ➡*[h,n2] X2 & n1 + n2 = n
- | â\88\83â\88\83n1,n2,p,V0,V2,V,T. â\9dªG,Lâ\9d« â\8a¢ V1 â\9e¡*[h,0] V0 & â\87§[1] V0 â\89\98 V2 & â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡*[h,n1] â\93\93[p]V.T & â\9dªG,Lâ\9d« ⊢ ⓓ[p]V.ⓐV2.T ➡*[h,n2] X2 & n1 + n2 = n.
+ â\88\80V1,T1,X2. â\9d¨G,Lâ\9d© ⊢ ⓐV1.T1 ➡*[h,n] X2 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. â\9d¨G,Lâ\9d© â\8a¢ V1 â\9e¡*[h,0] V2 & â\9d¨G,Lâ\9d© ⊢ T1 ➡*[h,n] T2 & X2 = ⓐV2.T2
+ | â\88\83â\88\83n1,n2,p,W,T. â\9d¨G,Lâ\9d© â\8a¢ T1 â\9e¡*[h,n1] â\93\9b[p]W.T & â\9d¨G,Lâ\9d© ⊢ ⓓ[p]ⓝW.V1.T ➡*[h,n2] X2 & n1 + n2 = n
+ | â\88\83â\88\83n1,n2,p,V0,V2,V,T. â\9d¨G,Lâ\9d© â\8a¢ V1 â\9e¡*[h,0] V0 & â\87§[1] V0 â\89\98 V2 & â\9d¨G,Lâ\9d© â\8a¢ T1 â\9e¡*[h,n1] â\93\93[p]V.T & â\9d¨G,Lâ\9d© ⊢ ⓓ[p]V.ⓐV2.T ➡*[h,n2] X2 & n1 + n2 = n.