(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
definition cpe: lenv → relation term ≝
- λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍[T2].
+ λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍⦃T2⦄.
interpretation "context-sensitive parallel evaluation (term)"
'PEval L T1 T2 = (cpe L T1 T2).
(* Basic_properties *********************************************************)
(* Basic_1: was: nf2_sn3 *)
-lemma cpe_csn: â\88\80L,T1. L â\8a¢ â¬\87* T1 â\86\92 â\88\83T2. L â\8a¢ T1 â\9e¡* ð\9d\90\8d[T2].
+lemma cpe_csn: â\88\80L,T1. L â\8a¢ â¬\8a* T1 â\86\92 â\88\83T2. L â\8a¢ T1 â\9e¡* ð\9d\90\8dâ¦\83T2â¦\84.
#L #T1 #H @(csn_ind … H) -T1
#T1 #_ #IHT1
elim (cnf_dec L T1) /3 width=3/