(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
definition lcpr: relation lenv ≝
- λL1,L2. â\88\83â\88\83L. L1 â\87\92 L & L [0, |L|] â\89«* L2
+ λL1,L2. â\88\83â\88\83L. L1 â\9e¡ L & L [0, |L|] â\96¶* L2
.
interpretation
(* Basic properties *********************************************************)
-lemma lcpr_refl: â\88\80L. L â\8a¢ â\87\92 L.
+lemma lcpr_refl: â\88\80L. L â\8a¢ â\9e¡ L.
/2 width=3/ qed.
(* Basic inversion lemmas ***************************************************)
-lemma lcpr_inv_atom1: â\88\80L2. â\8b\86 â\8a¢ â\87\92 L2 → L2 = ⋆.
+lemma lcpr_inv_atom1: â\88\80L2. â\8b\86 â\8a¢ â\9e¡ L2 → L2 = ⋆.
#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 //
qed-.