-include "basic_2/rt_computation/cpxs_toeq_vector.ma".
-include "basic_2/rt_computation/csx_simple_toeq.ma".
+include "basic_2/rt_computation/cpxs_teqo_vector.ma".
+include "basic_2/rt_computation/csx_simple_teqo.ma".
include "basic_2/rt_computation/csx_cnx.ma".
include "basic_2/rt_computation/csx_cpxs.ma".
include "basic_2/rt_computation/csx_vector.ma".
include "basic_2/rt_computation/csx_cnx.ma".
include "basic_2/rt_computation/csx_cpxs.ma".
include "basic_2/rt_computation/csx_vector.ma".
- â\88\80T. ð\9d\90\92â¦\83Tâ¦\84 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88[h] ð\9d\90\8dâ¦\83Tâ¦\84 →
- â\88\80Vs. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Vsâ¦\84 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\92¶Vs.Tâ¦\84.
+ â\88\80T. ð\9d\90\92â\9dªTâ\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88[h] ð\9d\90\8dâ\9dªTâ\9d« →
+ â\88\80Vs. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªVsâ\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\92¶Vs.Tâ\9d«.
#h #G #L #T #H1T #H2T #Vs elim Vs -Vs
[ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/
| #V #Vs #IHV #H
elim (csxv_inv_cons … H) -H #HV #HVs
#h #G #L #T #H1T #H2T #Vs elim Vs -Vs
[ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/
| #V #Vs #IHV #H
elim (csxv_inv_cons … H) -H #HV #HVs
- â\88\80s,Vs. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Vsâ¦\84 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\92¶Vs.â\8b\86sâ¦\84.
+ â\88\80s,Vs. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªVsâ\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\92¶Vs.â\8b\86sâ\9d«.