(**************************************************************************)
include "basic_2/notation/relations/predtystrong_4.ma".
-include "static_2/syntax/tdeq.ma".
+include "static_2/syntax/teqx.ma".
include "basic_2/rt_transition/cpx.ma".
(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
definition csx: ∀h. relation3 genv lenv term ≝
- λh,G,L. SN … (cpx h G L) tdeq.
+ λh,G,L. SN … (cpx h G L) teqx.
interpretation
"strong normalization for unbound context-sensitive parallel rt-transition (term)"
#h #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csx_intro #V2 #HLV2 #HV2
@(IH (②{I}V2.T)) -IH /2 width=3 by cpx_pair_sn/ -HLV2
-#H elim (tdeq_inv_pair … H) -H /2 width=1 by/
+#H elim (teqx_inv_pair … H) -H /2 width=1 by/
qed-.
(* Basic_1: was just: sn3_gen_head *)
#h #G #L #U #H elim H -H #U0 #_ #IH #p #I #V #T #H destruct
@csx_intro #T2 #HLT2 #HT2
@(IH (ⓑ{p, I}V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2
-#H elim (tdeq_inv_pair … H) -H /2 width=1 by/
+#H elim (teqx_inv_pair … H) -H /2 width=1 by/
qed-.
(* Basic_1: was just: sn3_gen_bind *)
#h #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csx_intro #T2 #HLT2 #HT2
@(IH (ⓕ{I}V.T2)) -IH /2 width=3 by cpx_flat/ -HLT2
-#H elim (tdeq_inv_pair … H) -H /2 width=1 by/
+#H elim (teqx_inv_pair … H) -H /2 width=1 by/
qed-.
(* Basic_1: was just: sn3_gen_flat *)
sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind
*)
(* Basic_2A1: removed theorems 6:
- csxa_ind csxa_intro csxa_cpxs_trans csxa_intro_cpx
+ csxa_ind csxa_intro csxa_cpxs_trans csxa_intro_cpx
csx_csxa csxa_csx
*)