(* *)
(**************************************************************************)
-include "basic_2/computation/csx_lpx.ma".
-include "basic_2/computation/lpxs.ma".
+include "basic_2/rt_computation/csx_lpx.ma".
+include "basic_2/rt_computation/lpxs_lpx.ma".
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-(* Properties on sn extended parallel computation for local environments ****)
+(* Properties with unbound parallel rt-computation on all entries ***********)
-lemma csx_lpxs_conf: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 →
- ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, o] T → ⦃G, L2⦄ ⊢ ⬊*[h, o] T.
-#h #o #G #L1 #L2 #H @(lpxs_ind … H) -L2 /3 by lpxs_strap1, csx_lpx_conf/
+lemma csx_lpxs_conf: ∀h,G,L1,L2,T. ⦃G,L1⦄ ⊢ ⬈*[h] L2 →
+ ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+#h #G #L1 #L2 #T #H @(lpxs_ind_dx … H) -L2
+/3 by lpxs_step_dx, csx_lpx_conf/
qed-.