(**************************************************************************)
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)"
(* Basic eliminators ********************************************************)
lemma csx_ind: ∀h,G,L. ∀Q:predicate term.
- (â\88\80T1. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T1â¦\84 →
- (â\88\80T2. â¦\83G,Lâ¦\84 ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) →
+ (â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªT1â\9d« →
+ (â\88\80T2. â\9dªG,Lâ\9d« ⊢ T1 ⬈[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) →
Q T1
) →
- â\88\80T. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84 → Q T.
+ â\88\80T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d« → Q T.
#h #G #L #Q #H0 #T1 #H elim H -T1
/5 width=1 by SN_intro/
qed-.
(* Basic_1: was just: sn3_pr2_intro *)
lemma csx_intro: ∀h,G,L,T1.
- (â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b T2 â\86\92 â\8a¥) â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T2â¦\84) →
- â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83T1â¦\84.
+ (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b T2 â\86\92 â\8a¥) â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªT2â\9d«) →
+ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªT1â\9d«.
/4 width=1 by SN_intro/ qed.
(* Basic forward lemmas *****************************************************)
-fact csx_fwd_pair_sn_aux: â\88\80h,G,L,U. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Uâ¦\84 →
- ∀I,V,T. U = ②{I}V.T → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
+fact csx_fwd_pair_sn_aux: â\88\80h,G,L,U. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªUâ\9d« →
+ ∀I,V,T. U = ②[I]V.T → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫.
#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/
+@(IH (②[I]V2.T)) -IH /2 width=3 by cpx_pair_sn/ -HLV2
+#H elim (teqx_inv_pair … H) -H /2 width=1 by/
qed-.
(* Basic_1: was just: sn3_gen_head *)
-lemma csx_fwd_pair_sn: â\88\80h,I,G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\91¡{I}V.Tâ¦\84 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Vâ¦\84.
+lemma csx_fwd_pair_sn: â\88\80h,I,G,L,V,T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\91¡[I]V.Tâ\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªVâ\9d«.
/2 width=5 by csx_fwd_pair_sn_aux/ qed-.
-fact csx_fwd_bind_dx_aux: â\88\80h,G,L,U. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Uâ¦\84 →
- ∀p,I,V,T. U = ⓑ{p,I}V.T → ⦃G,L.ⓑ{I}V⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+fact csx_fwd_bind_dx_aux: â\88\80h,G,L,U. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªUâ\9d« →
+ ∀p,I,V,T. U = ⓑ[p,I]V.T → ❪G,L.ⓑ[I]V❫ ⊢ ⬈*[h] 𝐒❪T❫.
#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/
+@(IH (ⓑ[p, I]V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2
+#H elim (teqx_inv_pair … H) -H /2 width=1 by/
qed-.
(* Basic_1: was just: sn3_gen_bind *)
-lemma csx_fwd_bind_dx: â\88\80h,p,I,G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\93\91{p,I}V.Tâ¦\84 â\86\92 â¦\83G,L.â\93\91{I}Vâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84.
+lemma csx_fwd_bind_dx: â\88\80h,p,I,G,L,V,T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\93\91[p,I]V.Tâ\9d« â\86\92 â\9dªG,L.â\93\91[I]Vâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d«.
/2 width=4 by csx_fwd_bind_dx_aux/ qed-.
-fact csx_fwd_flat_dx_aux: â\88\80h,G,L,U. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Uâ¦\84 →
- ∀I,V,T. U = ⓕ{I}V.T → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+fact csx_fwd_flat_dx_aux: â\88\80h,G,L,U. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªUâ\9d« →
+ ∀I,V,T. U = ⓕ[I]V.T → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫.
#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/
+@(IH (ⓕ[I]V.T2)) -IH /2 width=3 by cpx_flat/ -HLT2
+#H elim (teqx_inv_pair … H) -H /2 width=1 by/
qed-.
(* Basic_1: was just: sn3_gen_flat *)
-lemma csx_fwd_flat_dx: â\88\80h,I,G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\93\95{I}V.Tâ¦\84 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84.
+lemma csx_fwd_flat_dx: â\88\80h,I,G,L,V,T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\93\95[I]V.Tâ\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d«.
/2 width=5 by csx_fwd_flat_dx_aux/ qed-.
-lemma csx_fwd_bind: â\88\80h,p,I,G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\93\91{p,I}V.Tâ¦\84 →
- â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Vâ¦\84 â\88§ â¦\83G,L.â\93\91{I}Vâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84.
+lemma csx_fwd_bind: â\88\80h,p,I,G,L,V,T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\93\91[p,I]V.Tâ\9d« →
+ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªVâ\9d« â\88§ â\9dªG,L.â\93\91[I]Vâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d«.
/3 width=3 by csx_fwd_pair_sn, csx_fwd_bind_dx, conj/ qed-.
-lemma csx_fwd_flat: â\88\80h,I,G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\93\95{I}V.Tâ¦\84 →
- â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Vâ¦\84 â\88§ â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Tâ¦\84.
+lemma csx_fwd_flat: â\88\80h,I,G,L,V,T. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\93\95[I]V.Tâ\9d« →
+ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªVâ\9d« â\88§ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d«.
/3 width=3 by csx_fwd_pair_sn, csx_fwd_flat_dx, conj/ qed-.
(* Basic_1: removed theorems 14:
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
*)