(* Basic_1: includes: pr2_delta1 *)
definition cpr: lenv → relation term ≝
- λL,T1,T2. ∃∃T. T1 ➡ T & L ⊢ T [0, |L|] ▶* T2.
+ λL,T1,T2. ∃∃T. T1 ➡ T & L ⊢ T ▶* [0, |L|] T2.
interpretation
"context-sensitive parallel reduction (term)"
(* Basic properties *********************************************************)
-lemma cpr_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T [d, e] ▶* T2 → L ⊢ T1 ➡ T2.
+lemma cpr_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡ T2.
/4 width=3/ qed-.
(* Basic_1: was by definition: pr2_free *)
lemma cpr_tpr: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ T1 ➡ T2.
/2 width=3/ qed.
-lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 ➡ T2.
+lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ➡ T2.
/3 width=5/ qed.
lemma cpr_refl: ∀L,T. L ⊢ T ➡ T.
qed.
lemma cpr_cast: ∀L,V,T1,T2.
- L â\8a¢ T1 â\9e¡ T2 â\86\92 L â\8a¢ â\93£V. T1 ➡ T2.
+ L â\8a¢ T1 â\9e¡ T2 â\86\92 L â\8a¢ â\93\9dV. T1 ➡ T2.
#L #V #T1 #T2 * /3 width=3/
qed.
(* Note: it does not hold replacing |L1| with |L2| *)
(* Basic_1: was only: pr2_change *)
-lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
- ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ➡ T2.
+lemma cpr_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
+ ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
-lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 -HL12 /3 width=4/
+lapply (tpss_lsubs_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
qed.
(* Basic inversion lemmas ***************************************************)
(* Basic_1: was pr2_gen_abbr *)
lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 →
- (∃∃V,V2,T2. V1 ➡ V & L ⊢ V [O, |L|] ▶* V2 &
+ (∃∃V,V2,T2. V1 ➡ V & L ⊢ V ▶* [O, |L|] V2 &
L. ⓓV ⊢ T1 ➡ T2 &
U2 = ⓓV2. T2
) ∨
elim (tpr_inv_abbr1 … H1) -H1 *
[ #V #T0 #T #HV1 #HT10 #HT0 #H destruct
elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
- lapply (tps_lsubs_conf … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
+ lapply (tps_lsubs_trans … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
lapply (tps_weak_all … HT0) -HT0 #HT0
- lapply (tpss_lsubs_conf … HT2 (L. ⓓV) ?) -HT2 /2 width=1/ #HT2
+ lapply (tpss_lsubs_trans … HT2 (L. ⓓV) ?) -HT2 /2 width=1/ #HT2
lapply (tpss_weak_all … HT2) -HT2 #HT2
lapply (tpss_strap … HT0 HT2) -T /4 width=7/
| /4 width=5/
qed-.
(* Basic_1: was: pr2_gen_cast *)
-lemma cpr_inv_cast1: â\88\80L,V1,T1,U2. L â\8a¢ â\93£V1. T1 ➡ U2 → (
+lemma cpr_inv_cast1: â\88\80L,V1,T1,U2. L â\8a¢ â\93\9dV1. T1 ➡ U2 → (
∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 &
- U2 = â\93£V2. T2
+ U2 = â\93\9dV2. T2
) ∨ L ⊢ T1 ➡ U2.
#L #V1 #T1 #U2 * #X #H #HU2
elim (tpr_inv_cast1 … H) -H /3 width=3/
elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
qed-.
-(* Basic_1: removed theorems 4:
+(* Basic_1: removed theorems 6:
pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
+ pr2_gen_ctail pr2_ctail
Basic_1: removed local theorems 3:
pr2_free_free pr2_free_delta pr2_delta_delta
*)