- â\88\80V1,U1,U2. â\9dªG,Lâ\9d« ⊢ ⓐV1.U1 ⬈[Rs,Rk,c] U2 →
- â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â¬\88[Rs,Rk,cV] V2 & â\9dªG,Lâ\9d« ⊢ U1 ⬈[Rs,Rk,cT] T2 & U2 = ⓐV2.T2 & c = ((↕*cV)∨cT)
- | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â¬\88[Rs,Rk,cV] V2 & â\9dªG,Lâ\9d« â\8a¢ W1 â¬\88[Rs,Rk,cW] W2 & â\9dªG,L.â\93\9bW1â\9d« ⊢ T1 ⬈[Rs,Rk,cT] T2 & U1 = ⓛ[p]W1.T1 & U2 = ⓓ[p]ⓝW2.V2.T2 & c = ((↕*cV)∨(↕*cW)∨cT)+𝟙𝟘
- | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â¬\88[Rs,Rk,cV] V & â\87§[1] V â\89\98 V2 & â\9dªG,Lâ\9d« â\8a¢ W1 â¬\88[Rs,Rk,cW] W2 & â\9dªG,L.â\93\93W1â\9d« ⊢ T1 ⬈[Rs,Rk,cT] T2 & U1 = ⓓ[p]W1.T1 & U2 = ⓓ[p]W2.ⓐV2.T2 & c = ((↕*cV)∨(↕*cW)∨cT)+𝟙𝟘.
+ â\88\80V1,U1,U2. â\9d¨G,Lâ\9d© ⊢ ⓐV1.U1 ⬈[Rs,Rk,c] U2 →
+ â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â\9d¨G,Lâ\9d© â\8a¢ V1 â¬\88[Rs,Rk,cV] V2 & â\9d¨G,Lâ\9d© ⊢ U1 ⬈[Rs,Rk,cT] T2 & U2 = ⓐV2.T2 & c = ((↕*cV)∨cT)
+ | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â\9d¨G,Lâ\9d© â\8a¢ V1 â¬\88[Rs,Rk,cV] V2 & â\9d¨G,Lâ\9d© â\8a¢ W1 â¬\88[Rs,Rk,cW] W2 & â\9d¨G,L.â\93\9bW1â\9d© ⊢ T1 ⬈[Rs,Rk,cT] T2 & U1 = ⓛ[p]W1.T1 & U2 = ⓓ[p]ⓝW2.V2.T2 & c = ((↕*cV)∨(↕*cW)∨cT)+𝟙𝟘
+ | â\88\83â\88\83cV,cW,cT,p,V,V2,W1,W2,T1,T2. â\9d¨G,Lâ\9d© â\8a¢ V1 â¬\88[Rs,Rk,cV] V & â\87§[1] V â\89\98 V2 & â\9d¨G,Lâ\9d© â\8a¢ W1 â¬\88[Rs,Rk,cW] W2 & â\9d¨G,L.â\93\93W1â\9d© ⊢ T1 ⬈[Rs,Rk,cT] T2 & U1 = ⓓ[p]W1.T1 & U2 = ⓓ[p]W2.ⓐV2.T2 & c = ((↕*cV)∨(↕*cW)∨cT)+𝟙𝟘.