(* *)
(**************************************************************************)
-include "basic_2/syntax/cext2.ma".
+include "static_2/syntax/cext2.ma".
include "basic_2/rt_computation/cpms.ma".
(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR BINDERS *********************)
-definition cprs_ext (h) (G): relation3 lenv bind bind ≝
- cext2 (λL. cpms h G L 0).
+definition cprs_ext (h) (n) (G): relation3 lenv bind bind ≝
+ cext2 (λL. cpms h G L n).
interpretation
"context-sensitive parallel r-computation (binder)"
- 'PRedStar h G L I1 I2 = (cprs_ext h G L I1 I2).
+ 'PRedStar h n G L I1 I2 = (cprs_ext h n G L I1 I2).