(* Basic_2A1: uses: lsx_cpx_trans_lcosx *)
lemma rsx_cpx_trans_jsx (h) (G):
- â\88\80L0,T1,T2. â¦\83G,L0â¦\84 ⊢ T1 ⬈[h] T2 →
- â\88\80L. G â\8a¢ L0 â\8a\92[h] L â\86\92 G â\8a¢ â¬\88*[h,T1] ð\9d\90\92â¦\83Lâ¦\84 â\86\92 G â\8a¢ â¬\88*[h,T2] ð\9d\90\92â¦\83Lâ¦\84.
+ â\88\80L0,T1,T2. â\9dªG,L0â\9d« ⊢ T1 ⬈[h] T2 →
+ â\88\80L. G â\8a¢ L0 â\8a\92[h] L â\86\92 G â\8a¢ â¬\88*[h,T1] ð\9d\90\92â\9dªLâ\9d« â\86\92 G â\8a¢ â¬\88*[h,T2] ð\9d\90\92â\9dªLâ\9d«.
#h #G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2
[ //
| //
(* Basic_2A1: uses: lsx_cpx_trans_O *)
lemma rsx_cpx_trans (h) (G):
- â\88\80L,T1,T2. â¦\83G,Lâ¦\84 ⊢ T1 ⬈[h] T2 →
- G â\8a¢ â¬\88*[h,T1] ð\9d\90\92â¦\83Lâ¦\84 â\86\92 G â\8a¢ â¬\88*[h,T2] ð\9d\90\92â¦\83Lâ¦\84.
+ â\88\80L,T1,T2. â\9dªG,Lâ\9d« ⊢ T1 ⬈[h] T2 →
+ G â\8a¢ â¬\88*[h,T1] ð\9d\90\92â\9dªLâ\9d« â\86\92 G â\8a¢ â¬\88*[h,T2] ð\9d\90\92â\9dªLâ\9d«.
/3 width=6 by rsx_cpx_trans_jsx, jsx_refl/ qed-.
lemma rsx_cpxs_trans (h) (G):
- â\88\80L,T1,T2. â¦\83G,Lâ¦\84 ⊢ T1 ⬈*[h] T2 →
- G â\8a¢ â¬\88*[h,T1] ð\9d\90\92â¦\83Lâ¦\84 â\86\92 G â\8a¢ â¬\88*[h,T2] ð\9d\90\92â¦\83Lâ¦\84.
+ â\88\80L,T1,T2. â\9dªG,Lâ\9d« ⊢ T1 ⬈*[h] T2 →
+ G â\8a¢ â¬\88*[h,T1] ð\9d\90\92â\9dªLâ\9d« â\86\92 G â\8a¢ â¬\88*[h,T2] ð\9d\90\92â\9dªLâ\9d«.
#h #G #L #T1 #T2 #H
@(cpxs_ind_dx ???????? H) -T1 //
/3 width=3 by rsx_cpx_trans/