]
qed-.
+lemma lex_ltc_step_dx: ∀R. c_reflexive … R → s_rs_transitive … R (λ_. lex R) →
+ ∀L1,L. lex (LTC … R) L1 L →
+ ∀L2. lex R L L2 → lex (LTC … R) L1 L2.
+/4 width=3 by lex_ltc, lex_inv_ltc, step/ qed-.
+
+lemma lex_ltc_step_sn: ∀R. c_reflexive … R → s_rs_transitive … R (λ_. lex R) →
+ ∀L1,L. lex R L1 L →
+ ∀L2. lex (LTC … R) L L2 → lex (LTC … R) L1 L2.
+/4 width=3 by lex_ltc, lex_inv_ltc, TC_strap/ qed-.
lemma lfpx_lfpxs: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
/2 width=1 by inj/ qed.
-(* Basic_2A1: was just: lpxs_strap1 *)
lemma lfpxs_step_dx: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
/2 width=3 by tc_lfxs_step_dx/ qed.
-(* Basic_2A1: was just: lpxs_strap2 *)
lemma lfpxs_step_sn: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
/2 width=3 by tc_lfxs_step_sn/ qed.
∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ⬈*[h, T] L.ⓑ{I}V2.
/2 width=1 by tc_lfxs_pair_refl/ qed.
-(* Basic_2A1: uses: lpxs_cpx_trans *)
lemma lfpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpxs h G).
#h #G @s_r_trans_LTC2 @lfpx_cpxs_trans (**) (* auto fails *)
qed-.
(* Note: lfpxs_cpx_conf does not hold, thus we cannot invoke s_r_trans_LTC1 *)
-(* Basic_2A1: uses: lpxs_cpxs_trans *)
lemma lfpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpxs h G).
#h #G @s_r_to_s_rs_trans @s_r_trans_LTC2
@s_rs_trans_TC1 /2 width=3 by lfpx_cpxs_trans/ (**) (* full auto too slow *)
(* Advanced properties ******************************************************)
-(* Basic_2A1: uses: lpxs_refl *)
lemma lfpxs_refl: ∀h,G,T. reflexive … (lfpxs h G T).
/2 width=1 by tc_lfxs_refl/ qed.
(* v GNU General Public License Version 2 *)
(* *)
(**************************************************************************)
-(*
+
+include "basic_2/rt_computation/lpxs_lpx.ma".
+include "basic_2/rt_computation/lpxs_cpxs.ma".
include "basic_2/rt_computation/csx_cpxs.ma".
include "basic_2/rt_computation/csx_lsubr.ma".
-include "basic_2/rt_computation/lfsx_lpxs.ma".
-*)
+include "basic_2/rt_computation/lfsx_lpx.ma".
include "basic_2/rt_computation/lsubsx_lfsx.ma".
(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
-(*
-axiom lpxs_trans: ∀h,G. Transitive … (lpxs h G).
-*)
(* Advanced properties ******************************************************)
∀I. G ⊢ ⬈*[h, o, #0] 𝐒⦃K2.ⓑ{I}V⦄.
#h #o #G #K1 #V #H
@(csx_ind_cpxs … H) -V #V0 #_ #IHV0 #K2 #H
-@(lfsx_ind_lpxs … H) -K2 #K0 #HK0 #IHK0 #HK10 #I
-@lfsx_intro_lpxs #Y #HY #HnY
-elim (lpxs_inv_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
+@(lfsx_ind_lpx … H) -K2 #K0 #HK0 #IHK0 #HK10 #I
+@lfsx_intro_lpx #Y #HY #HnY
+elim (lpx_inv_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
elim (tdeq_dec h o V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnY ]
-[ /5 width=5 by lfsx_lfdeq_trans, lpxs_trans, lfdeq_pair/
+[ /5 width=5 by lfsx_lfdeq_trans, lpxs_step_dx, lfdeq_pair/
| @(IHV0 … HnV02) -IHV0 -HnV02
- [
- | /3 width=3 by lfsx_lpxs_trans, lfsx_cpxs_trans/
- | /2 width=3 by lpxs_trans/
+ [ /2 width=3 by lpxs_cpx_trans/
+ | /3 width=3 by lfsx_lpx_trans, lfsx_cpx_trans/
+ | /2 width=3 by lpxs_step_dx/
]
-
-(*
- @(lfsx_lpxs_trans … (K0.ⓑ{I}V2))
- [ @(IHV0 … HnV02 … HK10) -IHV0 -HnV02
- [
- | /2 width=3 by lfsx_cpxs_trans/
- ]
- |
- ]
-*)
+]
+qed.
(* Basic_2A1: uses: lsx_lref_be *)
-lemma lfsx_lref_pair: ∀h,o,G,K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ →
- ∀I,L,i. ⬇*[i] L ≡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
-#h #o #G #K #V #HV #HK #I #L #i #HLK
-@(lfsx_lifts … (#0) … HLK) -L /2 width=3 by lfsx_pair_lpxs/
+lemma lfsx_lref_pair_drops: ∀h,o,G,K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ →
+ ∀I,i,L. ⬇*[i] L ≡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+#h #o #G #K #V #HV #HK #I #i elim i -i
+[ #L #H >(drops_fwd_isid … H) -H /2 width=3 by lfsx_pair_lpxs/
+| #i #IH #L #H
+ elim (drops_inv_bind2_isuni_next … H) -H // #J #Y #HY #H destruct
+ @(lfsx_lifts … (𝐔❴1❵)) /3 width=6 by drops_refl, drops_drop/ (**) (* full auto fails *)
+]
qed.
(* Main properties **********************************************************)
-theorem csx_lsx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄.
+(* Basic_2A1: uses: csx_lsx *)
+theorem csx_lfsx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄.
#h #o #G #L #T @(fqup_wf_ind_eq (Ⓕ) … G L T) -G -L -T
#Z #Y #X #IH #G #L * * //
[ #i #HG #HL #HT #H destruct
elim (csx_inv_lref … H) -H [ |*: * ]
[ /2 width=1 by lfsx_lref_atom/
| /2 width=3 by lfsx_lref_unit/
- | /4 width=6 by lfsx_lref_pair, fqup_lref/
+ | /4 width=6 by lfsx_lref_pair_drops, fqup_lref/
]
-| #a #I #V #T #HG #HL #HT #H destruct
+| #p #I #V #T #HG #HL #HT #H destruct
elim (csx_fwd_bind_unit … H Void) -H /3 width=1 by lfsx_bind_void/
| #I #V #T #HG #HL #HT #H destruct
elim (csx_fwd_flat … H) -H /3 width=1 by lfsx_flat/
"uncounted parallel rt-computation (local environment)"
'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2).
+(* Basic properties *********************************************************)
+
+lemma lpxs_refl: ∀h,G. reflexive … (lpxs h G).
+/2 width=1 by lex_refl/ qed.
+
(* Basic inversion lemmas ***************************************************)
lemma lpxs_inv_bind_sn: ∀h,G,I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 →
--- /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/rt_computation/lfpxs_cpxs.ma".
+include "basic_2/rt_computation/lfpxs_lpxs.ma".
+
+(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
+
+(* Properties with uncounted context-sensitive rt-computation for terms *****)
+
+lemma lpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (λ_.lpxs h G).
+/3 width=3 by lfpxs_cpx_trans, lfpxs_lpxs/ qed-.
+
+lemma lpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (λ_.lpxs h G).
+/3 width=3 by lfpxs_cpxs_trans, lfpxs_lpxs/ qed-.
--- /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/relocation/lex_tc.ma".
+include "basic_2/rt_computation/lpxs.ma".
+include "basic_2/rt_computation/cpxs_lpx.ma".
+
+(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
+
+(* Properties with uncounted rt-transition for local environments ***********)
+
+(* Basic_2A1: was: lpxs_strap1 *)
+lemma lpxs_step_dx: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
+ ∀L2. ⦃G, L⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2.
+/3 width=3 by lpx_cpxs_trans, lex_ltc_step_dx/ qed-.
+
+(* Basic_2A1: was: lpxs_strap2 *)
+lemma lpxs_step_sn: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L →
+ ∀L2. ⦃G, L⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2.
+/3 width=3 by lpx_cpxs_trans, lex_ltc_step_sn/ qed-.
cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
cpxs_ext.ma
-lpxs.ma lpxs_length.ma
+lpxs.ma lpxs_length.ma lpxs_lpx.ma lpxs_cpxs.ma
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_lpx.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_csx.ma lfsx_lfsx.ma
lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma
[ [ "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" * ]
- [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" * ]
+ [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_lpx" + "lpxs_cpxs" * ]
[ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ]
[ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
projects / helm.git / commitdiff