(* *)
(**************************************************************************)
+include "ground_2/xoa/ex_4_5.ma".
include "basic_2/rt_transition/cpx_lsubr.ma".
include "basic_2/rt_computation/cpxs.ma".
qed.
theorem cpxs_theta_rc: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2.
- â¦\83G,Lâ¦\84 â\8a¢ V1 â¬\88[h] V â\86\92 â¬\86*[1] V ≘ V2 →
+ â¦\83G,Lâ¦\84 â\8a¢ V1 â¬\88[h] V â\86\92 â\87§*[1] V ≘ V2 →
⦃G,L.ⓓW1⦄ ⊢ T1 ⬈*[h] T2 → ⦃G,L⦄ ⊢ W1 ⬈*[h] W2 →
⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ⬈*[h] ⓓ{p}W2.ⓐV2.T2.
#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H @(cpxs_ind … H) -W2
qed.
theorem cpxs_theta: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2.
- â¬\86*[1] V ≘ V2 → ⦃G,L⦄ ⊢ W1 ⬈*[h] W2 →
+ â\87§*[1] V ≘ V2 → ⦃G,L⦄ ⊢ W1 ⬈*[h] W2 →
⦃G,L.ⓓW1⦄ ⊢ T1 ⬈*[h] T2 → ⦃G,L⦄ ⊢ V1 ⬈*[h] V →
⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ⬈*[h] ⓓ{p}W2.ⓐV2.T2.
#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1
∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 &
U2 = ⓐV2.T2
| ∃∃p,W,T. ⦃G,L⦄ ⊢ T1 ⬈*[h] ⓛ{p}W.T & ⦃G,L⦄ ⊢ ⓓ{p}ⓝW.V1.T ⬈*[h] U2
- | â\88\83â\88\83p,V0,V2,V,T. â¦\83G,Lâ¦\84 â\8a¢ V1 â¬\88*[h] V0 & â¬\86*[1] V0 ≘ V2 &
+ | â\88\83â\88\83p,V0,V2,V,T. â¦\83G,Lâ¦\84 â\8a¢ V1 â¬\88*[h] V0 & â\87§*[1] V0 ≘ V2 &
⦃G,L⦄ ⊢ T1 ⬈*[h] ⓓ{p}V.T & ⦃G,L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] U2.
#h #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5 by or3_intro0, ex3_2_intro/ ]
#U #U2 #_ #HU2 * *