qed.
theorem cprs_theta_rc: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡ V â\86\92 â¬\86[0, 1] V â\89¡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡ V â\86\92 â¬\86[0, 1] V â\89\98 V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H @(cprs_ind … H) -W2
/3 width=5 by cprs_trans, cprs_theta_dx, cprs_bind_dx/
qed.
theorem cprs_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
- â¬\86[0, 1] V â\89¡ V2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
+ â¬\86[0, 1] V â\89\98 V2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ V1 ➡* V → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(cprs_ind_dx … H) -V1
/3 width=3 by cprs_trans, cprs_theta_rc, cprs_flat_dx/
U2 = ⓐV2. T2
| ∃∃a,W,T. ⦃G, L⦄ ⊢ T1 ➡* ⓛ{a}W.T &
⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V1.T ➡* U2
- | â\88\83â\88\83a,V0,V2,V,T. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡* V0 & â¬\86[0,1] V0 â\89¡ V2 &
+ | â\88\83â\88\83a,V0,V2,V,T. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡* V0 & â¬\86[0,1] V0 â\89\98 V2 &
⦃G, L⦄ ⊢ T1 ➡* ⓓ{a}V.T &
⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡* U2.
#G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/
(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
lemma lpr_cprs_trans: ∀G. b_rs_transitive … (cpr G) (λ_. lpr G).
-#G @b_c_trans_LTC1 /2 width=3 by lpr_cpr_trans/ (**) (* full auto fails *)
+#G @b_c_trans_CTC1 /2 width=3 by lpr_cpr_trans/ (**) (* full auto fails *)
qed-.
(* Basic_1: was: pr3_strip *)