--- /dev/null
+(* Note: this is the companion of lfxs_trans_fsle *)
+theorem lfxs_trans_fsge: ∀R,R1,R2,R3.
+ lfxs_transitive_next R1 R R3 →
+ ∀L1,L,T. L1 ⪤*[R1, T] L →
+ ∀L2. L ⪤[R2] L2 → L1 ⪤*[R3, T] L2.
+#R #R1 #R2 #R3 #HR #L1 #L #T #H
+cases H -H #f1 #Hf1 #HL1 #L2 * #f #Hf #HL2
+@(ex2_intro … Hf1) -Hf1
+@(lexs_trans_gen … HL1) -HL1
+[5: @(sle_lexs_conf … HL2) -HL2 /2 width=1 by sle_isid_sn/ |1,2: skip
+|4: //
+|3:
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/lfdeq_lfeq.ma".
+include "basic_2/rt_transition/lfpx_lpx.ma".
+include "basic_2/rt_computation/lfsx_lfsx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+
+(* Properties with uncounted rt-transition **********************************)
+
+lemma lfsx_intro_lpx: ∀h,o,G,L1,T.
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
+ G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
+#h #o #G #L1 #T #HT
+@lfsx_intro #L2 #H
+elim (lfpx_inv_lpx_lfeq … H) -H
+/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfeq_lfdeq/
+qed-.
+
+lemma lfsx_lpx_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
+/3 width=3 by lfsx_lfpx_trans, lfpx_lpx/ qed-.
+
+(* Eliminators with uncounted rt-transition *********************************)
+
+lemma lfsx_ind_lpx: ∀h,o,G,T. ∀R:predicate lenv.
+ (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
+ R L1
+ ) →
+ ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
+/5 width=6 by lfsx_ind, lfpx_lpx/ qed-.
lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lpxs.ma lfpxs_lfpxs.ma
csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma
csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma
-lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_lfsx.ma
+lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_lfsx.ma
lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/lfxs_lex.ma".
+include "basic_2/rt_transition/lfpx_fsle.ma".
+include "basic_2/rt_transition/lpx.ma".
+
+(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+
+(* Properties with uncounted parallel rt-transition for local environments **)
+
+lemma lfpx_lpx: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2.
+/2 width=1 by lfxs_lex/ qed.
+
+(* Inversion lemmas with uncounted parallel rt-transition for local envs ****)
+
+lemma lfpx_inv_lpx_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 →
+ ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h] L & L ≡[T] L2.
+/3 width=3 by lfpx_fsge_comp, lfxs_inv_lex_lfeq/ qed-.
(**************************************************************************)
include "basic_2/relocation/lex.ma".
-include "basic_2/static/lfxs_fqup.ma".
+include "basic_2/static/lfxs_fsle.ma".
+include "basic_2/static/lfeq.ma".
(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
elim (frees_total L1 T) #g #Hg
/4 width=5 by lexs_sdj, sdj_isid_sn, ex2_intro/
qed.
+
+(* Inversion lemmas with generic extension of a context sensitive relation **)
+
+lemma lfxs_inv_lex_lfeq: ∀R. c_reflexive … R →
+ lfxs_fsge_compatible R →
+ ∀L1,L2,T. L1 ⪤*[R, T] L2 →
+ ∃∃L. L1 ⪤[R] L & L ≡[T] L2.
+#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
+elim (lexs_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL
+[ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R
+lapply (lexs_sdj … HL10 f1 ?) /2 width=1 by sdj_isid_sn/ #H
+elim (frees_lexs_conf … Hf1 … H) // -H2R -H #f0 #Hf0 #Hf01
+/4 width=7 by sle_lexs_trans, (* 2x *) ex2_intro/
+qed-.
*)
[ { "uncounted context-sensitive parallel rt-computation" * } {
[ [ "refinement for lenvs" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
- [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
+ [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
[ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
[ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
[ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
]
[ { "uncounted context-sensitive parallel rt-transition" * } {
[ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
- [ [ "for lenvs on referred entries" ] "lfpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ]
+ [ [ "for lenvs on referred entries" ] "lfpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lpx" + "lfpx_lfpx" * ]
[ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ]
[ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
[ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" * ]
projects / helm.git / commitdiff