-lemma cpg_inv_appl1: â\88\80Rt,c,h,G,L,V1,U1,U2. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.U1 â¬\88[Rt, c, h] U2 →
- â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[Rt, cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88[Rt, cT, h] T2 &
- U2 = â\93\90V2.T2 & c = ((â\86\93cV)∨cT)
- | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[Rt, cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[Rt, cW, h] W2 & â¦\83G, L.â\93\9bW1â¦\84 â\8a¢ T1 â¬\88[Rt, cT, h] 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. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[Rt, cV, h] V & â¬\86*[1] V â\89\98 V2 & â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\88[Rt, cW, h] W2 & â¦\83G, L.â\93\93W1â¦\84 â\8a¢ T1 â¬\88[Rt, cT, h] T2 &
- U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
+lemma cpg_inv_appl1: â\88\80Rt,c,h,G,L,V1,U1,U2. â\9dªG,Lâ\9d« â\8a¢ â\93\90V1.U1 â¬\88[Rt,c,h] U2 →
+ â\88¨â\88¨ â\88\83â\88\83cV,cT,V2,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â¬\88[Rt,cV,h] V2 & â\9dªG,Lâ\9d« â\8a¢ U1 â¬\88[Rt,cT,h] T2 &
+ U2 = â\93\90V2.T2 & c = ((â\86\95*cV)∨cT)
+ | â\88\83â\88\83cV,cW,cT,p,V2,W1,W2,T1,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â¬\88[Rt,cV,h] V2 & â\9dªG,Lâ\9d« â\8a¢ W1 â¬\88[Rt,cW,h] W2 & â\9dªG,L.â\93\9bW1â\9d« â\8a¢ T1 â¬\88[Rt,cT,h] 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[Rt,cV,h] V & â\87§[1] V â\89\98 V2 & â\9dªG,Lâ\9d« â\8a¢ W1 â¬\88[Rt,cW,h] W2 & â\9dªG,L.â\93\93W1â\9d« â\8a¢ T1 â¬\88[Rt,cT,h] T2 &
+ U1 = ⓓ[p]W1.T1 & U2 = ⓓ[p]W2.ⓐV2.T2 & c = ((↕*cV)∨(↕*cW)∨cT)+𝟙𝟘.