qed.
theorem cprs_theta_rc: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡ V â\86\92 â\87§[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡ V â\86\92 â¬\86[0, 1] V ≡ 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.
- â\87§[0, 1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
+ â¬\86[0, 1] V ≡ 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 & â\87§[0,1] V0 ≡ V2 &
+ | â\88\83â\88\83a,V0,V2,V,T. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡* V0 & â¬\86[0,1] V0 ≡ 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 just: pr3_pr2_pr2_t *)
(* Basic_1: includes: pr3_pr0_pr2_t *)
-lemma lpr_cpr_trans: ∀G. s_r_transitive … (cpr G) (λ_. lpr G).
+lemma lpr_cpr_trans: ∀G. c_r_transitive … (cpr G) (λ_. lpr G).
#G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
[ /2 width=3 by/
| #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
(* Advanced properties ******************************************************)
(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
-lemma lpr_cprs_trans: ∀G. s_rs_transitive … (cpr G) (λ_. lpr G).
-#G @s_r_trans_LTC1 /2 width=3 by lpr_cpr_trans/ (**) (* full auto fails *)
+lemma lpr_cprs_trans: ∀G. c_rs_transitive … (cpr G) (λ_. lpr G).
+#G @c_r_trans_LTC1 /2 width=3 by lpr_cpr_trans/ (**) (* full auto fails *)
qed-.
(* Basic_1: was: pr3_strip *)