include "basic_2/relocation/lex.ma".
include "basic_2/rt_computation/cpxs_ext.ma".
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************)
definition lpxs: ∀h. relation3 genv lenv lenv ≝
λh,G. lex (cpxs h G).
interpretation
- "uncounted parallel rt-computation (local environment)"
+ "unbound parallel rt-computation (local environment)"
'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2).
+(* Basic properties *********************************************************)
+
+lemma lpxs_refl: ∀h,G. reflexive … (lpxs h G).
+/2 width=1 by lex_refl/ qed.
+
(* Basic inversion lemmas ***************************************************)
lemma lpxs_inv_bind_sn: ∀h,G,I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 →