λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≡ K →
∀U. ⬆*[f] T ≡ U → R L U.
+definition d_liftable1_isuni: predicate (relation2 lenv term) ≝
+ λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≡ K → 𝐔⦃f⦄ →
+ ∀U. ⬆*[f] T ≡ U → R L U.
+
definition d_deliftable1: predicate (relation2 lenv term) ≝
λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K →
∀T. ⬆*[f] T ≡ U → R K T.
+definition d_deliftable1_isuni: predicate (relation2 lenv term) ≝
+ λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K → 𝐔⦃f⦄ →
+ ∀T. ⬆*[f] T ≡ U → R K T.
+
definition d_liftable2_sn: ∀C:Type[0]. ∀S:rtmap → relation C.
predicate (lenv → relation C) ≝
λC,S,R. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
]
qed-.
-
lemma drops_after_fwd_drop2: ∀b,f2,I,X,K. ⬇*[b, f2] X ≡ K.ⓘ{I} →
∀f1,f. 𝐈⦃f1⦄ → f2 ⊚ ⫯f1 ≡ f → ⬇*[b, f] X ≡ K.
#b #f2 #I #X #K #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H
(* *)
(**************************************************************************)
+include "basic_2/relocation/lifts_lifts_bind.ma".
include "basic_2/relocation/drops.ma".
(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
]
qed-.
+lemma lexs_liftable_co_dedropable_bi: ∀RN,RP. d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP →
+ ∀f2,L1,L2. L1 ⪤*[cfull, RP, f2] L2 → ∀f1,K1,K2. K1 ⪤*[RN, RP, f1] K2 →
+ ∀b,f. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 →
+ f ~⊚ f1 ≡ f2 → L1 ⪤*[RN, RP, f2] L2.
+#RN #RP #HRN #HRP #f2 #L1 #L2 #H elim H -f2 -L1 -L2 //
+#g2 #I1 #I2 #L1 #L2 #HL12 #HI12 #IH #f1 #Y1 #Y2 #HK12 #b #f #HY1 #HY2 #H
+[ elim (coafter_inv_xxn … H) [ |*: // ] -H #g #g1 #Hg2 #H1 #H2 destruct
+ elim (drops_inv_skip1 … HY1) -HY1 #J1 #K1 #HLK1 #HJI1 #H destruct
+ elim (drops_inv_skip1 … HY2) -HY2 #J2 #K2 #HLK2 #HJI2 #H destruct
+ elim (lexs_inv_next … HK12) -HK12 #HK12 #HJ12
+ elim (HRN … HJ12 … HLK1 … HJI1) -HJ12 -HJI1 #Z #Hz
+ >(liftsb_mono … Hz … HJI2) -Z /3 width=9 by lexs_next/
+| elim (coafter_inv_xxp … H) [1,2: |*: // ] -H *
+ [ #g #g1 #Hg2 #H1 #H2 destruct
+ elim (drops_inv_skip1 … HY1) -HY1 #J1 #K1 #HLK1 #HJI1 #H destruct
+ elim (drops_inv_skip1 … HY2) -HY2 #J2 #K2 #HLK2 #HJI2 #H destruct
+ elim (lexs_inv_push … HK12) -HK12 #HK12 #HJ12
+ elim (HRP … HJ12 … HLK1 … HJI1) -HJ12 -HJI1 #Z #Hz
+ >(liftsb_mono … Hz … HJI2) -Z /3 width=9 by lexs_push/
+ | #g #Hg2 #H destruct
+ lapply (drops_inv_drop1 … HY1) -HY1 #HLK1
+ lapply (drops_inv_drop1 … HY2) -HY2 #HLK2
+ /3 width=9 by lexs_push/
+ ]
+]
+qed-.
+
(* Basic_2A1: includes: lpx_sn_liftable_dedropable *)
lemma lexs_liftable_co_dedropable_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
- d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP → co_dedropable_sn (lexs RN RP).
+ d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP →
+ co_dedropable_sn (lexs RN RP).
#RN #RP #H1RN #H1RP #H2RN #H2RP #b #f #L1 #K1 #H elim H -f -L1 -K1
[ #f #Hf #X #f1 #H #f2 #Hf2 >(lexs_inv_atom1 … H) -X
/4 width=4 by drops_atom, lexs_atom, ex3_intro/
(* Forward lemmas with length for local environments ************************)
-(* Basic_2A1: includes: lpx_sn_fwd_length *)
+(* Basic_2A1: uses: lpx_sn_fwd_length *)
lemma lexs_fwd_length: ∀RN,RP,f,L1,L2. L1 ⪤*[RN, RP, f] L2 → |L1| = |L2|.
#RM #RP #f #L1 #L2 #H elim H -f -L1 -L2 //
#f #I1 #I2 #L1 #L2 >length_bind >length_bind //
qed-.
+
+(* Properties with length for local environments ****************************)
+
+lemma lexs_length_cfull: ∀L1,L2. |L1| = |L2| → ∀f. L1 ⪤*[cfull, cfull, f] L2.
+#L1 elim L1 -L1
+[ #Y2 #H >(length_inv_zero_sn … H) -Y2 //
+| #L1 #I1 #IH #Y2 #H #f
+ elim (length_inv_succ_sn … H) -H #I2 #L2 #HL12 #H destruct
+ elim (pn_split f) * #g #H destruct /3 width=1 by lexs_next, lexs_push/
+]
+qed.
[ elim (liftsb_inv_pair_sn … H) | lapply (liftsb_inv_unit_sn … H) ] -H
/3 width=6 by lifts_trans, ext2_pair, ext2_unit/
qed-.
+
+theorem liftsb_conf: ∀f1,I,I1. ⬆*[f1] I ≡ I1 → ∀f,I2. ⬆*[f] I ≡ I2 →
+ ∀f2. f2 ⊚ f1 ≡ f → ⬆*[f2] I1 ≡ I2.
+#f1 #I #I1 * -I -I1 #I [2: #V #V1 #HV1 ] #f2 #I2 #H
+[ elim (liftsb_inv_pair_sn … H) | lapply (liftsb_inv_unit_sn … H) ] -H
+/3 width=6 by lifts_conf, ext2_pair, ext2_unit/
+qed-.
+
+(* Advanced proprerties *****************************************************)
+
+lemma liftsb_inj: ∀f. is_inj2 … (liftsb f).
+#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐈𝐝 … f)
+/3 width=6 by liftsb_div3, liftsb_fwd_isid/
+qed-.
+
+lemma liftsb_mono: ∀f,T. is_mono … (liftsb f T).
+#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐈𝐝 … f)
+/3 width=6 by liftsb_conf, liftsb_fwd_isid/
+qed-.
elim (lifts_total V (𝐔❴⫯i❵))
/4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/
qed-.
+
+lemma csx_inv_lref: ∀h,o,G,L,i. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃#i⦄ →
+ ∨∨ ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆
+ | ∃∃I,K. ⬇*[i] L ≡ K.ⓤ{I}
+ | ∃∃I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄.
+#h #o #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/
+* * /4 width=9 by csx_inv_lref_pair, ex2_3_intro, ex1_2_intro, or3_intro2, or3_intro1/
+qed-.
(* Basic_1: was just: sn3_beta *)
lemma csx_appl_beta: ∀h,o,p,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}ⓝW.V.T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.ⓛ{p}W.T⦄.
/2 width=3 by csx_appl_beta_aux/ qed.
+
+(* Advanced forward lemmas **************************************************)
+
+fact csx_fwd_bind_dx_unit_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ →
+ ∀p,I,J,V,T. U = ⓑ{p,I}V.T → ⦃G, L.ⓤ{J}⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+#h #o #G #L #U #H elim H -H #U0 #_ #IH #p #I #J #V #T #H destruct
+@csx_intro #T2 #HLT2 #HT2
+@(IH (ⓑ{p,I}V.T2)) -IH /2 width=4 by cpx_bind_unit/ -HLT2
+#H elim (tdeq_inv_pair … H) -H /2 width=1 by/
+qed-.
+
+lemma csx_fwd_bind_dx_unit: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ →
+ ∀J. ⦃G, L.ⓤ{J}⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+/2 width=6 by csx_fwd_bind_dx_unit_aux/ qed-.
+
+lemma csx_fwd_bind_unit: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ →
+ ∀J. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ ∧ ⦃G, L.ⓤ{J}⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+/3 width=4 by csx_fwd_pair_sn, csx_fwd_bind_dx_unit, conj/ qed-.
⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V.
/2 width=2 by tc_lfxs_fwd_bind_dx/ qed-.
+lemma lfpxs_fwd_bind_dx_void: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 →
+ ⦃G, L1.ⓧ⦄ ⊢ ⬈*[h, T] L2.ⓧ.
+/2 width=4 by tc_lfxs_fwd_bind_dx_void/ qed-.
+
(* Advanced eliminators *****************************************************)
(* Basic_2A1: uses: lpxs_ind *)
]
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/csx_lsubr.ma".
+include "basic_2/rt_computation/lfsx_lfpxs.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(*
+(* Advanced properties ******************************************************)
+
+lemma lsx_lref_be_lpxs: ∀h,o,I,G,K1,V,i,l. l ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, o] V →
+ ∀K2. G ⊢ ⬊*[h, o, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, o] K2 →
+ ∀L2. ⬇[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⬊*[h, o, #i, l] L2.
+#h #o #I #G #K1 #V #i #l #Hli #H @(csx_ind_alt … H) -V
+#V0 #_ #IHV0 #K2 #H @(lsx_ind … H) -K2
+#K0 #HK0 #IHK0 #HK10 #L0 #HLK0 @lsx_intro
+#L2 #HL02 #HnL02 elim (lpx_drop_conf … HLK0 … HL02) -HL02
+#Y #H #HLK2 elim (lpx_inv_pair1 … H) -H
+#K2 #V2 #HK02 #HV02 #H destruct
+elim (eq_term_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnL02 -HLK0 ]
+[ /4 width=8 by lpxs_strap1, lleq_lref/
+| @(IHV0 … HnV02 … HLK2) -IHV0 -HnV02 -HLK2
+ /3 width=4 by lsx_cpx_trans_O, lsx_lpx_trans, lpxs_cpx_trans, lpxs_strap1/ (**) (* full auto too slow *)
+]
+qed.
+
+lemma lsx_lref_be: ∀h,o,I,G,K,V,i,l. l ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, o] V →
+ G ⊢ ⬊*[h, o, V, 0] K →
+ ∀L. ⬇[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, o, #i, l] L.
+/2 width=8 by lsx_lref_be_lpxs/ qed.
+*)
+(* Main properties **********************************************************)
+
+theorem csx_lsx: ∀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 [ |*: * ]
+ [ #HL
+ | #I #K #HLK
+ | #I #K #V #HLK #HV
+ ]
+(*
+ elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/
+ elim (ylt_split i l) /2 width=1 by lsx_lref_skip/
+ #Hli #Hi elim (drop_O1_lt (Ⓕ) … Hi) -Hi
+ #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H
+ /4 width=6 by lsx_lref_be, fqup_lref/
+*)
+| #a #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 UNCOUNTED 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-.
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/computation/csx_lpxs.ma".
-include "basic_2/computation/lcosx_cpx.ma".
-
-(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
-
-(* Advanced properties ******************************************************)
-
-lemma lsx_lref_be_lpxs: ∀h,o,I,G,K1,V,i,l. l ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, o] V →
- ∀K2. G ⊢ ⬊*[h, o, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, o] K2 →
- ∀L2. ⬇[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⬊*[h, o, #i, l] L2.
-#h #o #I #G #K1 #V #i #l #Hli #H @(csx_ind_alt … H) -V
-#V0 #_ #IHV0 #K2 #H @(lsx_ind … H) -K2
-#K0 #HK0 #IHK0 #HK10 #L0 #HLK0 @lsx_intro
-#L2 #HL02 #HnL02 elim (lpx_drop_conf … HLK0 … HL02) -HL02
-#Y #H #HLK2 elim (lpx_inv_pair1 … H) -H
-#K2 #V2 #HK02 #HV02 #H destruct
-elim (eq_term_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnL02 -HLK0 ]
-[ /4 width=8 by lpxs_strap1, lleq_lref/
-| @(IHV0 … HnV02 … HLK2) -IHV0 -HnV02 -HLK2
- /3 width=4 by lsx_cpx_trans_O, lsx_lpx_trans, lpxs_cpx_trans, lpxs_strap1/ (**) (* full auto too slow *)
-]
-qed.
-
-lemma lsx_lref_be: ∀h,o,I,G,K,V,i,l. l ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, o] V →
- G ⊢ ⬊*[h, o, V, 0] K →
- ∀L. ⬇[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, o, #i, l] L.
-/2 width=8 by lsx_lref_be_lpxs/ qed.
-
-(* Main properties **********************************************************)
-
-theorem csx_lsx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ∀l. G ⊢ ⬊*[h, o, T, l] 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 #l destruct
- elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/
- elim (ylt_split i l) /2 width=1 by lsx_lref_skip/
- #Hli #Hi elim (drop_O1_lt (Ⓕ) … Hi) -Hi
- #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H
- /4 width=6 by lsx_lref_be, fqup_lref/
-| #a #I #V #T #HG #HL #HT #H #l destruct
- elim (csx_fwd_bind … H) -H /3 width=1 by lsx_bind/
-| #I #V #T #HG #HL #HT #H #l destruct
- elim (csx_fwd_flat … H) -H /3 width=1 by lsx_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/multiple/lleq_drop.ma".
-include "basic_2/reduction/lpx_drop.ma".
-include "basic_2/computation/lsx.ma".
-
-(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
-
-(* Advanced properties ******************************************************)
-
-lemma lsx_lref_free: ∀h,o,G,L,l,i. |L| ≤ i → G ⊢ ⬊*[h, o, #i, l] L.
-#h #o #G #L1 #l #i #HL1 @lsx_intro
-#L2 #HL12 #H elim H -H
-/4 width=6 by lpx_fwd_length, lleq_free, le_repl_sn_conf_aux/
-qed.
-
-lemma lsx_lref_skip: ∀h,o,G,L,l,i. yinj i < l → G ⊢ ⬊*[h, o, #i, l] L.
-#h #o #G #L1 #l #i #HL1 @lsx_intro
-#L2 #HL12 #H elim H -H
-/3 width=4 by lpx_fwd_length, lleq_skip/
-qed.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma lsx_fwd_lref_be: ∀h,o,I,G,L,l,i. l ≤ yinj i → G ⊢ ⬊*[h, o, #i, l] L →
- ∀K,V. ⬇[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, o, V, 0] K.
-#h #o #I #G #L #l #i #Hli #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro
-#K2 #HK12 #HnK12 lapply (drop_fwd_drop2 … HLK1)
-#H2LK1 elim (drop_lpx_trans … H2LK1 … HK12) -H2LK1 -HK12
-#L2 #HL12 #H2LK2 #H elim (lreq_drop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/
-#Y #_ #HLK2 lapply (drop_fwd_drop2 … HLK2)
-#HY lapply (drop_mono … HY … H2LK2) -HY -H2LK2 #H destruct
-/4 width=10 by lleq_inv_lref_ge/
-qed-.
-
-(* Properties on relocation *************************************************)
-
-lemma lsx_lift_le: ∀h,o,G,K,T,U,lt,l,k. lt ≤ yinj l →
- ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, T, lt] K →
- ∀L. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, U, lt] L.
-#h #o #G #K #T #U #lt #l #k #Hltl #HTU #H @(lsx_ind … H) -K
-#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
-#L2 #HL12 #HnU elim (lpx_drop_conf … HLK1 … HL12) -HL12
-/4 width=10 by lleq_lift_le/
-qed-.
-
-lemma lsx_lift_ge: ∀h,o,G,K,T,U,lt,l,k. yinj l ≤ lt →
- ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, T, lt] K →
- ∀L. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, U, lt + k] L.
-#h #o #G #K #T #U #lt #l #k #Hllt #HTU #H @(lsx_ind … H) -K
-#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
-#L2 #HL12 #HnU elim (lpx_drop_conf … HLK1 … HL12) -HL12
-/4 width=9 by lleq_lift_ge/
-qed-.
-
-(* Inversion lemmas on relocation *******************************************)
-
-lemma lsx_inv_lift_le: ∀h,o,G,L,T,U,lt,l,k. lt ≤ yinj l →
- ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L →
- ∀K. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, T, lt] K.
-#h #o #G #L #T #U #lt #l #k #Hltl #HTU #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
-#K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12
-/4 width=10 by lleq_inv_lift_le/
-qed-.
-
-lemma lsx_inv_lift_be: ∀h,o,G,L,T,U,lt,l,k. yinj l ≤ lt → lt ≤ l + k →
- ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L →
- ∀K. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, T, l] K.
-#h #o #G #L #T #U #lt #l #k #Hllt #Hltlm #HTU #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
-#K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12
-/4 width=11 by lleq_inv_lift_be/
-qed-.
-
-lemma lsx_inv_lift_ge: ∀h,o,G,L,T,U,lt,l,k. yinj l + yinj k ≤ lt →
- ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L →
- ∀K. ⬇[Ⓕ, l, k] L ≡ K → G ⊢ ⬊*[h, o, T, lt-k] K.
-#h #o #G #L #T #U #lt #l #k #Hlmlt #HTU #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
-#K2 #HK12 #HnT elim (drop_lpx_trans … HLK1 … HK12) -HK12
-/4 width=9 by lleq_inv_lift_ge/
-qed-.
lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma
csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma
csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma
-lfsx.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma
+lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma
lemma lsubr_cpx_trans: ∀h,G. lsub_trans … (cpx h G) lsubr.
#h #G #L1 #T1 #T2 * /3 width=4 by lsubr_cpg_trans, ex_intro/
qed-.
+
+lemma cpx_bind_unit: ∀h,L,G,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
+ ∀J,T1,T2. ⦃G, L.ⓤ{J}⦄ ⊢ T1 ⬈[h] T2 →
+ ∀p,I. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] ⓑ{p,I}V2.T2.
+/4 width=4 by lsubr_cpx_trans, cpx_bind, lsubr_unit/ 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.
+/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.
/2 width=3 by lfxs_fwd_pair_sn/ qed-.
(* Properties with generic slicing for local environments *******************)
-(* Basic_2A1: includes: lleq_lift_le lleq_lift_ge *)
lemma lfdeq_lifts_sn: ∀h,o. dedropable_sn (cdeq h o).
/3 width=5 by lfxs_liftable_dedropable_sn, tdeq_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)
-(* Basic_2A1: restricts: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
lemma lfdeq_inv_lifts_sn: ∀h,o. dropable_sn (cdeq h o).
/2 width=5 by lfxs_dropable_sn/ qed-.
lemma lfdeq_inv_lifts_dx: ∀h,o. dropable_dx (cdeq h o).
/2 width=5 by lfxs_dropable_dx/ qed-.
-(* Note: missing in basic_2A1 *)
-lemma lfdeq_inv_lifts_bi: ∀h,o,L1,L2,U. L1 ≡[h, o, U] L2 →
- ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 →
- ∀T. ⬆*[i] T ≡ U → K1 ≡[h, o, T] K2.
-/2 width=8 by lfxs_inv_lifts_bi/ qed-.
+(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
+lemma lfdeq_inv_lifts_bi: ∀h,o,L1,L2,U. L1 ≡[h, o, U] L2 → ∀b,f. 𝐔⦃f⦄ →
+ ∀K1,K2. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 →
+ ∀T. ⬆*[f] T ≡ U → K1 ≡[h, o, T] K2.
+/2 width=10 by lfxs_inv_lifts_bi/ qed-.
lemma lfdeq_inv_lref_pair_sn: ∀h,o,L1,L2,i. L1 ≡[h, o, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 →
∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ≡[h, o, V1] K2 & V1 ≡[h, o] V2.
/2 width=5 by fqu_flat_dx, ex3_2_intro/
| #I #G #L2 #T #U #HTU #Y #HU
elim (lfdeq_fwd_dx … HU) #L1 #V1 #H destruct
- /5 width=12 by lfdeq_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/
+ /5 width=14 by lfdeq_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/
]
qed-.
(* *)
(**************************************************************************)
+include "basic_2/relocation/lifts_tdeq.ma".
include "basic_2/static/lfxs_length.ma".
include "basic_2/static/lfdeq.ma".
(* Basic_2A1: lleq_fwd_length *)
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-.
+
+(* Properties with length for local environments ****************************)
+
+(* 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.
+/3 width=9 by lfxs_lifts_bi, tdeq_lifts_sn/ qed-.
∀L1. L0 ⪤*[RP1, T0] L1 → ∀L2. L0 ⪤*[RP2, T0] L2 →
∃∃T. R2 L1 T1 T & R1 L2 T2 T.
-(* Basic properties *********************************************************)
-
-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}.
-#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.
-#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}.
-/4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed.
-
-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}.
-#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}.
-#R #I #I1 #L1 #L2 #T * #f #Hf #HL12 #I2 #HR
-/3 width=5 by lexs_pair_repl, ex2_intro/
-qed-.
-
-lemma lfxs_sym: ∀R. lexs_frees_confluent (cext2 R) cfull →
- (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
- ∀T. symmetric … (lfxs R T).
-#R #H1R #H2R #T #L1 #L2 * #f1 #Hf1 #HL12 elim (H1R … Hf1 … HL12) -Hf1
-/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, 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.
-#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.
-#R1 #R2 #L1 #L2 #T1 #T2 #H1 #H2 *
-/4 width=7 by lexs_co_isid, ex2_intro/
-qed-.
-
(* Basic inversion lemmas ***************************************************)
lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⪤*[R, T] Y2 → Y2 = ⋆.
(* 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.
+#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.
#R * [ #p ] #I #L1 #L2 #V #T * #f #Hf #HL
/2 width=3 by ex1_2_intro/
qed-.
+(* Basic properties *********************************************************)
+
+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}.
+#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.
+#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}.
+/4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed.
+
+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}.
+#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}.
+#R #I #I1 #L1 #L2 #T * #f #Hf #HL12 #I2 #HR
+/3 width=5 by lexs_pair_repl, ex2_intro/
+qed-.
+
+lemma lfxs_sym: ∀R. lexs_frees_confluent (cext2 R) cfull →
+ (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
+ ∀T. symmetric … (lfxs R T).
+#R #H1R #H2R #T #L1 #L2 * #f1 #Hf1 #HL12 elim (H1R … Hf1 … HL12) -Hf1
+/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, 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.
+#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.
+#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.
+#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/
+qed-.
+
(* Basic_2A1: removed theorems 9:
llpx_sn_skip llpx_sn_lref llpx_sn_free
llpx_sn_fwd_lref
(* Properties with generic slicing for local environments *******************)
-(* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *)
lemma lfxs_liftable_dedropable_sn: ∀R. (∀L. reflexive ? (R L)) →
d_liftable2_sn … lifts R → dedropable_sn R.
#R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU
(* Inversion lemmas with generic slicing for local environments *************)
-(* Basic_2A1: restricts: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *)
+(* Basic_2A1: uses: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *)
(* Basic_2A1: was: llpx_sn_drop_conf_O *)
lemma lfxs_dropable_sn: ∀R. dropable_sn R.
#R #b #f #L1 #K1 #HLK1 #H1f #L2 #U * #f2 #Hf2 #HL12 #T #HTU
/4 width=9 by frees_inv_lifts, ex2_intro/
qed-.
-(* Basic_2A1: was: llpx_sn_inv_lift_O *)
-lemma lfxs_inv_lifts_bi: ∀R,L1,L2,U. L1 ⪤*[R, U] L2 →
- ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 →
- ∀T. ⬆*[i] T ≡ U → K1 ⪤*[R, T] K2.
-#R #L1 #L2 #U #HL12 #K1 #K2 #i #HLK1 #HLK2 #T #HTU
+(* Basic_2A1: uses: llpx_sn_inv_lift_O *)
+lemma lfxs_inv_lifts_bi: ∀R,L1,L2,U. L1 ⪤*[R, U] L2 → ∀b,f. 𝐔⦃f⦄ →
+ ∀K1,K2. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 →
+ ∀T. ⬆*[f] T ≡ U → K1 ⪤*[R, T] K2.
+#R #L1 #L2 #U #HL12 #b #f #Hf #K1 #K2 #HLK1 #HLK2 #T #HTU
elim (lfxs_dropable_sn … HLK1 … HL12 … HTU) -L1 -U // #Y #HK12 #HY
-lapply (drops_mono … HY … HLK2) -L2 -i #H destruct //
+lapply (drops_mono … HY … HLK2) -b -f -L2 #H destruct //
qed-.
lemma lfxs_inv_lref_pair_sn: ∀R,L1,L2,i. L1 ⪤*[R, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 →
(**************************************************************************)
include "basic_2/relocation/lexs_length.ma".
-include "basic_2/static/lfxs.ma".
+include "basic_2/static/lfxs_drops.ma".
(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
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_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.
+#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
+/4 width=12 by lexs_length_cfull, lexs_liftable_co_dedropable_bi, cext2_d_liftable2_sn, cfull_lift_sn, ex2_intro/
+qed-.
]
[ { "strongly normalizing rt-computation" * } {
[ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ]
- [ "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ]
+ [ "llsx_csx" * ]
[ "csx_fpbs" * ]
}
]
]
*)
[ { "uncounted context-sensitive rt-computation" * } {
- [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
+ [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
[ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
[ { "rt-transition" * } {
[ { "uncounted rst-transition" * } {
[ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
- [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
+ [ "fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
}
]
[ { "t-bound context-sensitive rt-transition" * } {
projects / helm.git / commitdiff