include "basic_2/notation/relations/predtystar_5.ma".
include "basic_2/rt_transition/cpx.ma".
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
definition cpxs: sh → relation4 genv lenv term term ≝
λh,G. CTC … (cpx h G).
-interpretation "uncounted context-sensitive parallel rt-computation (term)"
+interpretation "unbound context-sensitive parallel rt-computation (term)"
'PRedTyStar h G L T1 T2 = (cpxs h G L T1 T2).
(* Basic eliminators ********************************************************)
#h #G #L #X2 #s #H @(cpxs_ind … H) -X2 /2 width=2 by ex_intro/
#X #X2 #_ #HX2 * #n #H destruct
elim (cpx_inv_sort1 … HX2) -HX2 #H destruct /2 width=2 by ex_intro/
-@(ex_intro â\80¦ (⫯n)) >iter_S //
+@(ex_intro â\80¦ (â\86\91n)) >iter_S //
qed-.
lemma cpxs_inv_cast1: ∀h,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ⬈*[h] U2 →