(**************************************************************************)
include "basic_2/notation/relations/lsubeqx_6.ma".
-include "basic_2/rt_computation/lfsx.ma".
+include "basic_2/rt_computation/rdsx.ma".
-(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNBOUND RT-TRANSITION **********)
-(* Note: this should be an instance of a more general lexs *)
+(* Note: this should be an instance of a more general sex *)
(* Basic_2A1: uses: lcosx *)
inductive lsubsx (h) (o) (G): rtmap → relation lenv ≝
| lsubsx_atom: ∀f. lsubsx h o G f (⋆) (⋆)
| lsubsx_push: ∀f,I,K1,K2. lsubsx h o G f K1 K2 →
- lsubsx h o G (â\86\91f) (K1.ⓘ{I}) (K2.ⓘ{I})
+ lsubsx h o G (⫯f) (K1.ⓘ{I}) (K2.ⓘ{I})
| lsubsx_unit: ∀f,I,K1,K2. lsubsx h o G f K1 K2 →
- lsubsx h o G (⫯f) (K1.ⓤ{I}) (K2.ⓧ)
+ lsubsx h o G (â\86\91f) (K1.ⓤ{I}) (K2.ⓧ)
| lsubsx_pair: ∀f,I,K1,K2,V. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ →
- lsubsx h o G f K1 K2 â\86\92 lsubsx h o G (⫯f) (K1.ⓑ{I}V) (K2.ⓧ)
+ lsubsx h o G f K1 K2 â\86\92 lsubsx h o G (â\86\91f) (K1.ⓑ{I}V) (K2.ⓧ)
.
interpretation
/2 width=7 by lsubsx_inv_atom_sn_aux/ qed-.
fact lsubsx_inv_push_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
- â\88\80f,I,K1. g = â\86\91f → L1 = K1.ⓘ{I} →
+ â\88\80f,I,K1. g = ⫯f → L1 = K1.ⓘ{I} →
∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓘ{I}.
#h #o #g #G #L1 #L2 * -g -L1 -L2
[ #f #g #J #L1 #_ #H destruct
]
qed-.
-lemma lsubsx_inv_push_sn: â\88\80h,o,f,I,G,K1,L2. G â\8a¢ K1.â\93\98{I} â\8a\86â\93§[h, o, â\86\91f] L2 →
+lemma lsubsx_inv_push_sn: â\88\80h,o,f,I,G,K1,L2. G â\8a¢ K1.â\93\98{I} â\8a\86â\93§[h, o, ⫯f] L2 →
∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓘ{I}.
/2 width=5 by lsubsx_inv_push_sn_aux/ qed-.
fact lsubsx_inv_unit_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
- â\88\80f,I,K1. g = ⫯f → L1 = K1.ⓤ{I} →
+ â\88\80f,I,K1. g = â\86\91f → L1 = K1.ⓤ{I} →
∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
#h #o #g #G #L1 #L2 * -g -L1 -L2
[ #f #g #J #L1 #_ #H destruct
]
qed-.
-lemma lsubsx_inv_unit_sn: â\88\80h,o,f,I,G,K1,L2. G â\8a¢ K1.â\93¤{I} â\8a\86â\93§[h, o, ⫯f] L2 →
+lemma lsubsx_inv_unit_sn: â\88\80h,o,f,I,G,K1,L2. G â\8a¢ K1.â\93¤{I} â\8a\86â\93§[h, o, â\86\91f] L2 →
∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
/2 width=6 by lsubsx_inv_unit_sn_aux/ qed-.
fact lsubsx_inv_pair_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
- â\88\80f,I,K1,V. g = ⫯f → L1 = K1.ⓑ{I}V →
+ â\88\80f,I,K1,V. g = â\86\91f → L1 = K1.ⓑ{I}V →
∃∃K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ &
G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
#h #o #g #G #L1 #L2 * -g -L1 -L2
qed-.
(* Basic_2A1: uses: lcosx_inv_pair *)
-lemma lsubsx_inv_pair_sn: â\88\80h,o,f,I,G,K1,L2,V. G â\8a¢ K1.â\93\91{I}V â\8a\86â\93§[h, o, ⫯f] L2 →
+lemma lsubsx_inv_pair_sn: â\88\80h,o,f,I,G,K1,L2,V. G â\8a¢ K1.â\93\91{I}V â\8a\86â\93§[h, o, â\86\91f] L2 →
∃∃K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ &
G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
/2 width=6 by lsubsx_inv_pair_sn_aux/ qed-.
(* Advanced inversion lemmas ************************************************)
lemma lsubsx_inv_pair_sn_gen: ∀h,o,g,I,G,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊆ⓧ[h, o, g] L2 →
- â\88¨â\88¨ â\88\83â\88\83f,K2. G â\8a¢ K1 â\8a\86â\93§[h, o, f] K2 & g = â\86\91f & L2 = K2.ⓑ{I}V
+ â\88¨â\88¨ â\88\83â\88\83f,K2. G â\8a¢ K1 â\8a\86â\93§[h, o, f] K2 & g = ⫯f & L2 = K2.ⓑ{I}V
| ∃∃f,K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ &
- G â\8a¢ K1 â\8a\86â\93§[h, o, f] K2 & g = ⫯f & L2 = K2.ⓧ.
+ G â\8a¢ K1 â\8a\86â\93§[h, o, f] K2 & g = â\86\91f & L2 = K2.ⓧ.
#h #o #g #I #G #K1 #L2 #V #H
elim (pn_split g) * #f #Hf destruct
[ elim (lsubsx_inv_push_sn … H) -H /3 width=5 by ex3_2_intro, or_introl/