#L0 #HL03 #HL10 #H elim (H T) -H /4 width=4 by/
qed-.
-(* these two are better expressed with the binder \chi *)
+(* this is better expressed with the binder \chi *)
lemma lsx_fwd_bind_dx: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L →
G ⊢ ⬈*[h, o, T, ⫯l] L.ⓑ{I}V.
@(lleq_lreq_trans … (L2.ⓑ{I}V1))
/2 width=2 by lleq_fwd_bind_dx, lreq_succ/
qed-.
-
-lemma lsx_inv_bind: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a, I}V.T, l] L →
- G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, ⫯l] L.ⓑ{I}V.
-/3 width=4 by lsx_fwd_bind_sn, lsx_fwd_bind_dx, conj/ 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/notation/relations/predtysnstrong_5.ma".
+include "basic_2/static/lfdeq.ma".
+include "basic_2/rt_transition/lfpx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
+
+definition lfsx: ∀h. sd h → relation3 term genv lenv ≝
+ λh,o,T,G. SN … (lfpx h G T) (lfdeq h o T).
+
+interpretation
+ "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)"
+ 'PRedTySNStrong h o T G L = (lfsx h o T G L).
+
+(* Basic eliminators ********************************************************)
+
+(* Basic_2A1: uses: lsx_ind *)
+lemma lfsx_ind: ∀h,o,G,T. ∀R:predicate lenv.
+ (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
+ R L1
+ ) →
+ ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
+#h #o #G #T #R #H0 #L1 #H elim H -L1
+/5 width=1 by SN_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: uses: lsx_intro *)
+lemma lfsx_intro: ∀h,o,G,L1,T.
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
+ G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
+/5 width=1 by SN_intro/ qed.
+
+(* Basic_2A1: uses: lsx_sort *)
+lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄.
+#h #o #G #L1 #s @lfsx_intro
+#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H *
+[ #H1 #H2 destruct //
+| #I1 #I2 #K1 #K2 #HK12 #H1 #H2 destruct
+ /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort, frees_inv_sort/
+]
+qed.
+
+(* Basic_2A1: uses: lsx_gref *)
+lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄.
+#h #o #G #L1 #s @lfsx_intro
+#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_gref … H) -H *
+[ #H1 #H2 destruct //
+| #I1 #I2 #K1 #K2 #HK12 #H1 #H2 destruct
+ /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref, frees_inv_gref/
+]
+qed.
+
+lemma lfsx_unit: ∀h,o,I,G,L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L.ⓤ{I}⦄.
+#h #o #I #G #L1 @lfsx_intro
+#Y #HY #HnY elim HnY -HnY /2 width=2 by lfxs_unit_sn/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+fact lfsx_fwd_pair_aux: ∀h,o,G,L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L⦄ →
+ ∀I,K,V. L = K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
+#h #o #G #L #H
+@(lfsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct
+/5 width=5 by lfpx_pair, lfsx_intro, lfdeq_fwd_zero_pair/
+qed-.
+
+lemma lfsx_fwd_pair: ∀h,o,I,G,K,V.
+ G ⊢ ⬈*[h, o, #0] 𝐒⦃K.ⓑ{I}V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
+/2 width=4 by lfsx_fwd_pair_aux/ qed-.
+
+(* Basic_2A1: removed theorems 9:
+ lsx_ge_up lsx_ge
+ lsxa_ind lsxa_intro lsxa_lleq_trans lsxa_lpxs_trans lsxa_intro_lpx lsx_lsxa lsxa_inv_lsx
+*)
--- /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/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_lpx.ma".
+include "basic_2/rt_computation/lsubsx_lfsx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lsx_lref_be_lpxs *)
+lemma lfsx_pair_lpxs: ∀h,o,G,K1,V. ⦃G, K1⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ →
+ ∀K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ → ⦃G, K1⦄ ⊢ ⬈*[h] K2 →
+ ∀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_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_step_dx, lfdeq_pair/
+| @(IHV0 … HnV02) -IHV0 -HnV02
+ [ /2 width=3 by lpxs_cpx_trans/
+ | /3 width=3 by lfsx_lpx_trans, lfsx_cpx_trans/
+ | /2 width=3 by lpxs_step_dx/
+ ]
+]
+qed.
+
+(* Basic_2A1: uses: lsx_lref_be *)
+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 **********************************************************)
+
+(* 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_drops, fqup_lref/
+ ]
+| #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/
+]
+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/static/lfdeq_length.ma".
+include "basic_2/static/lfdeq_drops.ma".
+include "basic_2/rt_transition/lfpx_length.ma".
+include "basic_2/rt_transition/lfpx_drops.ma".
+include "basic_2/rt_computation/lfsx_fqup.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
+
+(* Properties with generic relocation ***************************************)
+
+(* Note: this uses length *)
+(* Basic_2A1: uses: lsx_lift_le lsx_lift_ge *)
+lemma lfsx_lifts: ∀h,o,G. d_liftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄).
+#h #o #G #K #T #H @(lfsx_ind … H) -K
+#K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @lfsx_intro
+#L2 #HL12 #HnL12 elim (lfpx_drops_conf … HLK1 … HL12 … HTU)
+/5 width=9 by lfdeq_lifts_bi, lfpx_fwd_length/
+qed-.
+
+(* Inversion lemmas on relocation *******************************************)
+
+(* Basic_2A1: uses: lsx_inv_lift_le lsx_inv_lift_be lsx_inv_lift_ge *)
+lemma lfsx_inv_lifts: ∀h,o,G. d_deliftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄).
+#h #o #G #L #U #H @(lfsx_ind … H) -L
+#L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @lfsx_intro
+#K2 #HK12 #HnK12 elim (drops_lfpx_trans … HLK1 … HK12 … HTU) -HK12
+/4 width=10 by lfdeq_inv_lifts_bi/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lsx_lref_free *)
+lemma lfsx_lref_atom: ∀h,o,G,L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+#h #o #G #L1 #i #HL1
+@(lfsx_lifts … (#0) … HL1) -HL1 //
+qed.
+
+(* Basic_2A1: uses: lsx_lref_skip *)
+lemma lfsx_lref_unit: ∀h,o,I,G,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+#h #o #I #G #L1 #K1 #i #HL1
+@(lfsx_lifts … (#0) … HL1) -HL1 //
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+(* Basic_2A1: uses: lsx_fwd_lref_be *)
+lemma lfsx_fwd_lref_pair: ∀h,o,G,L,i. G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄ →
+ ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
+#h #o #G #L #i #HL #I #K #V #HLK
+lapply (lfsx_inv_lifts … HL … HLK … (#0) ?) -L
+/2 width=2 by lfsx_fwd_pair/
+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/static/lfdeq_fqup.ma".
+include "basic_2/rt_computation/lfsx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lsx_atom *)
+lemma lfsx_atom: ∀h,o,G,T. G ⊢ ⬈*[h, o, T] 𝐒⦃⋆⦄.
+#h #o #G #T @lfsx_intro
+#Y #H #HI lapply (lfpx_inv_atom_sn … H) -H
+#H destruct elim HI -HI //
+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/rt_computation/lfpxs_lfdeq.ma".
+include "basic_2/rt_computation/lfpxs_cpxs.ma".
+include "basic_2/rt_computation/lfpxs_lfpxs.ma".
+include "basic_2/rt_computation/lfsx_lfsx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
+
+(* Properties with unbound rt-computation on referred entries ***************)
+
+(* Basic_2A1: uses: lsx_intro_alt *)
+lemma lfsx_intro_lfpxs: ∀h,o,G,L1,T.
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
+ G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
+/4 width=1 by lfpx_lfpxs, lfsx_intro/ qed-.
+
+(* Basic_2A1: uses: lsx_lpxs_trans *)
+lemma lfsx_lfpxs_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
+#h #o #G #L1 #T #HL1 #L2 #H @(lfpxs_ind_sn … H) -L2
+/2 width=3 by lfsx_lfpx_trans/
+qed-.
+
+(* Eliminators with unbound rt-computation on referred entries **************)
+
+lemma lfsx_ind_lfpxs_lfdeq: ∀h,o,G,T. ∀R:predicate lenv.
+ (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
+ R L1
+ ) →
+ ∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h, T] L0 → ∀L2. L0 ≛[h, o, T] L2 → R L2.
+#h #o #G #T #R #IH #L1 #H @(lfsx_ind … H) -L1
+#L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02
+@IH -IH /3 width=3 by lfsx_lfpxs_trans, lfsx_lfdeq_trans/ -HL1 #K2 #HLK2 #HnLK2
+lapply (lfdeq_lfdneq_trans … HL02 … HnLK2) -HnLK2 #H
+elim (lfdeq_lfpxs_trans … HLK2 … HL02) -L2 #K0 #HLK0 #HK02
+lapply (lfdneq_lfdeq_canc_dx … H … HK02) -H #HnLK0
+elim (lfdeq_dec h o L1 L0 T) #H
+[ lapply (lfdeq_lfdneq_trans … H … HnLK0) -H -HnLK0 #Hn10
+ lapply (lfpxs_trans … HL10 … HLK0) -L0 #H10
+ elim (lfpxs_lfdneq_inv_step_sn … H10 … Hn10) -H10 -Hn10
+ /3 width=8 by lfdeq_trans/
+| elim (lfpxs_lfdneq_inv_step_sn … HL10 … H) -HL10 -H #L #K #HL1 #HnL1 #HLK #HKL0
+ elim (lfdeq_lfpxs_trans … HLK0 … HKL0) -L0
+ /3 width=8 by lfpxs_trans, lfdeq_trans/
+]
+qed-.
+
+(* Basic_2A1: uses: lsx_ind_alt *)
+lemma lfsx_ind_lfpxs: ∀h,o,G,T. ∀R:predicate lenv.
+ (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
+ R L1
+ ) →
+ ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
+#h #o #G #T #R #IH #L #HL
+@(lfsx_ind_lfpxs_lfdeq … IH … HL) -IH -HL // (**) (* full auto fails *)
+qed-.
+
+(* Advanced properties ******************************************************)
+
+fact lfsx_bind_lfpxs_aux: ∀h,o,p,I,G,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
+ ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ →
+ ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 →
+ G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄.
+#h #o #p #I #G #L1 #V #H @(lfsx_ind_lfpxs … H) -L1
+#L1 #_ #IHL1 #Y #T #H @(lfsx_ind_lfpxs … H) -Y
+#Y #HY #IHY #L2 #H #HL12 destruct
+@lfsx_intro_lfpxs #L0 #HL20
+lapply (lfpxs_trans … HL12 … HL20) #HL10 #H
+elim (lfdneq_inv_bind … H) -H [ -IHY | -HY -IHL1 -HL12 ]
+[ #HnV elim (lfdeq_dec h o L1 L2 V)
+ [ #HV @(IHL1 … L0) -IHL1 -HL12
+ /3 width=4 by lfsx_lfpxs_trans, lfpxs_fwd_bind_dx, lfpxs_fwd_pair_sn, lfdeq_canc_sn/ (**) (* full auto too slow *)
+ | -HnV -HL10 /4 width=4 by lfsx_lfpxs_trans, lfpxs_fwd_pair_sn/
+ ]
+| /3 width=4 by lfpxs_fwd_bind_dx/
+]
+qed-.
+
+(* Basic_2A1: uses: lsx_bind *)
+lemma lfsx_bind: ∀h,o,p,I,G,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ →
+ ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓑ{I}V⦄ →
+ G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄.
+/2 width=3 by lfsx_bind_lfpxs_aux/ qed.
+
+(* Basic_2A1: uses: lsx_flat_lpxs *)
+lemma lfsx_flat_lfpxs: ∀h,o,I,G,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
+ ∀L2,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄ → ⦃G, L1⦄ ⊢ ⬈*[h, ⓕ{I}V.T] L2 →
+ G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L2⦄.
+#h #o #I #G #L1 #V #H @(lfsx_ind_lfpxs … H) -L1
+#L1 #HL1 #IHL1 #L2 #T #H @(lfsx_ind_lfpxs … H) -L2
+#L2 #HL2 #IHL2 #HL12 @lfsx_intro_lfpxs
+#L0 #HL20 lapply (lfpxs_trans … HL12 … HL20)
+#HL10 #H elim (lfdneq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ]
+[ #HnV elim (lfdeq_dec h o L1 L2 V)
+ [ #HV @(IHL1 … L0) -IHL1 -HL12
+ /3 width=5 by lfsx_lfpxs_trans, lfpxs_fwd_flat_dx, lfpxs_fwd_pair_sn, lfdeq_canc_sn/ (**) (* full auto too slow: 47s *)
+ | -HnV -HL10 /4 width=4 by lfsx_lfpxs_trans, lfpxs_fwd_pair_sn/
+ ]
+| /3 width=3 by lfpxs_fwd_flat_dx/
+]
+qed-.
+
+(* Basic_2A1: uses: lsx_flat *)
+lemma lfsx_flat: ∀h,o,I,G,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ →
+ ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄.
+/2 width=3 by lfsx_flat_lfpxs/ qed.
+
+fact lfsx_bind_lfpxs_void_aux: ∀h,o,p,I,G,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
+ ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ →
+ ∀L2. Y = L2.ⓧ → ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 →
+ G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄.
+#h #o #p #I #G #L1 #V #H @(lfsx_ind_lfpxs … H) -L1
+#L1 #_ #IHL1 #Y #T #H @(lfsx_ind_lfpxs … H) -Y
+#Y #HY #IHY #L2 #H #HL12 destruct
+@lfsx_intro_lfpxs #L0 #HL20
+lapply (lfpxs_trans … HL12 … HL20) #HL10 #H
+elim (lfdneq_inv_bind_void … H) -H [ -IHY | -HY -IHL1 -HL12 ]
+[ #HnV elim (lfdeq_dec h o L1 L2 V)
+ [ #HV @(IHL1 … L0) -IHL1 -HL12
+ /3 width=6 by lfsx_lfpxs_trans, lfpxs_fwd_bind_dx_void, lfpxs_fwd_pair_sn, lfdeq_canc_sn/ (**) (* full auto too slow *)
+ | -HnV -HL10 /4 width=4 by lfsx_lfpxs_trans, lfpxs_fwd_pair_sn/
+ ]
+| /3 width=4 by lfpxs_fwd_bind_dx_void/
+]
+qed-.
+
+lemma lfsx_bind_void: ∀h,o,p,I,G,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ →
+ ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄ →
+ G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄.
+/2 width=3 by lfsx_bind_lfpxs_void_aux/ 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/rt_transition/lfpx_lfdeq.ma".
+include "basic_2/rt_computation/lfsx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lsx_lleq_trans *)
+lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L2. L1 ≛[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
+#h #o #G #L1 #T #H @(lfsx_ind … H) -L1
+#L1 #_ #IHL1 #L2 #HL12 @lfsx_intro
+#L #HL2 #HnL2 elim (lfdeq_lfpx_trans … HL2 … HL12) -HL2
+/4 width=5 by lfdeq_repl/
+qed-.
+
+(* Basic_2A1: uses: lsx_lpx_trans *)
+lemma lfsx_lfpx_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
+#h #o #G #L1 #T #H @(lfsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
+elim (lfdeq_dec h o L1 L2 T) /3 width=4 by lfsx_lfdeq_trans, lfxs_refl/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+(* Basic_2A1: uses: lsx_fwd_pair_sn lsx_fwd_bind_sn lsx_fwd_flat_sn *)
+lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ②{I}V.T] 𝐒⦃L⦄ →
+ G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄.
+#h #o #I #G #L #V #T #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #H #HnL12 elim (lfpx_pair_sn_split … H o I T) -H
+/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_pair_sn/
+qed-.
+
+(* Basic_2A1: uses: lsx_fwd_flat_dx *)
+lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ →
+ G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄.
+#h #o #I #G #L #V #T #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #H #HnL12 elim (lfpx_flat_dx_split … H o I V) -H
+/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_flat_dx/
+qed-.
+
+(* Basic_2A1: uses: lsx_fwd_bind_dx *)
+(* Note: the exclusion binder (ⓧ) makes this more elegant and much simpler *)
+lemma lfsx_fwd_bind_dx: ∀h,o,p,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ →
+ G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄.
+#h #o #p #I #G #L #V #T #H @(lfsx_ind … H) -L
+#L1 #_ #IH @lfsx_intro
+#L2 #H #HT elim (lfpx_bind_dx_split_void … H o p I V) -H
+/6 width=5 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_bind_dx_void/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_2A1: uses: lsx_inv_flat *)
+lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ →
+ G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ ∧ G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄.
+/3 width=3 by lfsx_fwd_pair_sn, lfsx_fwd_flat_dx, conj/ qed-.
+
+(* Basic_2A1: uses: lsx_inv_bind *)
+lemma lfsx_inv_bind: ∀h,o,p,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ →
+ G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ ∧ G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄.
+/3 width=4 by lfsx_fwd_pair_sn, lfsx_fwd_bind_dx, conj/ 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/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 UNBOUND PARALLEL RT-TRANSITION ******)
+
+(* Properties with unbound 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 unbound 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-.
--- /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_computation/lfpxs_lpxs.ma".
+include "basic_2/rt_computation/lfsx_lfpxs.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
+
+(* Properties with unbound rt-computation ***********************************)
+
+lemma lfsx_intro_lpxs: ∀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_lfpxs #L2 #H
+elim (lfpxs_inv_lpxs_lfeq … H) -H
+/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfeq_lfdeq/
+qed-.
+
+lemma lfsx_lpxs_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_lfpxs_trans, lfpxs_lpxs/ qed-.
+
+(* Eliminators with unbound rt-computation **********************************)
+
+lemma lfsx_ind_lpxs: ∀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_lfpxs, lfpxs_lpxs/ qed-.
+++ /dev/null
-lemma lprs_aaa_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
- ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
-/3 width=5 by lprs_lpxs, lpxs_aaa_conf/ qed-.
+++ /dev/null
-(* Basic_2A1: was just: lprs_lpxs *)
-lemma lprs_lfpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2.
-/3 width=3 by lpr_lpx, monotonic_TC/ 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/notation/relations/predtysnstrong_5.ma".
-include "basic_2/static/lfdeq.ma".
-include "basic_2/rt_transition/lfpx.ma".
-
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
-
-definition lfsx: ∀h. sd h → relation3 term genv lenv ≝
- λh,o,T,G. SN … (lfpx h G T) (lfdeq h o T).
-
-interpretation
- "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)"
- 'PRedTySNStrong h o T G L = (lfsx h o T G L).
-
-(* Basic eliminators ********************************************************)
-
-(* Basic_2A1: uses: lsx_ind *)
-lemma lfsx_ind: ∀h,o,G,T. ∀R:predicate lenv.
- (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
- R L1
- ) →
- ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
-#h #o #G #T #R #H0 #L1 #H elim H -L1
-/5 width=1 by SN_intro/
-qed-.
-
-(* Basic properties *********************************************************)
-
-(* Basic_2A1: uses: lsx_intro *)
-lemma lfsx_intro: ∀h,o,G,L1,T.
- (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
- G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
-/5 width=1 by SN_intro/ qed.
-
-(* Basic_2A1: uses: lsx_sort *)
-lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄.
-#h #o #G #L1 #s @lfsx_intro
-#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H *
-[ #H1 #H2 destruct //
-| #I1 #I2 #K1 #K2 #HK12 #H1 #H2 destruct
- /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort, frees_inv_sort/
-]
-qed.
-
-(* Basic_2A1: uses: lsx_gref *)
-lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄.
-#h #o #G #L1 #s @lfsx_intro
-#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_gref … H) -H *
-[ #H1 #H2 destruct //
-| #I1 #I2 #K1 #K2 #HK12 #H1 #H2 destruct
- /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref, frees_inv_gref/
-]
-qed.
-
-lemma lfsx_unit: ∀h,o,I,G,L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L.ⓤ{I}⦄.
-#h #o #I #G #L1 @lfsx_intro
-#Y #HY #HnY elim HnY -HnY /2 width=2 by lfxs_unit_sn/
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-fact lfsx_fwd_pair_aux: ∀h,o,G,L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L⦄ →
- ∀I,K,V. L = K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
-#h #o #G #L #H
-@(lfsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct
-/5 width=5 by lfpx_pair, lfsx_intro, lfdeq_fwd_zero_pair/
-qed-.
-
-lemma lfsx_fwd_pair: ∀h,o,I,G,K,V.
- G ⊢ ⬈*[h, o, #0] 𝐒⦃K.ⓑ{I}V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
-/2 width=4 by lfsx_fwd_pair_aux/ qed-.
-
-(* Basic_2A1: removed theorems 9:
- lsx_ge_up lsx_ge
- lsxa_ind lsxa_intro lsxa_lleq_trans lsxa_lpxs_trans lsxa_intro_lpx lsx_lsxa lsxa_inv_lsx
-*)
+++ /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/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_lpx.ma".
-include "basic_2/rt_computation/lsubsx_lfsx.ma".
-
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
-
-(* Advanced properties ******************************************************)
-
-(* Basic_2A1: uses: lsx_lref_be_lpxs *)
-lemma lfsx_pair_lpxs: ∀h,o,G,K1,V. ⦃G, K1⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ →
- ∀K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ → ⦃G, K1⦄ ⊢ ⬈*[h] K2 →
- ∀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_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_step_dx, lfdeq_pair/
-| @(IHV0 … HnV02) -IHV0 -HnV02
- [ /2 width=3 by lpxs_cpx_trans/
- | /3 width=3 by lfsx_lpx_trans, lfsx_cpx_trans/
- | /2 width=3 by lpxs_step_dx/
- ]
-]
-qed.
-
-(* Basic_2A1: uses: lsx_lref_be *)
-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 **********************************************************)
-
-(* 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_drops, fqup_lref/
- ]
-| #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/
-]
-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/static/lfdeq_length.ma".
-include "basic_2/static/lfdeq_drops.ma".
-include "basic_2/rt_transition/lfpx_length.ma".
-include "basic_2/rt_transition/lfpx_drops.ma".
-include "basic_2/rt_computation/lfsx_fqup.ma".
-
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
-
-(* Properties with generic relocation ***************************************)
-
-(* Note: this uses length *)
-(* Basic_2A1: uses: lsx_lift_le lsx_lift_ge *)
-lemma lfsx_lifts: ∀h,o,G. d_liftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄).
-#h #o #G #K #T #H @(lfsx_ind … H) -K
-#K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @lfsx_intro
-#L2 #HL12 #HnL12 elim (lfpx_drops_conf … HLK1 … HL12 … HTU)
-/5 width=9 by lfdeq_lifts_bi, lfpx_fwd_length/
-qed-.
-
-(* Inversion lemmas on relocation *******************************************)
-
-(* Basic_2A1: uses: lsx_inv_lift_le lsx_inv_lift_be lsx_inv_lift_ge *)
-lemma lfsx_inv_lifts: ∀h,o,G. d_deliftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄).
-#h #o #G #L #U #H @(lfsx_ind … H) -L
-#L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @lfsx_intro
-#K2 #HK12 #HnK12 elim (drops_lfpx_trans … HLK1 … HK12 … HTU) -HK12
-/4 width=10 by lfdeq_inv_lifts_bi/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-(* Basic_2A1: uses: lsx_lref_free *)
-lemma lfsx_lref_atom: ∀h,o,G,L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
-#h #o #G #L1 #i #HL1
-@(lfsx_lifts … (#0) … HL1) -HL1 //
-qed.
-
-(* Basic_2A1: uses: lsx_lref_skip *)
-lemma lfsx_lref_unit: ∀h,o,I,G,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
-#h #o #I #G #L1 #K1 #i #HL1
-@(lfsx_lifts … (#0) … HL1) -HL1 //
-qed.
-
-(* Advanced forward lemmas **************************************************)
-
-(* Basic_2A1: uses: lsx_fwd_lref_be *)
-lemma lfsx_fwd_lref_pair: ∀h,o,G,L,i. G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄ →
- ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
-#h #o #G #L #i #HL #I #K #V #HLK
-lapply (lfsx_inv_lifts … HL … HLK … (#0) ?) -L
-/2 width=2 by lfsx_fwd_pair/
-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/static/lfdeq_fqup.ma".
-include "basic_2/rt_computation/lfsx.ma".
-
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
-
-(* Advanced properties ******************************************************)
-
-(* Basic_2A1: uses: lsx_atom *)
-lemma lfsx_atom: ∀h,o,G,T. G ⊢ ⬈*[h, o, T] 𝐒⦃⋆⦄.
-#h #o #G #T @lfsx_intro
-#Y #H #HI lapply (lfpx_inv_atom_sn … H) -H
-#H destruct elim HI -HI //
-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/rt_computation/lfpxs_lfdeq.ma".
-include "basic_2/rt_computation/lfpxs_cpxs.ma".
-include "basic_2/rt_computation/lfpxs_lfpxs.ma".
-include "basic_2/rt_computation/lfsx_lfsx.ma".
-
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
-
-(* Properties with unbound rt-computation on referred entries ***************)
-
-(* Basic_2A1: uses: lsx_intro_alt *)
-lemma lfsx_intro_lfpxs: ∀h,o,G,L1,T.
- (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
- G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
-/4 width=1 by lfpx_lfpxs, lfsx_intro/ qed-.
-
-(* Basic_2A1: uses: lsx_lpxs_trans *)
-lemma lfsx_lfpxs_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
-#h #o #G #L1 #T #HL1 #L2 #H @(lfpxs_ind_sn … H) -L2
-/2 width=3 by lfsx_lfpx_trans/
-qed-.
-
-(* Eliminators with unbound rt-computation on referred entries **************)
-
-lemma lfsx_ind_lfpxs_lfdeq: ∀h,o,G,T. ∀R:predicate lenv.
- (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
- R L1
- ) →
- ∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h, T] L0 → ∀L2. L0 ≛[h, o, T] L2 → R L2.
-#h #o #G #T #R #IH #L1 #H @(lfsx_ind … H) -L1
-#L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02
-@IH -IH /3 width=3 by lfsx_lfpxs_trans, lfsx_lfdeq_trans/ -HL1 #K2 #HLK2 #HnLK2
-lapply (lfdeq_lfdneq_trans … HL02 … HnLK2) -HnLK2 #H
-elim (lfdeq_lfpxs_trans … HLK2 … HL02) -L2 #K0 #HLK0 #HK02
-lapply (lfdneq_lfdeq_canc_dx … H … HK02) -H #HnLK0
-elim (lfdeq_dec h o L1 L0 T) #H
-[ lapply (lfdeq_lfdneq_trans … H … HnLK0) -H -HnLK0 #Hn10
- lapply (lfpxs_trans … HL10 … HLK0) -L0 #H10
- elim (lfpxs_lfdneq_inv_step_sn … H10 … Hn10) -H10 -Hn10
- /3 width=8 by lfdeq_trans/
-| elim (lfpxs_lfdneq_inv_step_sn … HL10 … H) -HL10 -H #L #K #HL1 #HnL1 #HLK #HKL0
- elim (lfdeq_lfpxs_trans … HLK0 … HKL0) -L0
- /3 width=8 by lfpxs_trans, lfdeq_trans/
-]
-qed-.
-
-(* Basic_2A1: uses: lsx_ind_alt *)
-lemma lfsx_ind_lfpxs: ∀h,o,G,T. ∀R:predicate lenv.
- (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
- R L1
- ) →
- ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
-#h #o #G #T #R #IH #L #HL
-@(lfsx_ind_lfpxs_lfdeq … IH … HL) -IH -HL // (**) (* full auto fails *)
-qed-.
-
-(* Advanced properties ******************************************************)
-
-fact lfsx_bind_lfpxs_aux: ∀h,o,p,I,G,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
- ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ →
- ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 →
- G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄.
-#h #o #p #I #G #L1 #V #H @(lfsx_ind_lfpxs … H) -L1
-#L1 #_ #IHL1 #Y #T #H @(lfsx_ind_lfpxs … H) -Y
-#Y #HY #IHY #L2 #H #HL12 destruct
-@lfsx_intro_lfpxs #L0 #HL20
-lapply (lfpxs_trans … HL12 … HL20) #HL10 #H
-elim (lfdneq_inv_bind … H) -H [ -IHY | -HY -IHL1 -HL12 ]
-[ #HnV elim (lfdeq_dec h o L1 L2 V)
- [ #HV @(IHL1 … L0) -IHL1 -HL12
- /3 width=4 by lfsx_lfpxs_trans, lfpxs_fwd_bind_dx, lfpxs_fwd_pair_sn, lfdeq_canc_sn/ (**) (* full auto too slow *)
- | -HnV -HL10 /4 width=4 by lfsx_lfpxs_trans, lfpxs_fwd_pair_sn/
- ]
-| /3 width=4 by lfpxs_fwd_bind_dx/
-]
-qed-.
-
-(* Basic_2A1: uses: lsx_bind *)
-lemma lfsx_bind: ∀h,o,p,I,G,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ →
- ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓑ{I}V⦄ →
- G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄.
-/2 width=3 by lfsx_bind_lfpxs_aux/ qed.
-
-(* Basic_2A1: uses: lsx_flat_lpxs *)
-lemma lfsx_flat_lfpxs: ∀h,o,I,G,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
- ∀L2,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄ → ⦃G, L1⦄ ⊢ ⬈*[h, ⓕ{I}V.T] L2 →
- G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L2⦄.
-#h #o #I #G #L1 #V #H @(lfsx_ind_lfpxs … H) -L1
-#L1 #HL1 #IHL1 #L2 #T #H @(lfsx_ind_lfpxs … H) -L2
-#L2 #HL2 #IHL2 #HL12 @lfsx_intro_lfpxs
-#L0 #HL20 lapply (lfpxs_trans … HL12 … HL20)
-#HL10 #H elim (lfdneq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ]
-[ #HnV elim (lfdeq_dec h o L1 L2 V)
- [ #HV @(IHL1 … L0) -IHL1 -HL12
- /3 width=5 by lfsx_lfpxs_trans, lfpxs_fwd_flat_dx, lfpxs_fwd_pair_sn, lfdeq_canc_sn/ (**) (* full auto too slow: 47s *)
- | -HnV -HL10 /4 width=4 by lfsx_lfpxs_trans, lfpxs_fwd_pair_sn/
- ]
-| /3 width=3 by lfpxs_fwd_flat_dx/
-]
-qed-.
-
-(* Basic_2A1: uses: lsx_flat *)
-lemma lfsx_flat: ∀h,o,I,G,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ →
- ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄.
-/2 width=3 by lfsx_flat_lfpxs/ qed.
-
-fact lfsx_bind_lfpxs_void_aux: ∀h,o,p,I,G,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
- ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ →
- ∀L2. Y = L2.ⓧ → ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 →
- G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄.
-#h #o #p #I #G #L1 #V #H @(lfsx_ind_lfpxs … H) -L1
-#L1 #_ #IHL1 #Y #T #H @(lfsx_ind_lfpxs … H) -Y
-#Y #HY #IHY #L2 #H #HL12 destruct
-@lfsx_intro_lfpxs #L0 #HL20
-lapply (lfpxs_trans … HL12 … HL20) #HL10 #H
-elim (lfdneq_inv_bind_void … H) -H [ -IHY | -HY -IHL1 -HL12 ]
-[ #HnV elim (lfdeq_dec h o L1 L2 V)
- [ #HV @(IHL1 … L0) -IHL1 -HL12
- /3 width=6 by lfsx_lfpxs_trans, lfpxs_fwd_bind_dx_void, lfpxs_fwd_pair_sn, lfdeq_canc_sn/ (**) (* full auto too slow *)
- | -HnV -HL10 /4 width=4 by lfsx_lfpxs_trans, lfpxs_fwd_pair_sn/
- ]
-| /3 width=4 by lfpxs_fwd_bind_dx_void/
-]
-qed-.
-
-lemma lfsx_bind_void: ∀h,o,p,I,G,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ →
- ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄ →
- G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄.
-/2 width=3 by lfsx_bind_lfpxs_void_aux/ 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/rt_transition/lfpx_lfdeq.ma".
-include "basic_2/rt_computation/lfsx.ma".
-
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
-
-(* Advanced properties ******************************************************)
-
-(* Basic_2A1: uses: lsx_lleq_trans *)
-lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- ∀L2. L1 ≛[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
-#h #o #G #L1 #T #H @(lfsx_ind … H) -L1
-#L1 #_ #IHL1 #L2 #HL12 @lfsx_intro
-#L #HL2 #HnL2 elim (lfdeq_lfpx_trans … HL2 … HL12) -HL2
-/4 width=5 by lfdeq_repl/
-qed-.
-
-(* Basic_2A1: uses: lsx_lpx_trans *)
-lemma lfsx_lfpx_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
-#h #o #G #L1 #T #H @(lfsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
-elim (lfdeq_dec h o L1 L2 T) /3 width=4 by lfsx_lfdeq_trans, lfxs_refl/
-qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-(* Basic_2A1: uses: lsx_fwd_pair_sn lsx_fwd_bind_sn lsx_fwd_flat_sn *)
-lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ②{I}V.T] 𝐒⦃L⦄ →
- G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄.
-#h #o #I #G #L #V #T #H @(lfsx_ind … H) -L
-#L1 #_ #IHL1 @lfsx_intro
-#L2 #H #HnL12 elim (lfpx_pair_sn_split … H o I T) -H
-/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_pair_sn/
-qed-.
-
-(* Basic_2A1: uses: lsx_fwd_flat_dx *)
-lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ →
- G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄.
-#h #o #I #G #L #V #T #H @(lfsx_ind … H) -L
-#L1 #_ #IHL1 @lfsx_intro
-#L2 #H #HnL12 elim (lfpx_flat_dx_split … H o I V) -H
-/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_flat_dx/
-qed-.
-
-(* Basic_2A1: uses: lsx_fwd_bind_dx *)
-(* Note: the exclusion binder (ⓧ) makes this more elegant and much simpler *)
-lemma lfsx_fwd_bind_dx: ∀h,o,p,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ →
- G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄.
-#h #o #p #I #G #L #V #T #H @(lfsx_ind … H) -L
-#L1 #_ #IH @lfsx_intro
-#L2 #H #HT elim (lfpx_bind_dx_split_void … H o p I V) -H
-/6 width=5 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_bind_dx_void/
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-(* Basic_2A1: uses: lsx_inv_flat *)
-lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ →
- G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ ∧ G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄.
-/3 width=3 by lfsx_fwd_pair_sn, lfsx_fwd_flat_dx, conj/ qed-.
-
-(* Basic_2A1: uses: lsx_inv_bind *)
-lemma lfsx_inv_bind: ∀h,o,p,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ →
- G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ ∧ G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄.
-/3 width=4 by lfsx_fwd_pair_sn, lfsx_fwd_bind_dx, conj/ 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/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 UNBOUND PARALLEL RT-TRANSITION ******)
-
-(* Properties with unbound 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 unbound 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-.
+++ /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_computation/lfpxs_lpxs.ma".
-include "basic_2/rt_computation/lfsx_lfpxs.ma".
-
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
-
-(* Properties with unbound rt-computation ***********************************)
-
-lemma lfsx_intro_lpxs: ∀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_lfpxs #L2 #H
-elim (lfpxs_inv_lpxs_lfeq … H) -H
-/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfeq_lfdeq/
-qed-.
-
-lemma lfsx_lpxs_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_lfpxs_trans, lfpxs_lpxs/ qed-.
-
-(* Eliminators with unbound rt-computation **********************************)
-
-lemma lfsx_ind_lpxs: ∀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_lfpxs, lfpxs_lpxs/ qed-.
--- /dev/null
+lemma lprs_aaa_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+/3 width=5 by lprs_lpxs, lpxs_aaa_conf/ qed-.
--- /dev/null
+include "basic_2/rt_computation/lprs.ma".
+
+lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
+/3 width=3 by lpr_lpx, monotonic_TC/ qed.
(**************************************************************************)
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 UNBOUND RT-TRANSITION **********)
+++ /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/lfsx_drops.ma".
-include "basic_2/rt_computation/lfsx_lfpxs.ma".
-include "basic_2/rt_computation/lsubsx.ma".
-
-(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNBOUND RT-TRANSITION **********)
-
-(* Properties with strong normalizing env's for unbound rt-transition *******)
-
-(* Basic_2A1: uses: lsx_cpx_trans_lcosx *)
-lemma lfsx_cpx_trans_lsubsx: ∀h,o,G,L0,T1,T2. ⦃G, L0⦄ ⊢ T1 ⬈[h] T2 →
- ∀f,L. G ⊢ L0 ⊆ⓧ[h, o, f] L →
- G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
-#h #o #G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2 //
-[ #I0 #G #K0 #V1 #V2 #W2 #_ #IH #HVW2 #g #L #HK0 #HL
- elim (lsubsx_inv_pair_sn_gen … HK0) -HK0 *
- [ #f #K #HK0 #H1 #H2 destruct
- /4 width=8 by lfsx_lifts, lfsx_fwd_pair, drops_refl, drops_drop/
- | #f #K #HV1 #HK0 #H1 #H2 destruct
- /4 width=8 by lfsx_lifts, drops_refl, drops_drop/
- ]
-| #I0 #G #K0 #T #U #i #_ #IH #HTU #g #L #HK0 #HL
- elim (lsubsx_fwd_bind_sn … HK0) -HK0 #I #K #HK0 #H destruct
- /6 width=8 by lfsx_inv_lifts, lfsx_lifts, drops_refl, drops_drop/
-| #p #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
- elim (lfsx_inv_bind … HL) -HL
- /4 width=2 by lsubsx_pair, lfsx_bind_void/
-| #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
- elim (lfsx_inv_flat … HL) -HL /3 width=2 by lfsx_flat/
-| #G #L0 #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #f #L #HL0 #HL
- elim (lfsx_inv_bind … HL) -HL #HV #HU1
- /4 width=8 by lsubsx_pair, lfsx_inv_lifts, drops_refl, drops_drop/
-| #G #L0 #V #T1 #T2 #_ #IHT12 #f #L #HL0 #HL
- elim (lfsx_inv_flat … HL) -HL /2 width=2 by/
-| #G #L0 #V1 #V2 #T #_ #IHV12 #f #L #HL0 #HL
- elim (lfsx_inv_flat … HL) -HL /2 width=2 by/
-| #p #G #L0 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #f #L #HL0 #HL
- elim (lfsx_inv_flat … HL) -HL #HV1 #HL
- elim (lfsx_inv_bind … HL) -HL #HW1 #HT1
- /4 width=2 by lsubsx_pair, lfsx_bind_void, lfsx_flat/
-| #p #G #L0 #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #HVU2 #f #L #HL0 #HL
- elim (lfsx_inv_flat … HL) -HL #HV1 #HL
- elim (lfsx_inv_bind … HL) -HL #HW1 #HT1
- /6 width=8 by lsubsx_pair, lfsx_lifts, lfsx_bind_void, lfsx_flat, drops_refl, drops_drop/
-]
-qed-.
-
-(* Basic_2A1: uses: lsx_cpx_trans_O *)
-lemma lfsx_cpx_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
- G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
-/3 width=6 by lfsx_cpx_trans_lsubsx, lsubsx_refl/ qed-.
-
-(* Properties with strong normalizing env's for unbound rt-computation ******)
-
-lemma lfsx_cpxs_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
- G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
-#h #o #G #L #T1 #T2 #H
-@(cpxs_ind_dx ???????? H) -T1 //
-/3 width=3 by lfsx_cpx_trans/
-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/rt_computation/rdsx_drops.ma".
+include "basic_2/rt_computation/rdsx_lpxs.ma".
+include "basic_2/rt_computation/lsubsx.ma".
+
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNBOUND RT-TRANSITION **********)
+
+(* Properties with strongly normalizing referred local environments *********)
+
+(* Basic_2A1: uses: lsx_cpx_trans_lcosx *)
+lemma rdsx_cpx_trans_lsubsx (h) (o): ∀G,L0,T1,T2. ⦃G, L0⦄ ⊢ T1 ⬈[h] T2 →
+ ∀f,L. G ⊢ L0 ⊆ⓧ[h, o, f] L →
+ G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
+#h #o #G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2 //
+[ #I0 #G #K0 #V1 #V2 #W2 #_ #IH #HVW2 #g #L #HK0 #HL
+ elim (lsubsx_inv_pair_sn_gen … HK0) -HK0 *
+ [ #f #K #HK0 #H1 #H2 destruct
+ /4 width=8 by rdsx_lifts, rdsx_fwd_pair, drops_refl, drops_drop/
+ | #f #K #HV1 #HK0 #H1 #H2 destruct
+ /4 width=8 by rdsx_lifts, drops_refl, drops_drop/
+ ]
+| #I0 #G #K0 #T #U #i #_ #IH #HTU #g #L #HK0 #HL
+ elim (lsubsx_fwd_bind_sn … HK0) -HK0 #I #K #HK0 #H destruct
+ /6 width=8 by rdsx_inv_lifts, rdsx_lifts, drops_refl, drops_drop/
+| #p #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
+ elim (rdsx_inv_bind … HL) -HL
+ /4 width=2 by lsubsx_pair, rdsx_bind_void/
+| #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
+ elim (rdsx_inv_flat … HL) -HL /3 width=2 by rdsx_flat/
+| #G #L0 #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #f #L #HL0 #HL
+ elim (rdsx_inv_bind … HL) -HL #HV #HU1
+ /4 width=8 by lsubsx_pair, rdsx_inv_lifts, drops_refl, drops_drop/
+| #G #L0 #V #T1 #T2 #_ #IHT12 #f #L #HL0 #HL
+ elim (rdsx_inv_flat … HL) -HL /2 width=2 by/
+| #G #L0 #V1 #V2 #T #_ #IHV12 #f #L #HL0 #HL
+ elim (rdsx_inv_flat … HL) -HL /2 width=2 by/
+| #p #G #L0 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #f #L #HL0 #HL
+ elim (rdsx_inv_flat … HL) -HL #HV1 #HL
+ elim (rdsx_inv_bind … HL) -HL #HW1 #HT1
+ /4 width=2 by lsubsx_pair, rdsx_bind_void, rdsx_flat/
+| #p #G #L0 #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #HVU2 #f #L #HL0 #HL
+ elim (rdsx_inv_flat … HL) -HL #HV1 #HL
+ elim (rdsx_inv_bind … HL) -HL #HW1 #HT1
+ /6 width=8 by lsubsx_pair, rdsx_lifts, rdsx_bind_void, rdsx_flat, drops_refl, drops_drop/
+]
+qed-.
+
+(* Advanced properties of strongly normalizing referred local environments **)
+
+(* Basic_2A1: uses: lsx_cpx_trans_O *)
+lemma rdsx_cpx_trans (h) (o): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
+ G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
+/3 width=6 by rdsx_cpx_trans_lsubsx, lsubsx_refl/ qed-.
+
+lemma rdsx_cpxs_trans (h) (o): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
+ G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
+#h #o #G #L #T1 #T2 #H
+@(cpxs_ind_dx ???????? H) -T1 //
+/3 width=3 by rdsx_cpx_trans/
+qed-.
lpxs.ma lpxs_length.ma lpxs_drops.ma lpxs_lfdeq.ma lpxs_ffdeq.ma lpxs_aaa.ma lpxs_lpx.ma lpxs_cpxs.ma lpxs_lpxs.ma
csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_ffdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_fpbq.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_csx.ma lfsx_lfsx.ma
+rdsx.ma rdsx_length.ma rdsx_drops.ma rdsx_fqup.ma rdsx_lpxs.ma rdsx_csx.ma rdsx_rdsx.ma
lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma
fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma
fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lfpxs.ma fpbg_fpbs.ma fpbg_fpbg.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/notation/relations/predtysnstrong_5.ma".
+include "basic_2/static/lfdeq.ma".
+include "basic_2/rt_transition/lpx.ma".
+
+(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
+
+definition rdsx (h) (o) (G) (T): predicate lenv ≝
+ SN … (lpx h G) (lfdeq h o T).
+
+interpretation
+ "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)"
+ 'PRedTySNStrong h o T G L = (rdsx h o G T L).
+
+(* Basic eliminators ********************************************************)
+
+(* Basic_2A1: uses: lsx_ind *)
+lemma rdsx_ind (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.
+#h #o #G #T #R #H0 #L1 #H elim H -L1
+/5 width=1 by SN_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: uses: lsx_intro *)
+lemma rdsx_intro (h) (o) (G) (T):
+ ∀L1.
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
+ G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
+/5 width=1 by SN_intro/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+(* Basic_2A1: uses: lsx_fwd_pair_sn lsx_fwd_bind_sn lsx_fwd_flat_sn *)
+lemma rdsx_fwd_pair_sn (h) (o) (G):
+ ∀I,L,V,T. G ⊢ ⬈*[h, o, ②{I}V.T] 𝐒⦃L⦄ →
+ G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄.
+#h #o #G #I #L #V #T #H
+@(rdsx_ind … H) -L #L1 #_ #IHL1
+@rdsx_intro #L2 #HL12 #HnL12
+/4 width=3 by lfdeq_fwd_pair_sn/
+qed-.
+
+(* Basic_2A1: uses: lsx_fwd_flat_dx *)
+lemma rdsx_fwd_flat_dx (h) (o) (G):
+ ∀I,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ →
+ G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄.
+#h #o #G #I #L #V #T #H
+@(rdsx_ind … H) -L #L1 #_ #IHL1
+@rdsx_intro #L2 #HL12 #HnL12
+/4 width=3 by lfdeq_fwd_flat_dx/
+qed-.
+
+fact rdsx_fwd_pair_aux (h) (o) (G): ∀L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L⦄ →
+ ∀I,K,V. L = K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
+#h #o #G #L #H
+@(rdsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct
+/5 width=5 by lpx_pair, rdsx_intro, lfdeq_fwd_zero_pair/
+qed-.
+
+lemma rdsx_fwd_pair (h) (o) (G):
+ ∀I,K,V. G ⊢ ⬈*[h, o, #0] 𝐒⦃K.ⓑ{I}V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
+/2 width=4 by rdsx_fwd_pair_aux/ qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+(* Basic_2A1: uses: lsx_inv_flat *)
+lemma rdsx_inv_flat (h) (o) (G): ∀I,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ →
+ ∧∧ G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ & G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄.
+/3 width=3 by rdsx_fwd_pair_sn, rdsx_fwd_flat_dx, conj/ qed-.
+
+(* Basic_2A1: removed theorems 9:
+ lsx_ge_up lsx_ge
+ lsxa_ind lsxa_intro lsxa_lleq_trans lsxa_lpxs_trans lsxa_intro_lpx lsx_lsxa lsxa_inv_lsx
+*)
--- /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/csx_lsubr.ma".
+include "basic_2/rt_computation/csx_cpxs.ma".
+include "basic_2/rt_computation/lsubsx_rdsx.ma".
+
+(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lsx_lref_be_lpxs *)
+lemma rdsx_pair_lpxs (h) (o) (G):
+ ∀K1,V. ⦃G, K1⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ →
+ ∀K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ → ⦃G, K1⦄ ⊢ ⬈*[h] K2 →
+ ∀I. G ⊢ ⬈*[h, o, #0] 𝐒⦃K2.ⓑ{I}V⦄.
+#h #o #G #K1 #V #H
+@(csx_ind_cpxs … H) -V #V0 #_ #IHV0 #K2 #H
+@(rdsx_ind … H) -K2 #K0 #HK0 #IHK0 #HK10 #I
+@rdsx_intro #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 rdsx_lfdeq_trans, lpxs_step_dx, lfdeq_pair/
+| @(IHV0 … HnV02) -IHV0 -HnV02
+ [ /2 width=3 by lpxs_cpx_trans/
+ | /3 width=3 by rdsx_lpx_trans, rdsx_cpx_trans/
+ | /2 width=3 by lpxs_step_dx/
+ ]
+]
+qed.
+
+(* Basic_2A1: uses: lsx_lref_be *)
+lemma rdsx_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 rdsx_pair_lpxs/
+| #i #IH #L #H
+ elim (drops_inv_bind2_isuni_next … H) -H // #J #Y #HY #H destruct
+ @(rdsx_lifts … (𝐔❴1❵)) /3 width=6 by drops_refl, drops_drop/ (**) (* full auto fails *)
+]
+qed.
+
+(* Main properties **********************************************************)
+
+(* Basic_2A1: uses: csx_lsx *)
+theorem csx_rdsx (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 rdsx_lref_atom/
+ | /2 width=3 by rdsx_lref_unit/
+ | /4 width=6 by rdsx_lref_pair_drops, fqup_lref/
+ ]
+| #p #I #V #T #HG #HL #HT #H destruct
+ elim (csx_fwd_bind_unit … H Void) -H /3 width=1 by rdsx_bind_void/
+| #I #V #T #HG #HL #HT #H destruct
+ elim (csx_fwd_flat … H) -H /3 width=1 by rdsx_flat/
+]
+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/static/lfdeq_drops.ma".
+include "basic_2/rt_transition/lpx_drops.ma".
+include "basic_2/rt_computation/rdsx_length.ma".
+include "basic_2/rt_computation/rdsx_fqup.ma".
+
+(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
+
+(* Properties with generic relocation ***************************************)
+
+(* Note: this uses length *)
+(* Basic_2A1: uses: lsx_lift_le lsx_lift_ge *)
+lemma rdsx_lifts (h) (o) (G): d_liftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄).
+#h #o #G #K #T #H @(rdsx_ind … H) -K
+#K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @rdsx_intro
+#L2 #HL12 #HnL12 elim (lpx_drops_conf … HLK1 … HL12)
+/5 width=9 by lfdeq_lifts_bi, lpx_fwd_length/
+qed-.
+
+(* Inversion lemmas on relocation *******************************************)
+
+(* Basic_2A1: uses: lsx_inv_lift_le lsx_inv_lift_be lsx_inv_lift_ge *)
+lemma rdsx_inv_lifts (h) (o) (G): d_deliftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄).
+#h #o #G #L #U #H @(rdsx_ind … H) -L
+#L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @rdsx_intro
+#K2 #HK12 #HnK12 elim (drops_lpx_trans … HLK1 … HK12) -HK12
+/4 width=10 by lfdeq_inv_lifts_bi/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lsx_lref_free *)
+lemma rdsx_lref_atom (h) (o) (G): ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+#h #o #G #L1 #i #HL1
+@(rdsx_lifts … (#0) … HL1) -HL1 //
+qed.
+
+(* Basic_2A1: uses: lsx_lref_skip *)
+lemma rdsx_lref_unit (h) (o) (G): ∀I,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+#h #o #G #I #L1 #K1 #i #HL1
+@(rdsx_lifts … (#0) … HL1) -HL1 //
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+(* Basic_2A1: uses: lsx_fwd_lref_be *)
+lemma rdsx_fwd_lref_pair (h) (o) (G):
+ ∀L,i. G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄ →
+ ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄.
+#h #o #G #L #i #HL #I #K #V #HLK
+lapply (rdsx_inv_lifts … HL … HLK … (#0) ?) -L
+/2 width=2 by rdsx_fwd_pair/
+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/static/lfdeq_fqup.ma".
+include "basic_2/rt_computation/rdsx.ma".
+
+(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lsx_atom *)
+lemma lfsx_atom (h) (o) (G) (T): G ⊢ ⬈*[h, o, T] 𝐒⦃⋆⦄.
+#h #o #G #T
+@rdsx_intro #Y #H #HnT
+lapply (lpx_inv_atom_sn … H) -H #H destruct
+elim HnT -HnT //
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+(* Basic_2A1: uses: lsx_fwd_bind_dx *)
+(* Note: the exclusion binder (ⓧ) makes this more elegant and much simpler *)
+(* Note: the old proof without the exclusion binder requires lreq *)
+lemma rdsx_fwd_bind_dx (h) (o) (G):
+ ∀p,I,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ →
+ G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄.
+#h #o #G #p #I #L #V #T #H
+@(rdsx_ind … H) -L #L1 #_ #IH
+@rdsx_intro #Y #H #HT
+elim (lpx_inv_unit_sn … H) -H #L2 #HL12 #H destruct
+/4 width=4 by lfdeq_fwd_bind_dx_void/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_2A1: uses: lsx_inv_bind *)
+lemma rdsx_inv_bind (h) (o) (G): ∀p,I,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ →
+ ∧∧ G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ & G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄.
+/3 width=4 by rdsx_fwd_pair_sn, rdsx_fwd_bind_dx, conj/ 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/static/lfdeq_length.ma".
+include "basic_2/rt_transition/lpx_length.ma".
+include "basic_2/rt_computation/rdsx.ma".
+
+(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lsx_sort *)
+lemma rdsx_sort (h) (o) (G): ∀L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄.
+#h #o #G #L1 #s @rdsx_intro #L2 #H #Hs
+elim Hs -Hs /3 width=3 by lpx_fwd_length, lfdeq_sort_length/
+qed.
+
+(* Basic_2A1: uses: lsx_gref *)
+lemma rdsx_gref (h) (o) (G): ∀L,l. G ⊢ ⬈*[h, o, §l] 𝐒⦃L⦄.
+#h #o #G #L1 #s @rdsx_intro #L2 #H #Hs
+elim Hs -Hs /3 width=3 by lpx_fwd_length, lfdeq_gref_length/
+qed.
+
+lemma rdsx_unit (h) (o) (G): ∀I,L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L.ⓤ{I}⦄.
+#h #o #G #I #L1 @rdsx_intro
+#Y #HY #HnY elim HnY -HnY
+elim (lpx_inv_unit_sn … HY) -HY #L2 #HL12 #H destruct
+/3 width=3 by lpx_fwd_length, lfdeq_unit_length/
+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/rt_computation/lpxs_lfdeq.ma".
+include "basic_2/rt_computation/lpxs_lpx.ma".
+include "basic_2/rt_computation/lpxs_lpxs.ma".
+include "basic_2/rt_computation/rdsx_rdsx.ma".
+
+(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
+
+(* Properties with unbound rt-computation for full local environments *******)
+
+(* Basic_2A1: uses: lsx_intro_alt *)
+lemma rdsx_intro_lpxs (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⦄.
+/4 width=1 by lpx_lpxs, rdsx_intro/ qed-.
+
+(* Basic_2A1: uses: lsx_lpxs_trans *)
+lemma rdsx_lpxs_trans (h) (o) (G): ∀L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
+#h #o #G #L1 #T #HL1 #L2 #H @(lpxs_ind_dx … H) -L2
+/2 width=3 by rdsx_lpx_trans/
+qed-.
+
+(* Eliminators with unbound rt-computation for full local environments ******)
+
+lemma rdsx_ind_lpxs_lfdeq (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
+ ) →
+ ∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[h, o, T] L2 → R L2.
+#h #o #G #T #R #IH #L1 #H @(rdsx_ind … H) -L1
+#L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02
+@IH -IH /3 width=3 by rdsx_lpxs_trans, rdsx_lfdeq_trans/ -HL1 #K2 #HLK2 #HnLK2
+lapply (lfdeq_lfdneq_trans … HL02 … HnLK2) -HnLK2 #H
+elim (lfdeq_lpxs_trans … HLK2 … HL02) -L2 #K0 #HLK0 #HK02
+lapply (lfdneq_lfdeq_canc_dx … H … HK02) -H #HnLK0
+elim (lfdeq_dec h o L1 L0 T) #H
+[ lapply (lfdeq_lfdneq_trans … H … HnLK0) -H -HnLK0 #Hn10
+ lapply (lpxs_trans … HL10 … HLK0) -L0 #H10
+ elim (lpxs_lfdneq_inv_step_sn … H10 … Hn10) -H10 -Hn10
+ /3 width=8 by lfdeq_trans/
+| elim (lpxs_lfdneq_inv_step_sn … HL10 … H) -HL10 -H #L #K #HL1 #HnL1 #HLK #HKL0
+ elim (lfdeq_lpxs_trans … HLK0 … HKL0) -L0
+ /3 width=8 by lpxs_trans, lfdeq_trans/
+]
+qed-.
+
+(* Basic_2A1: uses: lsx_ind_alt *)
+lemma rdsx_ind_lpxs (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.
+#h #o #G #T #R #IH #L #HL
+@(rdsx_ind_lpxs_lfdeq … IH … HL) -IH -HL // (**) (* full auto fails *)
+qed-.
+
+(* Advanced properties ******************************************************)
+
+fact rdsx_bind_lpxs_aux (h) (o) (G):
+ ∀p,I,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
+ ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ →
+ ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
+ G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄.
+#h #o #G #p #I #L1 #V #H @(rdsx_ind_lpxs … H) -L1
+#L1 #_ #IHL1 #Y #T #H @(rdsx_ind_lpxs … H) -Y
+#Y #HY #IHY #L2 #H #HL12 destruct
+@rdsx_intro_lpxs #L0 #HL20
+lapply (lpxs_trans … HL12 … HL20) #HL10 #H
+elim (lfdneq_inv_bind … H) -H [ -IHY | -HY -IHL1 -HL12 ]
+[ #HnV elim (lfdeq_dec h o L1 L2 V)
+ [ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10
+ /3 width=4 by rdsx_lpxs_trans, lpxs_bind_refl_dx, lfdeq_canc_sn/ (**) (* full auto too slow *)
+ | -HnV -HL10 /4 width=4 by rdsx_lpxs_trans, lpxs_bind_refl_dx/
+ ]
+| /3 width=4 by lpxs_bind_refl_dx/
+]
+qed-.
+
+(* Basic_2A1: uses: lsx_bind *)
+lemma rdsx_bind (h) (o) (G):
+ ∀p,I,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ →
+ ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓑ{I}V⦄ →
+ G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄.
+/2 width=3 by rdsx_bind_lpxs_aux/ qed.
+
+(* Basic_2A1: uses: lsx_flat_lpxs *)
+lemma rdsx_flat_lpxs (h) (o) (G):
+ ∀I,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
+ ∀L2,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄ → ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
+ G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L2⦄.
+#h #o #G #I #L1 #V #H @(rdsx_ind_lpxs … H) -L1
+#L1 #HL1 #IHL1 #L2 #T #H @(rdsx_ind_lpxs … H) -L2
+#L2 #HL2 #IHL2 #HL12 @rdsx_intro_lpxs
+#L0 #HL20 lapply (lpxs_trans … HL12 … HL20)
+#HL10 #H elim (lfdneq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ]
+[ #HnV elim (lfdeq_dec h o L1 L2 V)
+ [ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10
+ /3 width=5 by rdsx_lpxs_trans, lfdeq_canc_sn/ (**) (* full auto too slow: 47s *)
+ | -HnV -HL10 /3 width=4 by rdsx_lpxs_trans/
+ ]
+| /3 width=3 by/
+]
+qed-.
+
+(* Basic_2A1: uses: lsx_flat *)
+lemma rdsx_flat (h) (o) (G):
+ ∀I,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ →
+ ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄.
+/2 width=3 by rdsx_flat_lpxs/ qed.
+
+fact rdsx_bind_lpxs_void_aux (h) (o) (G):
+ ∀p,I,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ →
+ ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ →
+ ∀L2. Y = L2.ⓧ → ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
+ G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄.
+#h #o #G #p #I #L1 #V #H @(rdsx_ind_lpxs … H) -L1
+#L1 #_ #IHL1 #Y #T #H @(rdsx_ind_lpxs … H) -Y
+#Y #HY #IHY #L2 #H #HL12 destruct
+@rdsx_intro_lpxs #L0 #HL20
+lapply (lpxs_trans … HL12 … HL20) #HL10 #H
+elim (lfdneq_inv_bind_void … H) -H [ -IHY | -HY -IHL1 -HL12 ]
+[ #HnV elim (lfdeq_dec h o L1 L2 V)
+ [ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10
+ /3 width=6 by rdsx_lpxs_trans, lpxs_bind_refl_dx, lfdeq_canc_sn/ (**) (* full auto too slow *)
+ | -HnV -HL10 /4 width=4 by rdsx_lpxs_trans, lpxs_bind_refl_dx/
+ ]
+| /3 width=4 by lpxs_bind_refl_dx/
+]
+qed-.
+
+lemma rdsx_bind_void (h) (o) (G):
+ ∀p,I,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ →
+ ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄ →
+ G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄.
+/2 width=3 by rdsx_bind_lpxs_void_aux/ 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/rt_transition/lpx_lfdeq.ma".
+include "basic_2/rt_computation/rdsx.ma".
+
+(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lsx_lleq_trans *)
+lemma rdsx_lfdeq_trans (h) (o) (G):
+ ∀L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L2. L1 ≛[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
+#h #o #G #L1 #T #H @(rdsx_ind … H) -L1
+#L1 #_ #IHL1 #L2 #HL12 @rdsx_intro
+#L #HL2 #HnL2 elim (lfdeq_lpx_trans … HL2 … HL12) -HL2
+/4 width=5 by lfdeq_repl/
+qed-.
+
+(* Basic_2A1: uses: lsx_lpx_trans *)
+lemma rdsx_lpx_trans (h) (o) (G):
+ ∀L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
+#h #o #G #L1 #T #H @(rdsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
+elim (lfdeq_dec h o L1 L2 T) /3 width=4 by rdsx_lfdeq_trans/
+qed-.
(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******)
-definition lfdeq: ∀h. sd h → relation3 term lenv lenv ≝
- λh,o. lfxs (cdeq h o).
+definition lfdeq (h) (o): relation3 term lenv lenv ≝
+ lfxs (cdeq h o).
interpretation
"degree-based equivalence on referred entries (local environment)"
(* Basic properties ***********************************************************)
-lemma frees_tdeq_conf_lfdeq: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → ∀T2. T1 ≛[h, o] T2 →
- ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≘ f.
+lemma frees_tdeq_conf_lfdeq (h) (o): ∀f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → ∀T2. T1 ≛[h, o] T2 →
+ ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≘ f.
#h #o #f #L1 #T1 #H elim H -f -L1 -T1
[ #f #L1 #s1 #Hf #X #H1 #L2 #_
elim (tdeq_inv_sort1 … H1) -H1 #s2 #d #_ #_ #H destruct
]
qed-.
-lemma frees_tdeq_conf: ∀h,o,f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≘ f →
- ∀T2. T1 ≛[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≘ f.
+lemma frees_tdeq_conf (h) (o): ∀f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≘ f →
+ ∀T2. T1 ≛[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≘ f.
/4 width=7 by frees_tdeq_conf_lfdeq, lexs_refl, ext2_refl/ qed-.
-lemma frees_lfdeq_conf: ∀h,o,f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≘ f →
- ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≘ f.
+lemma frees_lfdeq_conf (h) (o): ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≘ f →
+ ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≘ f.
/2 width=7 by frees_tdeq_conf_lfdeq, tdeq_refl/ qed-.
-lemma tdeq_lfxs_conf: ∀R,h,o. s_r_confluent1 … (cdeq h o) (lfxs R).
+lemma tdeq_lfxs_conf (R) (h) (o): s_r_confluent1 … (cdeq h o) (lfxs R).
#R #h #o #L1 #T1 #T2 #HT12 #L2 *
/3 width=5 by frees_tdeq_conf, ex2_intro/
qed-.
-lemma tdeq_lfxs_div: ∀R,h,o,T1,T2. T1 ≛[h, o] T2 →
- ∀L1,L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2.
+lemma tdeq_lfxs_div (R) (h) (o): ∀T1,T2. T1 ≛[h, o] T2 →
+ ∀L1,L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2.
/3 width=5 by tdeq_lfxs_conf, tdeq_sym/ qed-.
-lemma tdeq_lfdeq_conf: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o).
+lemma tdeq_lfdeq_conf (h) (o): s_r_confluent1 … (cdeq h o) (lfdeq h o).
/2 width=5 by tdeq_lfxs_conf/ qed-.
-lemma tdeq_lfdeq_div: ∀h,o,T1,T2. T1 ≛[h, o] T2 →
- ∀L1,L2. L1 ≛[h, o, T2] L2 → L1 ≛[h, o, T1] L2.
+lemma tdeq_lfdeq_div (h) (o): ∀T1,T2. T1 ≛[h, o] T2 →
+ ∀L1,L2. L1 ≛[h, o, T2] L2 → L1 ≛[h, o, T1] L2.
/2 width=5 by tdeq_lfxs_div/ qed-.
-lemma lfdeq_atom: ∀h,o,I. ⋆ ≛[h, o, ⓪{I}] ⋆.
+lemma lfdeq_atom (h) (o): ∀I. ⋆ ≛[h, o, ⓪{I}] ⋆.
/2 width=1 by lfxs_atom/ qed.
-(* Basic_2A1: uses: lleq_sort *)
-lemma lfdeq_sort: ∀h,o,I1,I2,L1,L2,s.
- L1 ≛[h, o, ⋆s] L2 → L1.ⓘ{I1} ≛[h, o, ⋆s] L2.ⓘ{I2}.
+lemma lfdeq_sort (h) (o): ∀I1,I2,L1,L2,s.
+ L1 ≛[h, o, ⋆s] L2 → L1.ⓘ{I1} ≛[h, o, ⋆s] L2.ⓘ{I2}.
/2 width=1 by lfxs_sort/ qed.
-lemma lfdeq_pair: ∀h,o,I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 → V1 ≛[h, o] V2 →
- L1.ⓑ{I}V1 ≛[h, o, #0] L2.ⓑ{I}V2.
+lemma lfdeq_pair (h) (o): ∀I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 → V1 ≛[h, o] V2 →
+ L1.ⓑ{I}V1 ≛[h, o, #0] L2.ⓑ{I}V2.
/2 width=1 by lfxs_pair/ qed.
(*
-lemma lfdeq_unit: ∀h,o,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cdeq_ext h o, cfull, f] L2 →
- L1.ⓤ{I} ≛[h, o, #0] L2.ⓤ{I}.
+lemma lfdeq_unit (h) (o): ∀f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cdeq_ext h o, cfull, f] L2 →
+ L1.ⓤ{I} ≛[h, o, #0] L2.ⓤ{I}.
/2 width=3 by lfxs_unit/ qed.
*)
-lemma lfdeq_lref: ∀h,o,I1,I2,L1,L2,i.
- L1 ≛[h, o, #i] L2 → L1.ⓘ{I1} ≛[h, o, #↑i] L2.ⓘ{I2}.
+lemma lfdeq_lref (h) (o): ∀I1,I2,L1,L2,i.
+ L1 ≛[h, o, #i] L2 → L1.ⓘ{I1} ≛[h, o, #↑i] L2.ⓘ{I2}.
/2 width=1 by lfxs_lref/ qed.
-(* Basic_2A1: uses: lleq_gref *)
-lemma lfdeq_gref: ∀h,o,I1,I2,L1,L2,l.
- L1 ≛[h, o, §l] L2 → L1.ⓘ{I1} ≛[h, o, §l] L2.ⓘ{I2}.
+lemma lfdeq_gref (h) (o): ∀I1,I2,L1,L2,l.
+ L1 ≛[h, o, §l] L2 → L1.ⓘ{I1} ≛[h, o, §l] L2.ⓘ{I2}.
/2 width=1 by lfxs_gref/ qed.
-lemma lfdeq_bind_repl_dx: ∀h,o,I,I1,L1,L2.∀T:term.
- L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I1} →
- ∀I2. I ≛[h, o] I2 →
- L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I2}.
+lemma lfdeq_bind_repl_dx (h) (o): ∀I,I1,L1,L2.∀T:term.
+ L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I1} →
+ ∀I2. I ≛[h, o] I2 →
+ L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I2}.
/2 width=2 by lfxs_bind_repl_dx/ qed-.
(* Basic inversion lemmas ***************************************************)
-lemma lfdeq_inv_atom_sn: ∀h,o,Y2. ∀T:term. ⋆ ≛[h, o, T] Y2 → Y2 = ⋆.
+lemma lfdeq_inv_atom_sn (h) (o): ∀Y2. ∀T:term. ⋆ ≛[h, o, T] Y2 → Y2 = ⋆.
/2 width=3 by lfxs_inv_atom_sn/ qed-.
-lemma lfdeq_inv_atom_dx: ∀h,o,Y1. ∀T:term. Y1 ≛[h, o, T] ⋆ → Y1 = ⋆.
+lemma lfdeq_inv_atom_dx (h) (o): ∀Y1. ∀T:term. Y1 ≛[h, o, T] ⋆ → Y1 = ⋆.
/2 width=3 by lfxs_inv_atom_dx/ qed-.
(*
-lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≛[h, o, #0] Y2 →
- ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
- | ∃∃I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
- | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤*[cdeq_ext h o, cfull, f] L2 &
- Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
+lemma lfdeq_inv_zero (h) (o): ∀Y1,Y2. Y1 ≛[h, o, #0] Y2 →
+ ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
+ | ∃∃I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
+ | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤*[cdeq_ext h o, cfull, f] L2 &
+ Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
#h #o #Y1 #Y2 #H elim (lfxs_inv_zero … H) -H *
/3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/
qed-.
*)
-lemma lfdeq_inv_lref: ∀h,o,Y1,Y2,i. Y1 ≛[h, o, #↑i] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
- ∃∃I1,I2,L1,L2. L1 ≛[h, o, #i] L2 &
- Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
+lemma lfdeq_inv_lref (h) (o): ∀Y1,Y2,i. Y1 ≛[h, o, #↑i] Y2 →
+ ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
+ | ∃∃I1,I2,L1,L2. L1 ≛[h, o, #i] L2 &
+ Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
/2 width=1 by lfxs_inv_lref/ qed-.
(* Basic_2A1: uses: lleq_inv_bind lleq_inv_bind_O *)
-lemma lfdeq_inv_bind: ∀h,o,p,I,L1,L2,V,T. L1 ≛[h, o, ⓑ{p,I}V.T] L2 →
- L1 ≛[h, o, V] L2 ∧ L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V.
+lemma lfdeq_inv_bind (h) (o): ∀p,I,L1,L2,V,T. L1 ≛[h, o, ⓑ{p,I}V.T] L2 →
+ ∧∧ L1 ≛[h, o, V] L2 & L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V.
/2 width=2 by lfxs_inv_bind/ qed-.
(* Basic_2A1: uses: lleq_inv_flat *)
-lemma lfdeq_inv_flat: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 →
- L1 ≛[h, o, V] L2 ∧ L1 ≛[h, o, T] L2.
+lemma lfdeq_inv_flat (h) (o): ∀I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 →
+ ∧∧ L1 ≛[h, o, V] L2 & L1 ≛[h, o, T] L2.
/2 width=2 by lfxs_inv_flat/ qed-.
(* Advanced inversion lemmas ************************************************)
-lemma lfdeq_inv_zero_pair_sn: ∀h,o,I,Y2,L1,V1. L1.ⓑ{I}V1 ≛[h, o, #0] Y2 →
- ∃∃L2,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y2 = L2.ⓑ{I}V2.
+lemma lfdeq_inv_zero_pair_sn (h) (o): ∀I,Y2,L1,V1. L1.ⓑ{I}V1 ≛[h, o, #0] Y2 →
+ ∃∃L2,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y2 = L2.ⓑ{I}V2.
/2 width=1 by lfxs_inv_zero_pair_sn/ qed-.
-lemma lfdeq_inv_zero_pair_dx: ∀h,o,I,Y1,L2,V2. Y1 ≛[h, o, #0] L2.ⓑ{I}V2 →
- ∃∃L1,V1. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y1 = L1.ⓑ{I}V1.
+lemma lfdeq_inv_zero_pair_dx (h) (o): ∀I,Y1,L2,V2. Y1 ≛[h, o, #0] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y1 = L1.ⓑ{I}V1.
/2 width=1 by lfxs_inv_zero_pair_dx/ qed-.
-lemma lfdeq_inv_lref_bind_sn: ∀h,o,I1,Y2,L1,i. L1.ⓘ{I1} ≛[h, o, #↑i] Y2 →
- ∃∃I2,L2. L1 ≛[h, o, #i] L2 & Y2 = L2.ⓘ{I2}.
+lemma lfdeq_inv_lref_bind_sn (h) (o): ∀I1,Y2,L1,i. L1.ⓘ{I1} ≛[h, o, #↑i] Y2 →
+ ∃∃I2,L2. L1 ≛[h, o, #i] L2 & Y2 = L2.ⓘ{I2}.
/2 width=2 by lfxs_inv_lref_bind_sn/ qed-.
-lemma lfdeq_inv_lref_bind_dx: ∀h,o,I2,Y1,L2,i. Y1 ≛[h, o, #↑i] L2.ⓘ{I2} →
- ∃∃I1,L1. L1 ≛[h, o, #i] L2 & Y1 = L1.ⓘ{I1}.
+lemma lfdeq_inv_lref_bind_dx (h) (o): ∀I2,Y1,L2,i. Y1 ≛[h, o, #↑i] L2.ⓘ{I2} →
+ ∃∃I1,L1. L1 ≛[h, o, #i] L2 & Y1 = L1.ⓘ{I1}.
/2 width=2 by lfxs_inv_lref_bind_dx/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma lfdeq_fwd_zero_pair: ∀h,o,I,K1,K2,V1,V2.
- K1.ⓑ{I}V1 ≛[h, o, #0] K2.ⓑ{I}V2 → K1 ≛[h, o, V1] K2.
+lemma lfdeq_fwd_zero_pair (h) (o): ∀I,K1,K2,V1,V2.
+ K1.ⓑ{I}V1 ≛[h, o, #0] K2.ⓑ{I}V2 → K1 ≛[h, o, V1] K2.
/2 width=3 by lfxs_fwd_zero_pair/ qed-.
(* Basic_2A1: uses: lleq_fwd_bind_sn lleq_fwd_flat_sn *)
-lemma lfdeq_fwd_pair_sn: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ②{I}V.T] L2 → L1 ≛[h, o, V] L2.
+lemma lfdeq_fwd_pair_sn (h) (o): ∀I,L1,L2,V,T. L1 ≛[h, o, ②{I}V.T] L2 → L1 ≛[h, o, V] L2.
/2 width=3 by lfxs_fwd_pair_sn/ qed-.
(* Basic_2A1: uses: lleq_fwd_bind_dx lleq_fwd_bind_O_dx *)
-lemma lfdeq_fwd_bind_dx: ∀h,o,p,I,L1,L2,V,T.
- L1 ≛[h, o, ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V.
+lemma lfdeq_fwd_bind_dx (h) (o): ∀p,I,L1,L2,V,T.
+ L1 ≛[h, o, ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V.
/2 width=2 by lfxs_fwd_bind_dx/ qed-.
(* Basic_2A1: uses: lleq_fwd_flat_dx *)
-lemma lfdeq_fwd_flat_dx: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → L1 ≛[h, o, T] L2.
+lemma lfdeq_fwd_flat_dx (h) (o): ∀I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → L1 ≛[h, o, T] L2.
/2 width=3 by lfxs_fwd_flat_dx/ qed-.
-lemma lfdeq_fwd_dx: ∀h,o,I2,L1,K2. ∀T:term. L1 ≛[h, o, T] K2.ⓘ{I2} →
- ∃∃I1,K1. L1 = K1.ⓘ{I1}.
+lemma lfdeq_fwd_dx (h) (o): ∀I2,L1,K2. ∀T:term. L1 ≛[h, o, T] K2.ⓘ{I2} →
+ ∃∃I1,K1. L1 = K1.ⓘ{I1}.
/2 width=5 by lfxs_fwd_dx/ qed-.
(* Advanved properties with free variables inclusion ************************)
-lemma lfdeq_fsge_comp: ∀h,o. lfxs_fsge_compatible (cdeq h o).
+lemma lfdeq_fsge_comp (h) (o): lfxs_fsge_compatible (cdeq h o).
#h #o #L1 #L2 #T * #f1 #Hf1 #HL12
lapply (frees_lfdeq_conf h o … Hf1 … HL12)
lapply (lexs_fwd_length … HL12)
(* Properties with length for local environments ****************************)
+(* Basic_2A1: uses: lleq_sort *)
+lemma lfdeq_sort_length (h) (o): ∀L1,L2. |L1| = |L2| → ∀s. L1 ≛[h, o, ⋆s] L2.
+/2 width=1 by lfxs_sort_length/ qed.
+
+(* Basic_2A1: uses: lleq_gref *)
+lemma lfdeq_gref_length (h) (o): ∀L1,L2. |L1| = |L2| → ∀l. L1 ≛[h, o, §l] L2.
+/2 width=1 by lfxs_gref_length/ qed.
+
+lemma lfdeq_unit_length (h) (o): ∀L1,L2. |L1| = |L2| →
+ ∀I. L1.ⓤ{I} ≛[h, o, #0] L2.ⓤ{I}.
+/2 width=1 by lfxs_unit_length/ qed.
+
(* Basic_2A1: uses: lleq_lift_le lleq_lift_ge *)
-lemma lfdeq_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀h,o,K1,K2,T. K1 ≛[h, o, T] K2 →
- ∀b,f. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 →
- ∀U. ⬆*[f] T ≘ U → L1 ≛[h, o, U] L2.
+lemma lfdeq_lifts_bi (h) (o): ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ≛[h, o, T] K2 →
+ ∀b,f. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 →
+ ∀U. ⬆*[f] T ≘ U → L1 ≛[h, o, U] L2.
/3 width=9 by lfxs_lifts_bi, tdeq_lifts_sn/ qed-.
(* Forward lemmas with length for local environments ************************)
(* Basic_2A1: lleq_fwd_length *)
-lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≛[h, o, T] L2 → |L1| = |L2|.
+lemma lfdeq_fwd_length (h) (o): ∀L1,L2. ∀T:term. L1 ≛[h, o, T] L2 → |L1| = |L2|.
/2 width=3 by lfxs_fwd_length/ qed-.
-
(* Basic inversion lemmas ***************************************************)
-lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⪤*[R, T] Y2 → Y2 = ⋆.
+lemma lfxs_inv_atom_sn (R): ∀Y2,T. ⋆ ⪤*[R, T] Y2 → Y2 = ⋆.
#R #Y2 #T * /2 width=4 by lexs_inv_atom1/
qed-.
-lemma lfxs_inv_atom_dx: ∀R,Y1,T. Y1 ⪤*[R, T] ⋆ → Y1 = ⋆.
+lemma lfxs_inv_atom_dx (R): ∀Y1,T. Y1 ⪤*[R, T] ⋆ → Y1 = ⋆.
#R #I #Y1 * /2 width=4 by lexs_inv_atom2/
qed-.
-lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⪤*[R, ⋆s] Y2 →
- ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
- | ∃∃I1,I2,L1,L2. L1 ⪤*[R, ⋆s] L2 &
- Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
+lemma lfxs_inv_sort (R): ∀Y1,Y2,s. Y1 ⪤*[R, ⋆s] Y2 →
+ ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
+ | ∃∃I1,I2,L1,L2. L1 ⪤*[R, ⋆s] L2 &
+ Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
#R * [ | #Y1 #I1 ] #Y2 #s * #f #H1 #H2
[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
| lapply (frees_inv_sort … H1) -H1 #Hf
]
qed-.
-lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⪤*[R, #0] Y2 →
- ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
- | ∃∃I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 & R L1 V1 V2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
- | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤*[cext2 R, cfull, f] L2 &
- Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
+lemma lfxs_inv_zero (R): ∀Y1,Y2. Y1 ⪤*[R, #0] Y2 →
+ ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
+ | ∃∃I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 & R L1 V1 V2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
+ | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤*[cext2 R, cfull, f] L2 &
+ Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
#R * [ | #Y1 * #I1 [ | #X ] ] #Y2 * #f #H1 #H2
[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or3_intro0, conj/
| elim (frees_inv_unit … H1) -H1 #g #HX #H destruct
]
qed-.
-lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⪤*[R, #↑i] Y2 →
- ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
- | ∃∃I1,I2,L1,L2. L1 ⪤*[R, #i] L2 &
- Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
+lemma lfxs_inv_lref (R): ∀Y1,Y2,i. Y1 ⪤*[R, #↑i] Y2 →
+ ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
+ | ∃∃I1,I2,L1,L2. L1 ⪤*[R, #i] L2 &
+ Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
#R * [ | #Y1 #I1 ] #Y2 #i * #f #H1 #H2
[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
| elim (frees_inv_lref … H1) -H1 #g #Hg #H destruct
]
qed-.
-lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⪤*[R, §l] Y2 →
- ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
- | ∃∃I1,I2,L1,L2. L1 ⪤*[R, §l] L2 &
- Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
+lemma lfxs_inv_gref (R): ∀Y1,Y2,l. Y1 ⪤*[R, §l] Y2 →
+ ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
+ | ∃∃I1,I2,L1,L2. L1 ⪤*[R, §l] L2 &
+ Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
#R * [ | #Y1 #I1 ] #Y2 #l * #f #H1 #H2
[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
| lapply (frees_inv_gref … H1) -H1 #Hf
qed-.
(* Basic_2A1: uses: llpx_sn_inv_bind llpx_sn_inv_bind_O *)
-lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⪤*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 →
- L1 ⪤*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⪤*[R, T] L2.ⓑ{I}V2.
+lemma lfxs_inv_bind (R): ∀p,I,L1,L2,V1,V2,T. L1 ⪤*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 →
+ ∧∧ L1 ⪤*[R, V1] L2 & L1.ⓑ{I}V1 ⪤*[R, T] L2.ⓑ{I}V2.
#R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf
/6 width=6 by sle_lexs_trans, lexs_inv_tl, ext2_pair, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/
qed-.
(* Basic_2A1: uses: llpx_sn_inv_flat *)
-lemma lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⪤*[R, ⓕ{I}V.T] L2 →
- L1 ⪤*[R, V] L2 ∧ L1 ⪤*[R, T] L2.
+lemma lfxs_inv_flat (R): ∀I,L1,L2,V,T. L1 ⪤*[R, ⓕ{I}V.T] L2 →
+ ∧∧ L1 ⪤*[R, V] L2 & L1 ⪤*[R, T] L2.
#R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf
/5 width=6 by sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/
qed-.
(* Advanced inversion lemmas ************************************************)
-lemma lfxs_inv_sort_bind_sn: ∀R,I1,K1,L2,s. K1.ⓘ{I1} ⪤*[R, ⋆s] L2 →
- ∃∃I2,K2. K1 ⪤*[R, ⋆s] K2 & L2 = K2.ⓘ{I2}.
+lemma lfxs_inv_sort_bind_sn (R): ∀I1,K1,L2,s. K1.ⓘ{I1} ⪤*[R, ⋆s] L2 →
+ ∃∃I2,K2. K1 ⪤*[R, ⋆s] K2 & L2 = K2.ⓘ{I2}.
#R #I1 #K1 #L2 #s #H elim (lfxs_inv_sort … H) -H *
[ #H destruct
| #Z1 #I2 #Y1 #K2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
]
qed-.
-lemma lfxs_inv_sort_bind_dx: ∀R,I2,K2,L1,s. L1 ⪤*[R, ⋆s] K2.ⓘ{I2} →
- ∃∃I1,K1. K1 ⪤*[R, ⋆s] K2 & L1 = K1.ⓘ{I1}.
+lemma lfxs_inv_sort_bind_dx (R): ∀I2,K2,L1,s. L1 ⪤*[R, ⋆s] K2.ⓘ{I2} →
+ ∃∃I1,K1. K1 ⪤*[R, ⋆s] K2 & L1 = K1.ⓘ{I1}.
#R #I2 #K2 #L1 #s #H elim (lfxs_inv_sort … H) -H *
[ #_ #H destruct
| #I1 #Z2 #K1 #Y2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
]
qed-.
-lemma lfxs_inv_zero_pair_sn: ∀R,I,L2,K1,V1. K1.ⓑ{I}V1 ⪤*[R, #0] L2 →
- ∃∃K2,V2. K1 ⪤*[R, V1] K2 & R K1 V1 V2 &
- L2 = K2.ⓑ{I}V2.
+lemma lfxs_inv_zero_pair_sn (R): ∀I,L2,K1,V1. K1.ⓑ{I}V1 ⪤*[R, #0] L2 →
+ ∃∃K2,V2. K1 ⪤*[R, V1] K2 & R K1 V1 V2 &
+ L2 = K2.ⓑ{I}V2.
#R #I #L2 #K1 #V1 #H elim (lfxs_inv_zero … H) -H *
[ #H destruct
| #Z #Y1 #K2 #X1 #V2 #HK12 #HV12 #H1 #H2 destruct
]
qed-.
-lemma lfxs_inv_zero_pair_dx: ∀R,I,L1,K2,V2. L1 ⪤*[R, #0] K2.ⓑ{I}V2 →
- ∃∃K1,V1. K1 ⪤*[R, V1] K2 & R K1 V1 V2 &
- L1 = K1.ⓑ{I}V1.
+lemma lfxs_inv_zero_pair_dx (R): ∀I,L1,K2,V2. L1 ⪤*[R, #0] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. K1 ⪤*[R, V1] K2 & R K1 V1 V2 &
+ L1 = K1.ⓑ{I}V1.
#R #I #L1 #K2 #V2 #H elim (lfxs_inv_zero … H) -H *
[ #_ #H destruct
| #Z #K1 #Y2 #V1 #X2 #HK12 #HV12 #H1 #H2 destruct
]
qed-.
-lemma lfxs_inv_zero_unit_sn: ∀R,I,K1,L2. K1.ⓤ{I} ⪤*[R, #0] L2 →
- ∃∃f,K2. 𝐈⦃f⦄ & K1 ⪤*[cext2 R, cfull, f] K2 &
- L2 = K2.ⓤ{I}.
+lemma lfxs_inv_zero_unit_sn (R): ∀I,K1,L2. K1.ⓤ{I} ⪤*[R, #0] L2 →
+ ∃∃f,K2. 𝐈⦃f⦄ & K1 ⪤*[cext2 R, cfull, f] K2 &
+ L2 = K2.ⓤ{I}.
#R #I #K1 #L2 #H elim (lfxs_inv_zero … H) -H *
[ #H destruct
| #Z #Y1 #Y2 #X1 #X2 #_ #_ #H destruct
]
qed-.
-lemma lfxs_inv_zero_unit_dx: ∀R,I,L1,K2. L1 ⪤*[R, #0] K2.ⓤ{I} →
- ∃∃f,K1. 𝐈⦃f⦄ & K1 ⪤*[cext2 R, cfull, f] K2 &
- L1 = K1.ⓤ{I}.
+lemma lfxs_inv_zero_unit_dx (R): ∀I,L1,K2. L1 ⪤*[R, #0] K2.ⓤ{I} →
+ ∃∃f,K1. 𝐈⦃f⦄ & K1 ⪤*[cext2 R, cfull, f] K2 &
+ L1 = K1.ⓤ{I}.
#R #I #L1 #K2 #H elim (lfxs_inv_zero … H) -H *
[ #_ #H destruct
| #Z #Y1 #Y2 #X1 #X2 #_ #_ #_ #H destruct
]
qed-.
-lemma lfxs_inv_lref_bind_sn: ∀R,I1,K1,L2,i. K1.ⓘ{I1} ⪤*[R, #↑i] L2 →
- ∃∃I2,K2. K1 ⪤*[R, #i] K2 & L2 = K2.ⓘ{I2}.
+lemma lfxs_inv_lref_bind_sn (R): ∀I1,K1,L2,i. K1.ⓘ{I1} ⪤*[R, #↑i] L2 →
+ ∃∃I2,K2. K1 ⪤*[R, #i] K2 & L2 = K2.ⓘ{I2}.
#R #I1 #K1 #L2 #i #H elim (lfxs_inv_lref … H) -H *
[ #H destruct
| #Z1 #I2 #Y1 #K2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/
]
qed-.
-lemma lfxs_inv_lref_bind_dx: ∀R,I2,K2,L1,i. L1 ⪤*[R, #↑i] K2.ⓘ{I2} →
- ∃∃I1,K1. K1 ⪤*[R, #i] K2 & L1 = K1.ⓘ{I1}.
+lemma lfxs_inv_lref_bind_dx (R): ∀I2,K2,L1,i. L1 ⪤*[R, #↑i] K2.ⓘ{I2} →
+ ∃∃I1,K1. K1 ⪤*[R, #i] K2 & L1 = K1.ⓘ{I1}.
#R #I2 #K2 #L1 #i #H elim (lfxs_inv_lref … H) -H *
[ #_ #H destruct
| #I1 #Z2 #K1 #Y2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/
]
qed-.
-lemma lfxs_inv_gref_bind_sn: ∀R,I1,K1,L2,l. K1.ⓘ{I1} ⪤*[R, §l] L2 →
- ∃∃I2,K2. K1 ⪤*[R, §l] K2 & L2 = K2.ⓘ{I2}.
+lemma lfxs_inv_gref_bind_sn (R): ∀I1,K1,L2,l. K1.ⓘ{I1} ⪤*[R, §l] L2 →
+ ∃∃I2,K2. K1 ⪤*[R, §l] K2 & L2 = K2.ⓘ{I2}.
#R #I1 #K1 #L2 #l #H elim (lfxs_inv_gref … H) -H *
[ #H destruct
| #Z1 #I2 #Y1 #K2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
]
qed-.
-lemma lfxs_inv_gref_bind_dx: ∀R,I2,K2,L1,l. L1 ⪤*[R, §l] K2.ⓘ{I2} →
- ∃∃I1,K1. K1 ⪤*[R, §l] K2 & L1 = K1.ⓘ{I1}.
+lemma lfxs_inv_gref_bind_dx (R): ∀I2,K2,L1,l. L1 ⪤*[R, §l] K2.ⓘ{I2} →
+ ∃∃I1,K1. K1 ⪤*[R, §l] K2 & L1 = K1.ⓘ{I1}.
#R #I2 #K2 #L1 #l #H elim (lfxs_inv_gref … H) -H *
[ #_ #H destruct
| #I1 #Z2 #K1 #Y2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
(* Basic forward lemmas *****************************************************)
-lemma lfxs_fwd_zero_pair: ∀R,I,K1,K2,V1,V2.
- K1.ⓑ{I}V1 ⪤*[R, #0] K2.ⓑ{I}V2 → K1 ⪤*[R, V1] K2.
+lemma lfxs_fwd_zero_pair (R): ∀I,K1,K2,V1,V2.
+ K1.ⓑ{I}V1 ⪤*[R, #0] K2.ⓑ{I}V2 → K1 ⪤*[R, V1] K2.
#R #I #K1 #K2 #V1 #V2 #H
elim (lfxs_inv_zero_pair_sn … H) -H #Y #X #HK12 #_ #H destruct //
qed-.
(* Basic_2A1: uses: llpx_sn_fwd_pair_sn llpx_sn_fwd_bind_sn llpx_sn_fwd_flat_sn *)
-lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⪤*[R, ②{I}V.T] L2 → L1 ⪤*[R, V] L2.
+lemma lfxs_fwd_pair_sn (R): ∀I,L1,L2,V,T. L1 ⪤*[R, ②{I}V.T] L2 → L1 ⪤*[R, V] L2.
#R * [ #p ] #I #L1 #L2 #V #T * #f #Hf #HL
[ elim (frees_inv_bind … Hf) | elim (frees_inv_flat … Hf) ] -Hf
/4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/
qed-.
(* Basic_2A1: uses: llpx_sn_fwd_bind_dx llpx_sn_fwd_bind_O_dx *)
-lemma lfxs_fwd_bind_dx: ∀R,p,I,L1,L2,V1,V2,T. L1 ⪤*[R, ⓑ{p,I}V1.T] L2 →
- R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, T] L2.ⓑ{I}V2.
+lemma lfxs_fwd_bind_dx (R): ∀p,I,L1,L2,V1,V2,T. L1 ⪤*[R, ⓑ{p,I}V1.T] L2 →
+ R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, T] L2.ⓑ{I}V2.
#R #p #I #L1 #L2 #V1 #V2 #T #H #HV elim (lfxs_inv_bind … H HV) -H -HV //
qed-.
(* Basic_2A1: uses: llpx_sn_fwd_flat_dx *)
-lemma lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⪤*[R, ⓕ{I}V.T] L2 → L1 ⪤*[R, T] L2.
+lemma lfxs_fwd_flat_dx (R): ∀I,L1,L2,V,T. L1 ⪤*[R, ⓕ{I}V.T] L2 → L1 ⪤*[R, T] L2.
#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H //
qed-.
-lemma lfxs_fwd_dx: ∀R,I2,L1,K2,T. L1 ⪤*[R, T] K2.ⓘ{I2} →
- ∃∃I1,K1. L1 = K1.ⓘ{I1}.
+lemma lfxs_fwd_dx (R): ∀I2,L1,K2,T. L1 ⪤*[R, T] K2.ⓘ{I2} →
+ ∃∃I1,K1. L1 = K1.ⓘ{I1}.
#R #I2 #L1 #K2 #T * #f elim (pn_split f) * #g #Hg #_ #Hf destruct
[ elim (lexs_inv_push2 … Hf) | elim (lexs_inv_next2 … Hf) ] -Hf #I1 #K1 #_ #_ #H destruct
/2 width=3 by ex1_2_intro/
(* Basic properties *********************************************************)
-lemma lfxs_atom: ∀R,I. ⋆ ⪤*[R, ⓪{I}] ⋆.
+lemma lfxs_atom (R): ∀I. ⋆ ⪤*[R, ⓪{I}] ⋆.
#R * /3 width=3 by frees_sort, frees_atom, frees_gref, lexs_atom, ex2_intro/
qed.
-(* Basic_2A1: uses: llpx_sn_sort *)
-lemma lfxs_sort: ∀R,I1,I2,L1,L2,s.
- L1 ⪤*[R, ⋆s] L2 → L1.ⓘ{I1} ⪤*[R, ⋆s] L2.ⓘ{I2}.
+lemma lfxs_sort (R): ∀I1,I2,L1,L2,s.
+ L1 ⪤*[R, ⋆s] L2 → L1.ⓘ{I1} ⪤*[R, ⋆s] L2.ⓘ{I2}.
#R #I1 #I2 #L1 #L2 #s * #f #Hf #H12
lapply (frees_inv_sort … Hf) -Hf
/4 width=3 by frees_sort, lexs_push, isid_push, ex2_intro/
qed.
-lemma lfxs_pair: ∀R,I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 →
- R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, #0] L2.ⓑ{I}V2.
+lemma lfxs_pair (R): ∀I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 →
+ R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, #0] L2.ⓑ{I}V2.
#R #I1 #I2 #L1 #L2 #V1 *
/4 width=3 by ext2_pair, frees_pair, lexs_next, ex2_intro/
qed.
-lemma lfxs_unit: ∀R,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2 →
- L1.ⓤ{I} ⪤*[R, #0] L2.ⓤ{I}.
+lemma lfxs_unit (R): ∀f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2 →
+ L1.ⓤ{I} ⪤*[R, #0] L2.ⓤ{I}.
/4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed.
-lemma lfxs_lref: ∀R,I1,I2,L1,L2,i.
+lemma lfxs_lref (R): ∀I1,I2,L1,L2,i.
L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #↑i] L2.ⓘ{I2}.
#R #I1 #I2 #L1 #L2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/
qed.
-(* Basic_2A1: uses: llpx_sn_gref *)
-lemma lfxs_gref: ∀R,I1,I2,L1,L2,l.
- L1 ⪤*[R, §l] L2 → L1.ⓘ{I1} ⪤*[R, §l] L2.ⓘ{I2}.
+lemma lfxs_gref (R): ∀I1,I2,L1,L2,l.
+ L1 ⪤*[R, §l] L2 → L1.ⓘ{I1} ⪤*[R, §l] L2.ⓘ{I2}.
#R #I1 #I2 #L1 #L2 #l * #f #Hf #H12
lapply (frees_inv_gref … Hf) -Hf
/4 width=3 by frees_gref, lexs_push, isid_push, ex2_intro/
qed.
-lemma lfxs_bind_repl_dx: ∀R,I,I1,L1,L2,T.
- L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I1} →
- ∀I2. cext2 R L1 I I2 →
- L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I2}.
+lemma lfxs_bind_repl_dx (R): ∀I,I1,L1,L2,T.
+ L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I1} →
+ ∀I2. cext2 R L1 I I2 →
+ L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I2}.
#R #I #I1 #L1 #L2 #T * #f #Hf #HL12 #I2 #HR
/3 width=5 by lexs_pair_repl, ex2_intro/
qed-.
(* Basic_2A1: uses: llpx_sn_co *)
-lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
- ∀L1,L2,T. L1 ⪤*[R1, T] L2 → L1 ⪤*[R2, T] L2.
+lemma lfxs_co (R1) (R2): (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
+ ∀L1,L2,T. L1 ⪤*[R1, T] L2 → L1 ⪤*[R2, T] L2.
#R1 #R2 #HR #L1 #L2 #T * /5 width=7 by lexs_co, cext2_co, ex2_intro/
qed-.
-lemma lfxs_isid: ∀R1,R2,L1,L2,T1,T2.
- (∀f. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → 𝐈⦃f⦄) →
- (∀f. 𝐈⦃f⦄ → L1 ⊢ 𝐅*⦃T2⦄ ≘ f) →
- L1 ⪤*[R1, T1] L2 → L1 ⪤*[R2, T2] L2.
+lemma lfxs_isid (R1) (R2): ∀L1,L2,T1,T2.
+ (∀f. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → 𝐈⦃f⦄) →
+ (∀f. 𝐈⦃f⦄ → L1 ⊢ 𝐅*⦃T2⦄ ≘ f) →
+ L1 ⪤*[R1, T1] L2 → L1 ⪤*[R2, T2] L2.
#R1 #R2 #L1 #L2 #T1 #T2 #H1 #H2 *
/4 width=7 by lexs_co_isid, ex2_intro/
qed-.
-lemma lfxs_unit_sn: ∀R1,R2,I,K1,L2.
- K1.ⓤ{I} ⪤*[R1, #0] L2 → K1.ⓤ{I} ⪤*[R2, #0] L2.
+lemma lfxs_unit_sn (R1) (R2):
+ ∀I,K1,L2. K1.ⓤ{I} ⪤*[R1, #0] L2 → K1.ⓤ{I} ⪤*[R2, #0] L2.
#R1 #R2 #I #K1 #L2 #H
elim (lfxs_inv_zero_unit_sn … H) -H #f #K2 #Hf #HK12 #H destruct
/3 width=7 by lfxs_unit, lexs_co_isid/
(* Forward lemmas with length for local environments ************************)
(* Basic_2A1: uses: llpx_sn_fwd_length *)
-lemma lfxs_fwd_length: ∀R,L1,L2,T. L1 ⪤*[R, T] L2 → |L1| = |L2|.
+lemma lfxs_fwd_length (R): ∀L1,L2,T. L1 ⪤*[R, T] L2 → |L1| = |L2|.
#R #L1 #L2 #T * /2 width=4 by lexs_fwd_length/
qed-.
(* Properties with length for local environments ****************************)
+(* Basic_2A1: uses: llpx_sn_sort *)
+lemma lfxs_sort_length (R): ∀L1,L2. |L1| = |L2| → ∀s. L1 ⪤*[R, ⋆s] L2.
+#R #L1 elim L1 -L1
+[ #Y #H #s >(length_inv_zero_sn … H) -H //
+| #K1 #I1 #IH #Y #H #s
+ elim (length_inv_succ_sn … H) -H #I2 #K2 #HK12 #H destruct
+ /3 width=1 by lfxs_sort/
+]
+qed.
+
+(* Basic_2A1: uses: llpx_sn_gref *)
+lemma lfxs_gref_length (R): ∀L1,L2. |L1| = |L2| → ∀l. L1 ⪤*[R, §l] L2.
+#R #L1 elim L1 -L1
+[ #Y #H #s >(length_inv_zero_sn … H) -H //
+| #K1 #I1 #IH #Y #H #s
+ elim (length_inv_succ_sn … H) -H #I2 #K2 #HK12 #H destruct
+ /3 width=1 by lfxs_gref/
+]
+qed.
+
+lemma lfxs_unit_length (R): ∀L1,L2. |L1| = |L2| → ∀I. L1.ⓤ{I} ⪤*[R, #0] L2.ⓤ{I}.
+/3 width=3 by lfxs_unit, lexs_length_isid/ qed.
+
(* Basic_2A1: uses: llpx_sn_lift_le llpx_sn_lift_ge *)
-lemma lfxs_lifts_bi: ∀R.d_liftable2_sn … lifts R →
- ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ⪤*[R, T] K2 →
- ∀b,f. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 →
- ∀U. ⬆*[f] T ≘ U → L1 ⪤*[R, U] L2.
+lemma lfxs_lifts_bi (R): d_liftable2_sn … lifts R →
+ ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ⪤*[R, T] K2 →
+ ∀b,f. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 →
+ ∀U. ⬆*[f] T ≘ U → L1 ⪤*[R, U] L2.
#R #HR #L1 #L2 #HL12 #K1 #K2 #T * #f1 #Hf1 #HK12 #b #f #HLK1 #HLK2 #U #HTU
elim (frees_total L1 U) #f2 #Hf2
lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf
(* Inversion lemmas with length for local environment ***********************)
-lemma lfxs_inv_zero_length: ∀R,Y1,Y2. Y1 ⪤*[R, #0] Y2 →
- ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
- | ∃∃I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 & R L1 V1 V2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
- | ∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
+lemma lfxs_inv_zero_length (R): ∀Y1,Y2. Y1 ⪤*[R, #0] Y2 →
+ ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
+ | ∃∃I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 & R L1 V1 V2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
+ | ∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
#R #Y1 #Y2 #H elim (lfxs_inv_zero … H) -H *
/4 width=9 by lexs_fwd_length, ex4_5_intro, ex3_3_intro, or3_intro2, or3_intro1, or3_intro0, conj/
qed-.
]
[ { "unbound context-sensitive parallel rt-computation" * } {
[ [ "refinement for lenvs on selected entries" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
- [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
+ [ [ "strongly normalizing for lenvs on referred entries" ] "rdsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "rdsx_length" + "rdsx_drops" + "rdsx_fqup" + "rdsx_cpxs" + "rdsx_csx" + "rdsx_rdsx" * ]
[ [ "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_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_ffdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
[ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
projects / helm.git / commitdiff