]
qed-.
-(* Basic_2A1: includes: lpx_sn_trans *)
theorem lexs_trans (RN) (RP) (f): (∀g,I,K. lexs_transitive RN RN RN RN RP g K I) →
(∀g,I,K. lexs_transitive RP RP RP RN RP g K I) →
Transitive … (lexs RN RP f).
/2 width=9 by lexs_trans_gen/ qed-.
theorem lexs_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤*[R1, cfull, f] L → 𝐈⦃f⦄ →
- ∀L2. L ⪤*[R2, cfull, f] L2 → L1 ⪤*[R3, cfull, f] L2.
+ ∀L2. L ⪤*[R2, cfull, f] L2 → L1 ⪤*[R3, cfull, f] L2.
#R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f
[ #f #Hf #L2 #H >(lexs_inv_atom1 … H) -L2 // ]
#f #I1 #I #K1 #K #HK1 #_ #IH #Hf #L2 #H
/3 width=1 by lexs_push/
qed-.
-(* Basic_2A1: includes: lpx_sn_conf *)
theorem lexs_conf (RN1) (RP1) (RN2) (RP2):
∀L,f.
(∀g,I,K,n. ⬇*[n] L ≘ K.ⓘ{I} → ↑g = ⫱*[n] f → R_pw_confluent2_lexs RN1 RN2 RN1 RP1 RN2 RP2 g K I) →