(* Properties on context-sensitive parallel computation for terms ***********)
-lemma lprs_cpr_trans: ∀G. s_r_transitive … (cpr G) (λ_. lprs G).
-/3 width=5 by s_r_trans_LTC2, lpr_cprs_trans/ qed-.
+lemma lprs_cpr_trans: ∀G. c_r_transitive … (cpr G) (λ_. lprs G).
+/3 width=5 by c_r_trans_LTC2, lpr_cprs_trans/ qed-.
(* Basic_1: was just: pr3_pr3_pr3_t *)
(* Note: alternative proof /3 width=5 by s_r_trans_LTC1, lprs_cpr_trans/ *)
-lemma lprs_cprs_trans: ∀G. s_rs_transitive … (cpr G) (λ_. lprs G).
-#G @s_r_to_s_rs_trans @s_r_trans_LTC2
-@s_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *)
+lemma lprs_cprs_trans: ∀G. c_rs_transitive … (cpr G) (λ_. lprs G).
+#G @c_r_to_c_rs_trans @c_r_trans_LTC2
+@c_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *)
qed-.
lemma lprs_cprs_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 &
U2 = ⓓ{a}V2.T2
) ∨
- â\88\83â\88\83T2. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡* T2 & â\87§[0, 1] U2 ≡ T2 & a = true.
+ â\88\83â\88\83T2. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡* T2 & â¬\86[0, 1] U2 ≡ T2 & a = true.
#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
#U0 #U2 #_ #HU02 * *
[ #V0 #T0 #HV10 #HT10 #H destruct
]
| #U1 #HTU1 #HU01 elim (lift_total U2 0 1)
#U #HU2 lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0
- /4 width=3 by cprs_strap1, ldrop_drop, ex3_intro, or_intror/
+ /4 width=3 by cprs_strap1, drop_drop, ex3_intro, or_intror/
]
qed-.