include "basic_2/rt_computation/csx_drops.ma".
(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Advanced properties ******************************************************)
include "basic_2/rt_computation/csx_drops.ma".
(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
(* Advanced properties ******************************************************)
∀L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
∀T2. T1 ≛ T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #G #L #T1 #H @(csx_ind … H) -T1 #T #_ #IH #T2 #HT2
∀L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
∀T2. T1 ≛ T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #G #L #T1 #H @(csx_ind … H) -T1 #T #_ #IH #T2 #HT2
qed-.
lemma csx_cpx_trans (h) (G):
∀L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
∀T2. ⦃G,L⦄ ⊢ T1 ⬈[h] T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12
qed-.
lemma csx_cpx_trans (h) (G):
∀L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
∀T2. ⦃G,L⦄ ⊢ T1 ⬈[h] T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12
[ -W -T #H elim H -H //
| -HW -IHT /3 width=3 by csx_cpx_trans/
| -HW -HT -IHW /4 width=3 by csx_cpx_trans, cpx_pair_sn/
[ -W -T #H elim H -H //
| -HW -IHT /3 width=3 by csx_cpx_trans/
| -HW -HT -IHW /4 width=3 by csx_cpx_trans, cpx_pair_sn/