include "basic_2/rt_computation/cpxs_lfpx.ma".
include "basic_2/rt_computation/csx_cpxs.ma".
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
-(* Properties with uncounted parallel rt-transition on referred entries *****)
+(* Properties with unbound parallel rt-transition on referred entries *******)
(* Basic_2A1: was just: csx_lpx_conf *)
lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
]
qed.
-fact csx_appl_theta_aux: â\88\80h,o,p,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Uâ¦\84 â\86\92 â\88\80V1,V2. â¬\86*[1] V1 â\89¡ V2 →
+fact csx_appl_theta_aux: â\88\80h,o,p,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Uâ¦\84 â\86\92 â\88\80V1,V2. â¬\86*[1] V1 â\89\98 V2 →
∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
#h #o #p #G #L #X #H @(csx_ind_cpxs … H) -X
#X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
qed-.
lemma csx_appl_theta: ∀h,o,p,G,L,V,V2,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.ⓐV2.T⦄ →
- â\88\80V1. â¬\86*[1] V1 â\89¡ V2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
+ â\88\80V1. â¬\86*[1] V1 â\89\98 V2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
/2 width=5 by csx_appl_theta_aux/ qed.