(* 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).