include "basic_2/i_static/tc_lfxs.ma".
include "basic_2/rt_transition/lfpx.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******)
definition lfpxs: ∀h. relation4 genv term lenv lenv ≝
λh,G. tc_lfxs (cpx h G).
interpretation
- "uncounted parallel rt-computation on referred entries (local environment)"
+ "unbound parallel rt-computation on referred entries (local environment)"
'PRedTySnStar h T G L1 L2 = (lfpxs h G T L1 L2).
(* Basic properties *********************************************************)
lemma lfpx_lfpxs: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
/2 width=1 by inj/ qed.
-(* Basic_2A1: was just: lpxs_strap1 *)
lemma lfpxs_step_dx: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
/2 width=3 by tc_lfxs_step_dx/ qed.
-(* Basic_2A1: was just: lpxs_strap2 *)
lemma lfpxs_step_sn: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
/2 width=3 by tc_lfxs_step_sn/ qed.