(* Basic_2A1: includes: cprs_theta_rc *)
theorem cpms_theta_rc (n) (h) (G) (L):
- â\88\80V1,V. â¦\83G,Lâ¦\84 â\8a¢ V1 â\9e¡[h] V â\86\92 â\88\80V2. â¬\86*[1] V ≘ V2 →
+ â\88\80V1,V. â¦\83G,Lâ¦\84 â\8a¢ V1 â\9e¡[h] V â\86\92 â\88\80V2. â\87§*[1] V ≘ V2 →
∀W1,T1,T2. ⦃G,L.ⓓW1⦄ ⊢ T1 ➡*[n,h] T2 →
∀W2. ⦃G,L⦄ ⊢ W1 ➡*[h] W2 →
∀p. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n,h] ⓓ{p}W2.ⓐV2.T2.
(* Basic_2A1: includes: cprs_theta *)
theorem cpms_theta (n) (h) (G) (L):
- â\88\80V,V2. â¬\86*[1] V ≘ V2 → ∀W1,W2. ⦃G,L⦄ ⊢ W1 ➡*[h] W2 →
+ â\88\80V,V2. â\87§*[1] V ≘ V2 → ∀W1,W2. ⦃G,L⦄ ⊢ W1 ➡*[h] W2 →
∀T1,T2. ⦃G,L.ⓓW1⦄ ⊢ T1 ➡*[n,h] T2 →
∀V1. ⦃G,L⦄ ⊢ V1 ➡*[h] V →
∀p. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n,h] ⓓ{p}W2.ⓐV2.T2.
⦃G,L⦄ ⊢ T1 ➡*[n1,h] ⓛ{p}W.T & ⦃G,L⦄ ⊢ ⓓ{p}ⓝW.V1.T ➡*[n2,h] X2 &
n1 + n2 = n
| ∃∃n1,n2,p,V0,V2,V,T.
- â¦\83G,Lâ¦\84 â\8a¢ V1 â\9e¡*[h] V0 & â¬\86*[1] V0 ≘ V2 &
+ â¦\83G,Lâ¦\84 â\8a¢ V1 â\9e¡*[h] V0 & â\87§*[1] V0 ≘ V2 &
⦃G,L⦄ ⊢ T1 ➡*[n1,h] ⓓ{p}V.T & ⦃G,L⦄ ⊢ ⓓ{p}V.ⓐV2.T ➡*[n2,h] X2 &
n1 + n2 = n.
#n #h #G #L #V1 #T1 #U2 #H