(* *)
(**************************************************************************)
-include "basic_2/reduction/lpx_leq.ma".
+include "basic_2/reduction/cpx_lleq.ma".
include "basic_2/computation/cpxs.ma".
(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
(* Properties on lazy equivalence for local environments ********************)
lemma lleq_cpxs_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 →
- ∀L1. L1 ⋕[0, T1] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2.
+ ∀L1. L1 ⋕[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2.
#h #g #G #L2 #T1 #T2 #H @(cpxs_ind_dx … H) -T1
/4 width=6 by lleq_cpx_conf_dx, lleq_cpx_trans, cpxs_strap2/
qed-.
lemma lleq_cpxs_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 →
- ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2.
+ ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
#h #g #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by lleq_cpx_conf_dx/
qed-.
(**************************************************************************)
include "basic_2/notation/relations/btpredproper_8.ma".
-include "basic_2/relocation/lleq.ma".
+include "basic_2/substitution/lleq.ma".
include "basic_2/computation/fpbs.ma".
(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
inductive fpbu (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
| fpbu_fqup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2
| fpbu_cpxs: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2
-| fpbu_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T1] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1
+| fpbu_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1
.
interpretation
⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
/3 width=1 by fpbu_cpxs, cprs_cpxs/ qed.
-lemma lprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[0, T] L2 → ⊥) →
+lemma lprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[T, 0] L2 → ⊥) →
⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄.
/3 width=1 by fpbu_lpxs, lprs_lpxs/ qed.
(**************************************************************************)
include "basic_2/notation/relations/btpredsnstar_8.ma".
-include "basic_2/relocation/lleq.ma".
+include "basic_2/substitution/lleq.ma".
include "basic_2/computation/lpxs.ma".
(* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************)
inductive fpns (h) (g) (G) (L1) (T): relation3 genv lenv term ≝
-| fpns_intro: ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[0, T] L2 → fpns h g G L1 T G L2 T
+| fpns_intro: ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[T, 0] L2 → fpns h g G L1 T G L2 T
.
interpretation
(* Basic inversion lemmas ***************************************************)
lemma fpns_inv_gen: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ →
- ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & L1 ⋕[0, T1] L2 & T1 = T2.
+ ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & L1 ⋕[T1, 0] L2 & T1 = T2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and4_intro/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/relocation/lleq_lleq.ma".
+include "basic_2/substitution/lleq_lleq.ma".
include "basic_2/computation/lpxs_lpxs.ma".
include "basic_2/computation/fpns.ma".
G1 ⊢ ⋕⬊*[h, g, T1] L1 → G2 ⊢ ⋕⬊*[h, g, T2] L2.
axiom fqup_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ →
- ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) →
+ ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[T2, 0] L2 →⊥) →
∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 &
- K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
+ K1 ⋕[T1, 0] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
(* *)
(**************************************************************************)
-include "basic_2/relocation/lleq_lleq.ma".
+include "basic_2/substitution/lleq_alt.ma".
include "basic_2/computation/lpxs_ldrop.ma".
include "basic_2/computation/lpxs_cpxs.ma".
(* Advanced properties ******************************************************)
-axiom lleq_lpxs_trans_nlleq: ∀h,g,G,L1s,L1d,T,d. L1s ⋕[d, T] L1d →
- ∀L2d. ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → (L1d ⋕[d, T] L2d → ⊥) →
- ∃∃L2s. ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s & L2s ⋕[d, T] L2d & L1s ⋕[d, T] L2s → ⊥.
+axiom lleq_lpxs_trans_nlleq: ∀h,g,G,L1s,L1d,T,d. L1s ⋕[T, d] L1d →
+ ∀L2d. ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → (L1d ⋕[T, d] L2d → ⊥) →
+ ∃∃L2s. ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s & L2s ⋕[T, d] L2d & L1s ⋕[T, d] L2s → ⊥.
(* Advanced inversion lemmas ************************************************)
-axiom lpxs_inv_cpxs_nlleq: ∀h,g,G,L1,L2,T1. ⦃G, L1⦄ ⊢ ➡*[h,g] L2 → (L1 ⋕[O, T1] L2 → ⊥) →
+axiom lpxs_inv_cpxs_nlleq: ∀h,g,G,L1,L2,T1. ⦃G, L1⦄ ⊢ ➡*[h,g] L2 → (L1 ⋕[T1, 0] L2 → ⊥) →
∃∃T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & T1 = T2 → ⊥ & ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2.
(* Properties on lazy equivalence for local environments ********************)
lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[0, T1] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[0, T2] L2.
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1
#K0 #V0 #H1KL1 #_ #H destruct
elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
- #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
+ #I1 #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
/2 width=4 by fqu_lref_O, ex3_intro/
| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
[ elim (lleq_inv_bind … H)
qed-.
lemma lpxs_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[0, T1] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[0, T2] L2.
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
elim (fquq_inv_gen … H) -H
[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
qed-.
lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[0, T1] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[0, T2] L2.
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
/3 width=4 by fqu_fqup, ex3_intro/
qed-.
lemma lpxs_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[0, T1] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[0, T2] L2.
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
elim (fqus_inv_gen … H) -H
[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
(**************************************************************************)
include "basic_2/notation/relations/lazysn_5.ma".
-include "basic_2/relocation/lleq.ma".
+include "basic_2/substitution/lleq.ma".
include "basic_2/computation/lpxs.ma".
(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
lemma lsx_ind: ∀h,g,T,G. ∀R:predicate lenv.
(∀L1. G ⊢ ⋕⬊*[h, g, T] L1 →
- (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T] L2 → ⊥) → R L2) →
+ (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → R L2) →
R L1
) →
∀L. G ⊢ ⋕⬊*[h, g, T] L → R L.
(* Basic properties *********************************************************)
lemma lsx_intro: ∀h,g,T,G,L1.
- (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) →
+ (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) →
G ⊢ ⋕⬊*[h, g, T] L1.
/5 width=1 by lleq_sym, SN_intro/ qed.
(* Advanced properties ******************************************************)
lemma lsx_lleq_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 →
- ∀L2. L1 ⋕[0, T] L2 → G ⊢ ⋕⬊*[h, g, T] L2.
+ ∀L2. L1 ⋕[T, 0] L2 → G ⊢ ⋕⬊*[h, g, T] L2.
#h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
@lsx_intro #L #HL2 #HnT elim (lleq_lpxs_trans_nlleq … HL12 … HL2 HnT) -L2 /3 width=4 by/
qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/ldrop_leq.ma".
+include "basic_2/relocation/lleq_lleq.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma lleq_cpx_trans_leq: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀L1,d. L1 ⋕[d, T1] L2 → L1 ≃[d, ∞] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_sort/
+[ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #d #H #HL12 elim (lleq_inv_lref_dx … H … HLK2) -H *
+ [ #K1 #HLK1 #HV1 #Hdi elim (ldrop_leq_conf_be … HL12 … HLK1) -HL12 /2 width=1 by yle_inj/
+ >yminus_Y_inj #J #Y #X #HK12 #H lapply (ldrop_mono … H … HLK2) -L2
+ #H destruct /3 width=7 by cpx_delta/
+ | #J #K1 #V #HLK1 #_ #HV1 #Hid elim (ldrop_leq_conf_lt … HL12 … HLK1) -HL12 /2 width=1 by ylt_inj/
+ <yminus_SO2 >yminus_inj #Y #HK12 #H lapply (ldrop_mono … H … HLK2) -L2
+ #H destruct /3 width=7 by cpx_delta/
+ ]
+| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_bind … H) -H
+ /4 width=3 by cpx_bind, leq_succ/
+| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
+ /3 width=3 by cpx_flat/
+| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #H elim (lleq_inv_bind … H) -H
+ /4 width=3 by cpx_zeta, leq_succ/
+| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
+ /3 width=3 by cpx_tau/
+| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #d #H elim (lleq_inv_flat … H) -H
+ /3 width=3 by cpx_ti/
+| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
+ #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_beta, leq_succ/
+| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
+ #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_theta, leq_succ/
+]
+qed-.
+
+(* Note: this can be proved directly *)
+lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀L1. L1 ⋕[0, T1] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
+/4 width=6 by lleq_cpx_trans_leq, lleq_fwd_length, leq_O_Y/ 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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ≃ break [ term 46 d , break term 46 e ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'Iso $d $e $L1 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/ynat/ynat_plus.ma".
+include "basic_2/grammar/leq.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
+
+lemma ldrop_leq_conf_ge: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀I,K,V,i. ⇩[O, i]L1 ≡ K.ⓑ{I}V → d + e ≤ i →
+ ⇩[O, i]L2 ≡ K.ⓑ{I}V.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #J #K #W #i #H elim (ldrop_inv_atom1 … H) -H
+ #H destruct
+| #I #L1 #L2 #V #HL12 #IHL12 #J #K #W #i #H #_ elim (ldrop_inv_O1_pair1 … H) -H
+ * #H1 #H2
+ [ -IHL12 lapply (leq_inv_O2 … HL12) -HL12
+ #H3 destruct //
+ | -HL12 /4 width=1 by ldrop_ldrop_lt, yle_inj/
+ ]
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #IHL12 #J #K #W #i #H1 >yplus_succ_swap
+ #Hei elim (yle_inv_inj2 … Hei) -Hei
+ #x #Hei #H elim (yplus_inv_inj … H) -H normalize
+ #y #z >commutative_plus
+ #H1 #H2 #H3 destruct elim (le_inv_plus_l … Hei) -Hei
+ #Hzi #Hi lapply (ldrop_inv_ldrop1_lt … H1 ?) -H1
+ /4 width=1 by ldrop_ldrop_lt, yle_inj/
+| #I #L1 #L2 #V #d #e #_ #IHL12 #J #K #W #i #H0 #Hdei elim (yle_inv_inj2 … Hdei) -Hdei
+ #x #Hdei #H elim (yplus_inv_inj … H) -H
+ #y #z >commutative_plus
+ #H1 #H2 #H3 destruct elim (ysucc_inv_inj_dx … H2) -H2
+ #x #H1 #H2 destruct elim (le_inv_plus_l … Hdei)
+ #_ #Hi lapply (ldrop_inv_ldrop1_lt … H0 ?) -H0
+ [2: #H0 @ldrop_ldrop_lt ] [2,3: /2 width=3 by lt_to_le_to_lt/ ]
+ /4 width=3 by yle_inj, monotonic_pred/
+]
+qed-.
+
+lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀I1,K1,V1,i. ⇩[O, i]L1 ≡ K1.ⓑ{I1}V1 → d ≤ i → i < d + e →
+ ∃∃I2,K2,V2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I2}V2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H
+ #H destruct
+| #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) //
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O1 >yplus_O1
+ #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
+ [ #_ lapply (ldrop_inv_O2 … H) -H
+ #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/
+ | lapply (ldrop_inv_ldrop1_lt … H ?) -H //
+ #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/
+ #Hie lapply (ylt_inv_succ … Hie) -Hie
+ #Hie elim (IHL12 … H) -IHL12 -H //
+ >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/
+ ]
+| #I #L1 #L2 #V #d #e #_ #IHL12 #J1 #K1 #W1 #i #H #Hdi lapply (ylt_yle_trans 0 … Hdi ?) //
+ #Hi <(ylt_inv_O1 … Hi) >yplus_succ1 >yminus_succ elim (yle_inv_succ1 … Hdi) -Hdi
+ #Hdi #_ #Hide lapply (ylt_inv_succ … Hide)
+ #Hide lapply (ylt_inv_inj … Hi) -Hi
+ #Hi lapply (ldrop_inv_ldrop1_lt … H ?) -H //
+ #H elim (IHL12 … H) -IHL12 -H
+ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/
+]
+qed-.
+
+lemma ldrop_leq_conf_lt: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀I,K1,V,i. ⇩[O, i]L1 ≡ K1.ⓑ{I}V → i < d →
+ ∃∃K2. K1 ≃[⫰(d-i), e] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I}V.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #J #K1 #W #i #H elim (ldrop_inv_atom1 … H) -H
+ #H destruct
+| #I #L1 #L2 #V #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) //
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) //
+| #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K1 #W #i #H elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
+ [ #_ lapply (ldrop_inv_O2 … H) -H
+ #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_intro/
+ | lapply (ldrop_inv_ldrop1_lt … H ?) -H //
+ #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/
+ #Hie lapply (ylt_inv_succ … Hie) -Hie
+ #Hie elim (IHL12 … H) -IHL12 -H
+ >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_intro/
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
-include "Basic_2/grammar/lenv_length.ma".
+include "ground_2/ynat/ynat_succ.ma".
+include "basic_2/notation/relations/iso_4.ma".
+include "basic_2/grammar/lenv_length.ma".
-(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
+(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
-notation "hvbox( T1 break [ d , break e ] ≈ break T2 )"
- non associative with precedence 45
- for @{ 'Eq $T1 $d $e $T2 }.
-
-inductive leq: nat → nat → relation lenv ≝
-| leq_sort: ∀d,e. leq d e (⋆) (⋆)
-| leq_OO: ∀L1,L2. leq 0 0 L1 L2
-| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 →
- leq 0 (e + 1) (L1. 𝕓{I} V) (L2.𝕓{I} V)
-| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
- leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
+inductive leq: ynat → ynat → relation lenv ≝
+| leq_atom: ∀d,e. leq d e (⋆) (⋆)
+| leq_zero: ∀I,L1,L2,V. leq 0 0 L1 L2 → leq 0 0 (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| leq_pair: ∀I1,I2,L1,L2,V1,V2,e.
+ leq 0 e L1 L2 → leq 0 (⫯e) (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
+| leq_succ: ∀I,L1,L2,V,d,e. leq d e L1 L2 → leq (⫯d) e (L1.ⓑ{I}V) (L2.ⓑ{I}V)
.
-interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2).
-
-definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R.
- ∀L1,s1,s2. R L1 s1 s2 →
- ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2.
+interpretation
+ "equivalence (local environment)"
+ 'Iso d e L1 L2 = (leq d e L1 L2).
(* Basic properties *********************************************************)
-lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))).
-#S #R #HR #L1 #s1 #s2 #H elim H -H s2
-[ /3 width=5/
-| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
- lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/
-]
+lemma leq_refl: ∀L,d,e. L ≃[d, e] L.
+#L elim L -L /2 width=1 by/
+#L #I #V #IHL #d #e elim (ynat_cases … d) [ | * /2 width=1 by leq_succ/ ]
+elim (ynat_cases … e) [ | * ]
+/2 width=1 by leq_zero, leq_pair/
qed.
-lemma leq_refl: ∀d,e,L. L [d, e] ≈ L.
-#d elim d -d
-[ #e elim e -e // #e #IHe #L elim L -L /2/
-| #d #IHd #e #L elim L -L /2/
-]
-qed.
+lemma leq_sym: ∀L1,L2,d,e. L1 ≃[d, e] L2 → L2 ≃[d, e] L1.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+/2 width=1 by leq_atom, leq_zero, leq_pair, leq_succ/
+qed-.
-lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/
+lemma leq_O_Y: ∀L1,L2. |L1| = |L2| → L1 ≃[0, ∞] L2.
+#L1 elim L1 -L1
+[ #X #H lapply (length_inv_zero_sn … H) -H //
+| #L1 #I1 #V1 #IHL1 #X #H elim (length_inv_pos_sn … H) -H
+ #L2 #I2 #V2 #HL12 #H destruct
+ @(leq_pair … (∞)) /2 width=1 by/ (**) (* explicit constructor *)
+]
qed.
-lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d →
- ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2.
+(* Basic forward lemmas *****************************************************)
-#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/
-qed.
+lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L1| = |L2|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize //
+qed-.
(* Basic inversion lemmas ***************************************************)
+
+fact leq_inv_O2_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → e = 0 → L1 = L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/
+#I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H elim (ysucc_inv_O_dx … H)
+qed-.
+
+lemma leq_inv_O2: ∀L1,L2,d. L1 ≃[d, 0] L2 → L1 = L2.
+/2 width=4 by leq_inv_O2_aux/ qed-.
+
+fact leq_inv_Y1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → d = ∞ → L1 = L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/
+[ #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H destruct
+| #I #L1 #L2 #V #d #e #_ #IHL12 #H lapply (ysucc_inv_Y_dx … H) -H
+ /3 width=1 by eq_f3/
+]
+qed-.
+
+lemma leq_inv_Y1: ∀L1,L2,e. L1 ≃[∞, e] L2 → L1 = L2.
+/2 width=4 by leq_inv_Y1_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/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
+
+notation "hvbox( T1 break [ d , break e ] ≈ break T2 )"
+ non associative with precedence 45
+ for @{ 'Eq $T1 $d $e $T2 }.
+
+inductive leq: nat → nat → relation lenv ≝
+| leq_sort: ∀d,e. leq d e (⋆) (⋆)
+| leq_OO: ∀L1,L2. leq 0 0 L1 L2
+| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 →
+ leq 0 (e + 1) (L1. 𝕓{I} V) (L2.𝕓{I} V)
+| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
+ leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
+.
+
+interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2).
+
+definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+ ∀L1,s1,s2. R L1 s1 s2 →
+ ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2.
+
+(* Basic properties *********************************************************)
+
+lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))).
+#S #R #HR #L1 #s1 #s2 #H elim H -H s2
+[ /3 width=5/
+| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
+ lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/
+]
+qed.
+
+lemma leq_refl: ∀d,e,L. L [d, e] ≈ L.
+#d elim d -d
+[ #e elim e -e // #e #IHe #L elim L -L /2/
+| #d #IHd #e #L elim L -L /2/
+]
+qed.
+
+lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1.
+#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/
+qed.
+
+lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d →
+ ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2.
+
+#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
--- /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/reduction/cpx_leq.ma".
+include "basic_2/reduction/lpx_ldrop.ma".
+
+(**) (* to be proved later *)
+axiom- lleq_beta: ∀L2s,L2d,V2,W2,T2,d.
+ L2s.ⓛW2 ⋕[d+1, T2] L2d.ⓛW2 →
+ L2s.ⓓⓝW2.V2 ⋕[d+1, T2] L2d.ⓓⓝW2.V2.
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+(* Properties using equivalences for local environments *********************)
+
+lemma lleq_cpx_conf_leq_dx: ∀h,g,G,L1s,L1d,T1,d. L1s ⋕[d, T1] L1d → L1s ≃[d, ∞] L1d →
+ ∀T2. ⦃G, L1d⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀L2s. ⦃G, L1s⦄ ⊢ ➡[h, g] L2s → L1s ≃[0, d] L2s →
+ ∀L2d. ⦃G, L1d⦄ ⊢ ➡[h, g] L2d → L1d ≃[0, d] L2d →
+ L2s ≃[d, ∞] L2d → L2s ⋕[d, T2] L2d.
+#h #g #G #L1s #L1d #T1 #d #H elim H -L1s -L1d -T1 -d
+[ #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3
+ lapply (leq_fwd_length … H3) -H3 #HL2sd
+ elim (cpx_inv_sort1 … H2) -H2 [| * #l #_ ]
+ #H destruct /2 width=1 by lleq_sort/
+| #Is #Id #L1s #L1d #K1s #K1d #V1s #V1d #d #i #Hid #HLK1s #HLK1d #_ #_ #_ #IHV1d #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
+ elim (ldrop_leq_conf_lt … H1 … HLK1s) -H1 /2 width=1 by ylt_inj/
+ <yminus_SO2 >yminus_inj #Y #H1 #HY
+ lapply (ldrop_mono … HY … HLK1d) -HY #H destruct
+ elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s
+ elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct
+ elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d
+ elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct
+ elim (ldrop_leq_conf_be … H2s … HLK1s) -H2s /2 width=1 by ylt_inj/
+ >yplus_O1 <yminus_SO2 >yminus_inj #Z #Y #X #HK12s #H
+ lapply (ldrop_mono … H … HLK2s) -H #H destruct
+ elim (ldrop_leq_conf_be … H2d … HLK1d) -H2d /2 width=1 by ylt_inj/
+ >yplus_O1 <yminus_SO2 >yminus_inj #Z #Y #X #HK12d #H
+ lapply (ldrop_mono … H … HLK2d) -H #H destruct
+ elim (ldrop_leq_conf_lt … H3 … HLK2s) -H3 /2 width=1 by ylt_inj/
+ <yminus_SO2 >yminus_inj #Y #H3 #HY
+ lapply (ldrop_mono … HY … HLK2d) -HY #H destruct
+ elim (cpx_inv_lref1 … H2) -H2 -L1s
+ [ -L1d #H destruct /3 width=15 by lleq_skip/
+ | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d
+ #H destruct >(plus_minus_m_m d (i+1)) //
+ lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s
+ lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d
+ /3 width=9 by lleq_lift_ge/
+ ]
+| #I #L1s #L1d #K1s #K1d #V1 #d #i #Hdi #HLK1s #HLK1d #_ #IHV1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
+ elim (ldrop_leq_conf_be … H1 … HLK1s) -H1 /2 width=1 by ylt_Y, yle_inj/ #Z #Y #X #H1 #HY
+ lapply (ldrop_mono … HY … HLK1d) -HY #H destruct
+ elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s
+ elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct
+ elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d
+ elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct
+ lapply (ldrop_leq_conf_ge … H2s … HLK1s ?) /2 width=1 by yle_inj/ #H
+ lapply (ldrop_mono … H … HLK2s) -H #H destruct
+ lapply (ldrop_leq_conf_ge … H2d … HLK1d ?) /2 width=1 by yle_inj/ #H
+ lapply (ldrop_mono … H … HLK2d) -H #H destruct
+ elim (ldrop_leq_conf_be … H3 … HLK2s) -H3 /2 width=1 by ylt_Y, yle_inj/
+ >yminus_Y_inj #Z #Y #X #H3 #HY
+ lapply (ldrop_mono … HY … HLK2d) -HY #H destruct
+ elim (cpx_inv_lref1 … H2) -H2 -L1s
+ [ -L1d #H destruct /3 width=12 by lleq_lref/
+ | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d
+ #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s #HLK2s
+ lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d #HLK2d
+ @(lleq_ge … 0) /3 width=10 by lleq_lift_le/ (**) (* full auto too slow *)
+ ]
+| #L1s #L1d #d #i #HL1s #HL1d #_ #_ #X #H2 #L2s #_ #_ #L2s #_ #H2d #H3
+ lapply (leq_fwd_length … H2d) -H2d
+ lapply (leq_fwd_length … H3) -H3
+ elim (cpx_inv_lref1 … H2) -H2
+ [ #H destruct /2 width=1 by lleq_free/
+ | -L1s * #I #K1d #V1 #V2 #HLK1d
+ lapply (ldrop_fwd_length_lt2 … HLK1d) -HLK1d #H
+ elim (lt_refl_false … i) /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
+ ]
+| #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3
+ lapply (leq_fwd_length … H3) -H3 #HL2sd
+ lapply (cpx_inv_gref1 … H2) -H2
+ #H destruct /2 width=1 by lleq_gref/
+| #a #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
+ elim (cpx_inv_bind1 … H2) -H2 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct
+ /5 width=5 by lpx_pair, lleq_cpx_trans_leq, lleq_bind, leq_pair, leq_succ/
+ | #T2 #HT12 #HT2X #H1 #H2 destruct >(minus_plus_m_m d 1)
+ /4 width=9 by lpx_pair, lleq_inv_lift_ge, ldrop_ldrop, leq_pair, leq_succ/
+ ]
+| #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
+ elim (cpx_inv_flat1 … H2) -H2 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by lleq_flat/
+ | #HT1X #H destruct /2 width=1 by/
+ | #HV1X #H destruct /2 width=1 by/
+ | #a #V2 #W1 #W2 #T0 #T2 #HV12 #HW12 #HT02 #H1 #H2 #H3 destruct
+ lapply (IHT1 … (ⓛ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H
+ elim (lleq_inv_bind … H) -H -HW12 -HT02 #HW2 #HT2
+ /4 width=1 by lleq_beta, lleq_flat, lleq_bind/
+ | #a #V0 #V2 #W1 #W2 #T0 #T2 #HV10 #HV02 #HW12 #HT02 #H1 #H2 #H3 destruct
+ lapply (IHT1 … (ⓓ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H
+ elim (lleq_inv_bind … H) -H -HW12 -HT02
+ /5 width=9 by lleq_lift_ge, lleq_flat, lleq_bind, ldrop_ldrop/
+ ]
+]
+qed-.
+
+lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2.
+#h #g #G #L2 #T1 #T2 #HT12 #L1 #HT1 lapply (lleq_fwd_length … HT1)
+/3 width=13 by lleq_cpx_conf_leq_dx, leq_O_Y/
+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/unwind/sstas_sstas.ma".
-include "basic_2/equivalence/cpcs_ltpr.ma".
-include "basic_2/dynamic/snv_ltpss_dx.ma".
-include "basic_2/dynamic/snv_sstas.ma".
-include "basic_2/dynamic/ygt.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Inductive premises for the preservation results **************************)
-
-definition IH_snv_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝
- λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 ¡[g].
-
-definition IH_ssta_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝
- λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
- ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
-
-definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝
- λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L1⦄ ⊢ U1 ¡[g].
-
-definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝
- λh,g,L2,T. ⦃h, L2⦄ ⊢ T ¡[g] →
- ∀L1. h ⊢ L1 ¡⊑[g] L2 → ⦃h, L1⦄ ⊢ T ¡[g].
-
-(* Properties for the preservation results **********************************)
-
-fact snv_ltpr_cpr_aux: ∀h,g,L1,T1. IH_snv_ltpr_tpr h g L1 T1 →
- ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 ¡[g].
-#h #g #L1 #T1 #IH #HT1 #L2 #HL12 #T2 * #T #HT1T #HTT2
-lapply (IH … HL12 … HT1T) -HL12 // -T1 #HT0
-lapply (snv_tpss_conf … HT0 … HTT2) -T //
-qed-.
-
-fact ssta_ltpr_cpr_aux: ∀h,g,L1,T1. IH_ssta_ltpr_tpr h g L1 T1 →
- ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
- ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
-#h #g #L1 #T1 #IH #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 * #T #HT1T #HTT2
-elim (IH … HTU1 … HL12 … HT1T) // -L1 -T1 #U #HTU #HU1
-elim (ssta_tpss_conf … HTU … HTT2) -T #U2 #HTU2 #HU2
-lapply (cpcs_cpr_strap1 … HU1 U2 ?) /2 width=3/
-qed-.
-
-fact snv_ltpr_cprs_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
- ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 ¡[g].
-#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #L2 #HL12 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=6 by snv_ltpr_cpr_aux/ ] -HT1
-/5 width=6 by snv_ltpr_cpr_aux, ygt_yprs_trans, ltpr_cprs_yprs/
-qed-.
-
-fact ssta_ltpr_cprs_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
- ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
- ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=7 by ssta_ltpr_cpr_aux/ ]
-#T #T2 #HT1T #HTT2 * #U #HTU #HU1
-elim (ssta_ltpr_cpr_aux … HTU … HTT2) //
-[2: /3 width=9 by snv_ltpr_cprs_aux/
-|3: /5 width=6 by ygt_yprs_trans, ltpr_cprs_yprs/
-] -L0 -L1 -T0 -T1 -T #U2 #HTU2 #HU2
-lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/
-qed-.
-
-fact ssta_ltpr_cpcs_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
- ∀L1,L2,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T2⦄ →
- ⦃h, L1⦄ ⊢ T1 ¡[g] → ⦃h, L2⦄ ⊢ T2 ¡[g] →
- ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l1, U1⦄ →
- ∀U2,l2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l2, U2⦄ →
- L1 ➡ L2 → L2 ⊢ T1 ⬌* T2 →
- l1 = l2 ∧ L2 ⊢ U1 ⬌* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L1 #L2 #T1 #T2 #HLT01 #HLT02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #HL12 #H
-elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (ssta_ltpr_cprs_aux … HLT01 HT1 … HTU1 … H1) -T1 /2 width=1/ #W1 #H1 #HUW1
-elim (ssta_ltpr_cprs_aux … HLT02 HT2 … HTU2 … H2) -T2 /2 width=1/ #W2 #H2 #HUW2 -L1 -L0 -T0
-elim (ssta_mono … H1 … H2) -h -T #H1 #H2 destruct
-lapply (cpcs_canc_dx … HUW1 … HUW2) -W2 /2 width=1/
-qed-.
-
-fact snv_sstas_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
- ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ⦃h, L1⦄ ⊢ U1 ¡[g].
-#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H
-@(sstas_ind … H) -U1 // -HT1 /4 width=5 by ygt_yprs_trans, sstas_yprs/
-qed-.
-
-fact sstas_ltpr_cprs_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
- ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ⬌* U2.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #L2 #HL12 #T2 #HT12 #U1 #H
-@(sstas_ind … H) -U1 [ /3 width=3/ ]
-#U1 #W1 #l1 #HTU1 #HUW1 * #U2 #HTU2 #HU12
-lapply (snv_ltpr_cprs_aux … IH2 … HT1 … HT12) // #HT2
-elim (snv_sstas_fwd_correct … HTU2) // #W2 #l2 #HUW2
-elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HUW1 … HUW2 … HU12) -IH2 -IH1 -HUW1 -HU12 //
-[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, ltpr_cprs_yprs/
-|3: /3 width=7 by snv_sstas_aux, ygt_yprs_trans, cprs_yprs/
-|4: /4 width=5 by ygt_yprs_trans, ltpr_cprs_yprs, sstas_yprs/
-|5: /3 width=4 by ygt_yprs_trans, cprs_yprs, sstas_yprs/
-] -L0 -T0 -T1 -HT2 #H #HW12 destruct /3 width=4/
-qed-.
-
-fact dxprs_ltpr_cprs_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
- ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 →
- ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L2 ⊢ U1 ➡* U2.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #L2 #HL12 #T2 #HT12
-elim (sstas_ltpr_cprs_aux … IH3 IH2 IH1 … H01 … HT12 … HTW1) // -L0 -T0 -T1 #W2 #HTW2 #HW12
-lapply (ltpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
-lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
-elim (cpcs_inv_cprs … H) -H /3 width=3/
-qed-.
-
-fact ssta_dxprs_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
- ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] →
- ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 →
- ∃∃U,U2. ⦃h, L1⦄ ⊢ U1 •*[g] U & ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U ⬌* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2
-elim (sstas_strip … HT1T … HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ]
-[ elim (ssta_ltpr_cprs_aux … IH2 IH1 … HTU1 L1 … HTT2) // -L0 -T0 -T /3 width=5/
-| @(ex3_2_intro …T2 HU1T) // /2 width=1/
-]
-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/dxprs_dxprs.ma".
-include "basic_2/dynamic/snv_cpcs.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Properties on context-free parallel reduction for local environments *****)
-
-fact snv_ltpr_tpr_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
- ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ltpr_tpr h g L1 T1.
-#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*]
-[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH4 -IH3 -IH2 -IH1 -L1
- >(tpr_inv_atom1 … H2) -X //
-| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2
- elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
- >(tpr_inv_atom1 … H2) -X
- elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
- elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
- lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1
- lapply (IH1 … HK12 … HV12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HLK1 /2 width=5/
-| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
- elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2
- elim (snv_inv_bind … H1) -H1 #HV1 #HT1
- elim (tpr_inv_bind1 … H2) -H2 *
- [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
- lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
- lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
- lapply (snv_ltpr_cpr_aux … HT1 (L2.ⓑ{I}V2) … T2 ?) -HT1
- [ /3 width=5 by cpr_intro, tps_tpss/ | /2 width=1/ | /3 width=1/ ] -IH1 -T0 /2 width=1/
- | #T2 #HT12 #HXT2 #H1 #H2 destruct
- lapply (IH1 … HT1 (L2.ⓓV1) … HT12) -IH1 -HT1 -HT12 [1,2: /2 width=1/ ] -HL12 #HT2
- lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/
- ]
-| #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct
- elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1
- elim (tpr_inv_appl1 … H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct -IH4
- lapply (IH1 … HV1 … HL12 … HV12) [ /2 width=1/ ] #HV2
- lapply (IH1 … HT1 … HL12 … HT12) [ /2 width=1/ ] #HT2
- elim (IH3 … HVW1 … HL12 … HV12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
- elim (dxprs_ltpr_cprs_aux … IH2 IH1 IH3 … HTU1 … HL12 T2) // [2: /3 width=1/ |3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #X #HTU2 #H
- elim (cprs_inv_abst1 Abst W1 … H) -H #W20 #U2 #HW120 #_ #H destruct
- lapply (ltpr_cprs_conf … HL12 … HW10) -L1 #HW10
- lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120
- lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20
- elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200
- lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/
- | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct
- elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
- elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
- lapply (cprs_div … HW10 … HW230) -W30 #HW120
- elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20
- elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #U10 #HWU10
- elim (ssta_ltpr_cpcs_aux … IH1 IH3 … HW20 … HWU10 … HWU20) // -IH3 -HWU10
- [2: /3 width=5/ |3: /2 width=1/
- |4: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
- ] #H #_ -IH2 -U10 destruct
- lapply (IH4 … HT20 (L1.ⓓV1) ?) [ /2 width=6/ | /2 width=1/ ] -U20 -W10 -l0 -IH4 -HT20 -HW20 #HT20
- lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
- lapply (IH1 … HT20 … (L2.ⓓV2) … HT202) [1,2: /2 width=1/ ] -L1 -V1 -W20 -T20 /2 width=1/
- | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct -IH4
- elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
- elim (dxprs_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
- elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
- lapply (ltpr_cprs_conf … HL12 … HW10) -HW10 #HW10
- elim (dxprs_ltpr_cprs_aux … IH2 IH1 IH3 … HTU0 (L2.ⓓW2) … T2 ?) // [2: /3 width=1/ |3,4: /2 width=1/ ] -IH2 -HTU0 #X #HTU2 #H
- elim (cprs_inv_abst1 Abst W3 … H) -H #W #U2 #HW1 #_ #H destruct -U3
- elim (IH3 … HVW1 … HL12 … HV10) // /2 width=1/ -IH3 -HVW1 #X #H1 #H2
- lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
- elim (lift_total X 0 1) #W20 #H3
- lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1/ -H1 #HVW20
- lapply (cpcs_lift (L2.ⓓW2) … H3 … HW13 H2) /2 width=1/ -HW13 -H3 -H2 #HW320
- lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
- elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
- lapply (dxprs_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) [ /2 width=1/ ] -HW3 -HTU2 #HTU2
- lapply (IH1 … HL12 … HW02) // [ /2 width=1/ ] -HW0 #HW2
- lapply (IH1 … HL12 … HV10) // [ /2 width=1/ ] -HV1 -HV10 #HV0
- lapply (IH1 … HT0 … (L2.ⓓW2) … HT02) [1,2: /2 width=1/ ] -L1 -HT02 -HW02 #HT2
- lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /2 width=1/ -HV0 -HV02 /3 width=8/
- ]
-| #W1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH2
- elim (snv_inv_cast … H1) -H1 #U1 #l #HW1 #HT1 #HTU1 #HUW1
- elim (tpr_inv_cast1 … H2) -H2
- [ * #W2 #T2 #HW12 #HT12 #H destruct
- lapply (cpcs_cprs_strap1 … HUW1 W2 ?) [ /3 width=1/ ] -HUW1 #H1
- lapply (IH1 … HL12 … HW12) // /2 width=1/ -HW1 -HW12 #HW2
- lapply (IH1 … HL12 … HT12) // /2 width=1/ -IH1 #HT2
- elim (IH3 … HTU1 … HL12 … HT12) // /2 width=1/ -IH3 -HT1 -HT12 -HTU1 #U2 #HTU2 #HU12
- lapply (ltpr_cpcs_conf … HL12 … H1) -L1 #H1
- lapply (cpcs_canc_sn … HU12 H1) -U1 /2 width=4/
- | #H -IH3 -HW1 -HTU1 -HUW1
- lapply (IH1 … HL12 … H) // /2 width=1/
- ]
-]
-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/equivalence/lsubss_ssta.ma".
-include "basic_2/dynamic/snv_cpcs.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Properties on context-free parallel reduction for local environments *****)
-
-fact ssta_ltpr_tpr_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
- ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_ltpr_tpr h g L1 T1.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *]
-[ #k #_ #_ #_ #X2 #l #H2 #L2 #HL12 #X3 #H3 -IH3 -IH2 -IH1
- elim (ssta_inv_sort1 … H2) -H2 #Hkl #H destruct
- >(tpr_inv_atom1 … H3) -X3 /4 width=6/
-| #i #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2
- elim (snv_inv_lref … H1) -H1 #I0 #K0 #V0 #H #HV1
- elim (ssta_inv_lref1 … H2) -H2 * #K1
- >(tpr_inv_atom1 … H3) -X3
- [ #V1 #W1 #HLK1 #HVW1 #HWU1
- lapply (ldrop_mono … H … HLK1) -H #H destruct
- lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
- elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
- elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
- elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HV12 // [2: /2 width=1/ ] -V1 #W2 #HVW2 #HW12
- lapply (ldrop_fwd_ldrop2 … HLK2) #H2
- elim (lift_total W2 0 (i+1)) #U2 #HWU2
- lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/
- | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct
- lapply (ldrop_mono … H … HLK1) -H #H destruct
- lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
- elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 #X #H #HLK2
- elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
- elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HK12 // [2: /2 width=1/ ] -HV1 -HKV1 #W2 #HVW2 #_ -W1
- elim (lift_total V2 0 (i+1)) #U2 #HVU2
- lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/
- ]
-| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
- elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2
- elim (snv_inv_bind … H1) -H1 #_ #HT1
- elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
- elim (tpr_inv_bind1 … H3) -H3 *
- [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
- lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02
- elim (ssta_ltpr_cpr_aux … HT1 … HTU1 (L2.ⓑ{I}V2) … T2) -HT1 -HTU1
- [2: /3 width=5 by cpr_intro, tps_tpss/ |3: /2 width=1/ |4: /3 width=1/ ] -IH1 -T0 -HL12 #U2 #HTU2 #HU12
- lapply (cpcs_bind2 … V1 … HU12 … a) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/
- | #T2 #HT12 #HT2 #H1 #H2 destruct
- elim (IH1 … HTU1 (L2.ⓓV1) … T2) -IH1 -HTU1 // [2,3: /2 width=1/ ] -T1 -HL12 #U2 #HTU2 #HU12
- lapply (cpcs_bind1 … HU12 … V1 … true) // -HU12 #HU12
- elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2
- lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/
- ]
-| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct
- elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10
- elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
- elim (tpr_inv_appl1 … H3) -H3 *
- [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2
- elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 #U2 #HTU2 #HU12
- lapply (cpcs_flat … V1 V2 … HU12) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/
- | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct
- elim (snv_inv_bind … HT1) -HT1 #HW #HT2
- elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct
- elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct
- lapply (cprs_div … HW10 … HW0) -W0 #HW1W
- elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #X1 #HWX1
- elim (snv_fwd_ssta … HW) #l1 #V #HWV
- lapply (IH3 … HVW1) -IH3 // [ /2 width=1/ ] #HW1
- elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HWX1 … HWV …) -IH2 -HWX1 //
- [2: /2 width=1/
- |3: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
- ] #H #_ destruct -X1
- elim (IH1 … HVW1 … HL12 … HV12) -HVW1 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
- elim (IH1 … HWV … HL12 W) -HWV // -HW [2: /2 width=1/ ] #V0 #HWV0 #_
- elim (IH1 … HTU2 (L2.ⓛW) … HT20) -IH1 -HTU2 -HT20 // [2,3: /2 width=1/ ] -HT2 #U20 #HTU20 #HU20
- lapply (ltpr_cpcs_conf … HL12 … HW1W) -L1 #HW1W
- lapply (cpcs_canc_sn … HW12 HW1W) -W1 #HW2
- elim (lsubss_ssta_trans … HTU20 (L2.ⓓV2) ?) -HTU20
- [ #U #HTU20 #HUU20 -HWV0 -W2
- @(ex2_intro … (ⓓ{b}V2.U)) [ /2 width=1/ ] -h -l -l1 -V -V0 -T2 -T20 -U0
- @(cpcs_cprs_strap2 … (ⓓ{b}V2.U2)) [ /3 width=1/ ] -V1
- @(cpcs_canc_dx … (ⓓ{b}V2.U20)) /2 width=2/
- | -b -l -V -V1 -T2 -T20 -U0 -U2 -U20 /2 width=6/
- ]
- | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct -a -l0 -W1 -W10 -HV1 -IH3 -IH2
- elim (ssta_inv_bind1 … HTU1) -HTU1 #U0 #HTU0 #H destruct
- elim (snv_inv_bind … HT1) -HT1 #_ #HT0
- elim (IH1 … HTU0 (L2.ⓓW2) … HT02) -IH1 -HTU0 // [2,3: /2 width=1/ ] -T0 -HL12 #U2 #HTU2 #HU02
- lapply (cpcs_bind2 … W0 … HU02 b) -HU02 [ /2 width=1/ ] #HU02
- lapply (cpcs_flat … V1 V0 … HU02 Appl) [ /2 width=1/ ] -HV10 -HU02 #HU02
- lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?) -HU02 [ /3 width=3/ ] -V0 -HW02 /4 width=3/
- ]
-| #U0 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2
- elim (snv_inv_cast … H1) -H1 #T0 #l0 #_ #HT1 #HT10 #_
- lapply (ssta_inv_cast1 … H2) -H2 #HTU1
- elim (ssta_mono … HT10 … HTU1) -HT10 #H1 #H2 destruct
- elim (tpr_inv_cast1 … H3) -H3
- [ * #U2 #T2 #_ #HT12 #H destruct
- elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 -U0 /3 width=3/
- | #HT1X3
- elim (IH1 … HTU1 … HL12 … HT1X3) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -U0 -T1 /2 width=3/
- ]
-]
-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 "ground_2/ynat/ynat_succ.ma".
-include "basic_2/notation/relations/iso_4.ma".
-include "basic_2/grammar/lenv_length.ma".
-
-(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
-
-inductive leq: ynat → ynat → relation lenv ≝
-| leq_atom: ∀d,e. leq d e (⋆) (⋆)
-| leq_zero: ∀I,L1,L2,V. leq 0 0 L1 L2 → leq 0 0 (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| leq_pair: ∀I1,I2,L1,L2,V1,V2,e.
- leq 0 e L1 L2 → leq 0 (⫯e) (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
-| leq_succ: ∀I,L1,L2,V,d,e. leq d e L1 L2 → leq (⫯d) e (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-.
-
-interpretation
- "equivalence (local environment)"
- 'Iso d e L1 L2 = (leq d e L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma leq_refl: ∀L,d,e. L ≃[d, e] L.
-#L elim L -L /2 width=1 by/
-#L #I #V #IHL #d #e elim (ynat_cases … d) [ | * /2 width=1 by leq_succ/ ]
-elim (ynat_cases … e) [ | * ]
-/2 width=1 by leq_zero, leq_pair/
-qed.
-
-lemma leq_sym: ∀L1,L2,d,e. L1 ≃[d, e] L2 → L2 ≃[d, e] L1.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-/2 width=1 by leq_atom, leq_zero, leq_pair, leq_succ/
-qed-.
-
-lemma leq_O_Y: ∀L1,L2. |L1| = |L2| → L1 ≃[0, ∞] L2.
-#L1 elim L1 -L1
-[ #X #H lapply (length_inv_zero_sn … H) -H //
-| #L1 #I1 #V1 #IHL1 #X #H elim (length_inv_pos_sn … H) -H
- #L2 #I2 #V2 #HL12 #H destruct
- @(leq_pair … (∞)) /2 width=1 by/ (**) (* explicit constructor *)
-]
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L1| = |L2|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize //
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact leq_inv_O2_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → e = 0 → L1 = L2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/
-#I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H elim (ysucc_inv_O_dx … H)
-qed-.
-
-lemma leq_inv_O2: ∀L1,L2,d. L1 ≃[d, 0] L2 → L1 = L2.
-/2 width=4 by leq_inv_O2_aux/ qed-.
-
-fact leq_inv_Y1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → d = ∞ → L1 = L2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/
-[ #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H destruct
-| #I #L1 #L2 #V #d #e #_ #IHL12 #H lapply (ysucc_inv_Y_dx … H) -H
- /3 width=1 by eq_f3/
-]
-qed-.
-
-lemma leq_inv_Y1: ∀L1,L2,e. L1 ≃[∞, e] L2 → L1 = L2.
-/2 width=4 by leq_inv_Y1_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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 ≃ break [ term 46 d , break term 46 e ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'Iso $d $e $L1 $L2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/ldrop_leq.ma".
-include "basic_2/relocation/lleq_lleq.ma".
-include "basic_2/reduction/cpx.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_cpx_trans_leq: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L1,d. L1 ⋕[d, T1] L2 → L1 ≃[d, ∞] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_sort/
-[ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #d #H #HL12 elim (lleq_inv_lref_dx … H … HLK2) -H *
- [ #K1 #HLK1 #HV1 #Hdi elim (ldrop_leq_conf_be … HL12 … HLK1) -HL12 /2 width=1 by yle_inj/
- >yminus_Y_inj #J #Y #X #HK12 #H lapply (ldrop_mono … H … HLK2) -L2
- #H destruct /3 width=7 by cpx_delta/
- | #J #K1 #V #HLK1 #_ #HV1 #Hid elim (ldrop_leq_conf_lt … HL12 … HLK1) -HL12 /2 width=1 by ylt_inj/
- <yminus_SO2 >yminus_inj #Y #HK12 #H lapply (ldrop_mono … H … HLK2) -L2
- #H destruct /3 width=7 by cpx_delta/
- ]
-| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_bind … H) -H
- /4 width=3 by cpx_bind, leq_succ/
-| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
- /3 width=3 by cpx_flat/
-| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #H elim (lleq_inv_bind … H) -H
- /4 width=3 by cpx_zeta, leq_succ/
-| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
- /3 width=3 by cpx_tau/
-| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #d #H elim (lleq_inv_flat … H) -H
- /3 width=3 by cpx_ti/
-| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
- #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_beta, leq_succ/
-| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
- #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_theta, leq_succ/
-]
-qed-.
-
-(* Note: this can be proved directly *)
-lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L1. L1 ⋕[0, T1] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
-/4 width=6 by lleq_cpx_trans_leq, lleq_fwd_length, leq_O_Y/ 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/substitution/lleq_alt.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀L1. L1 ⋕[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_sort/
+[ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2
+ [ #H elim (ylt_yle_false … H) //
+ | * /3 width=7 by cpx_delta/
+ ]
+| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H
+ /3 width=1 by cpx_bind/
+| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
+ /3 width=1 by cpx_flat/
+| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #H elim (lleq_inv_bind_O … H) -H
+ /3 width=3 by cpx_zeta/
+| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
+ /3 width=1 by cpx_tau/
+| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #H elim (lleq_inv_flat … H) -H
+ /3 width=1 by cpx_ti/
+| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
+ #HV1 #H elim (lleq_inv_bind_O … H) -H /3 width=1 by cpx_beta/
+| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
+ #HV1 #H elim (lleq_inv_bind_O … H) -H /3 width=3 by cpx_theta/
+]
+qed-.
+
+(* Note: lemma 1000 *)
+lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
+#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2
+[ //
+| /3 width=3 by lleq_fwd_length, lleq_sort/
+| #I2 #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_inv_lref_ge_dx … H … HLK2) // -H
+ #I1 #K1 #HLK1 #HV1
+ lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1
+ lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
+ @(lleq_lift_le … HLK1 HLK2 … HVW2) -HLK1 -HLK2 -HVW2 /2 width=1 by/ (**) (* full auto too slow *)
+| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H
+ /4 width=3 by lleq_bind_repl_SO, lleq_bind/
+| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
+ /3 width=1 by lleq_flat/
+| #G #L2 #V #T1 #T2 #T #_ #HT2 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H
+ /3 width=10 by lleq_inv_lift_le, ldrop_ldrop/
+| #G #L2 #V #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/
+| #G #L2 #V1 #V2 #T #_ #IHV12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/
+| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
+ #HV1 #H elim (lleq_inv_bind_O … H) -H
+ /4 width=3 by lleq_bind_repl_SO, lleq_flat, lleq_bind/
+| #a #G #L2 #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
+ #HV1 #H elim (lleq_inv_bind_O … H) -H
+ #HW1 #HT1 @lleq_bind_O /2 width=1 by/ @lleq_flat (**) (* full auto too slow *)
+ [ /3 width=10 by lleq_lift_le, ldrop_ldrop/
+ | /3 width=3 by lleq_bind_repl_O/
+]
+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/reduction/cpx_leq.ma".
-include "basic_2/reduction/lpx_ldrop.ma".
-
-(**) (* to be proved later *)
-axiom- lleq_beta: ∀L2s,L2d,V2,W2,T2,d.
- L2s.ⓛW2 ⋕[d+1, T2] L2d.ⓛW2 →
- L2s.ⓓⓝW2.V2 ⋕[d+1, T2] L2d.ⓓⓝW2.V2.
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties using equivalences for local environments *********************)
-
-(* Note: lemma 1000 *)
-lemma lleq_cpx_conf_leq_dx: ∀h,g,G,L1s,L1d,T1,d. L1s ⋕[d, T1] L1d → L1s ≃[d, ∞] L1d →
- ∀T2. ⦃G, L1d⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L2s. ⦃G, L1s⦄ ⊢ ➡[h, g] L2s → L1s ≃[0, d] L2s →
- ∀L2d. ⦃G, L1d⦄ ⊢ ➡[h, g] L2d → L1d ≃[0, d] L2d →
- L2s ≃[d, ∞] L2d → L2s ⋕[d, T2] L2d.
-#h #g #G #L1s #L1d #T1 #d #H elim H -L1s -L1d -T1 -d
-[ #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3
- lapply (leq_fwd_length … H3) -H3 #HL2sd
- elim (cpx_inv_sort1 … H2) -H2 [| * #l #_ ]
- #H destruct /2 width=1 by lleq_sort/
-| #Is #Id #L1s #L1d #K1s #K1d #V1s #V1d #d #i #Hid #HLK1s #HLK1d #_ #_ #_ #IHV1d #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
- elim (ldrop_leq_conf_lt … H1 … HLK1s) -H1 /2 width=1 by ylt_inj/
- <yminus_SO2 >yminus_inj #Y #H1 #HY
- lapply (ldrop_mono … HY … HLK1d) -HY #H destruct
- elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s
- elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct
- elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d
- elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct
- elim (ldrop_leq_conf_be … H2s … HLK1s) -H2s /2 width=1 by ylt_inj/
- >yplus_O1 <yminus_SO2 >yminus_inj #Z #Y #X #HK12s #H
- lapply (ldrop_mono … H … HLK2s) -H #H destruct
- elim (ldrop_leq_conf_be … H2d … HLK1d) -H2d /2 width=1 by ylt_inj/
- >yplus_O1 <yminus_SO2 >yminus_inj #Z #Y #X #HK12d #H
- lapply (ldrop_mono … H … HLK2d) -H #H destruct
- elim (ldrop_leq_conf_lt … H3 … HLK2s) -H3 /2 width=1 by ylt_inj/
- <yminus_SO2 >yminus_inj #Y #H3 #HY
- lapply (ldrop_mono … HY … HLK2d) -HY #H destruct
- elim (cpx_inv_lref1 … H2) -H2 -L1s
- [ -L1d #H destruct /3 width=15 by lleq_skip/
- | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d
- #H destruct >(plus_minus_m_m d (i+1)) //
- lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s
- lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d
- /3 width=9 by lleq_lift_ge/
- ]
-| #I #L1s #L1d #K1s #K1d #V1 #d #i #Hdi #HLK1s #HLK1d #_ #IHV1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
- elim (ldrop_leq_conf_be … H1 … HLK1s) -H1 /2 width=1 by ylt_Y, yle_inj/ #Z #Y #X #H1 #HY
- lapply (ldrop_mono … HY … HLK1d) -HY #H destruct
- elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s
- elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct
- elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d
- elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct
- lapply (ldrop_leq_conf_ge … H2s … HLK1s ?) /2 width=1 by yle_inj/ #H
- lapply (ldrop_mono … H … HLK2s) -H #H destruct
- lapply (ldrop_leq_conf_ge … H2d … HLK1d ?) /2 width=1 by yle_inj/ #H
- lapply (ldrop_mono … H … HLK2d) -H #H destruct
- elim (ldrop_leq_conf_be … H3 … HLK2s) -H3 /2 width=1 by ylt_Y, yle_inj/
- >yminus_Y_inj #Z #Y #X #H3 #HY
- lapply (ldrop_mono … HY … HLK2d) -HY #H destruct
- elim (cpx_inv_lref1 … H2) -H2 -L1s
- [ -L1d #H destruct /3 width=12 by lleq_lref/
- | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d
- #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s #HLK2s
- lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d #HLK2d
- @(lleq_ge … 0) /3 width=10 by lleq_lift_le/ (**) (* full auto too slow *)
- ]
-| #L1s #L1d #d #i #HL1s #HL1d #_ #_ #X #H2 #L2s #_ #_ #L2s #_ #H2d #H3
- lapply (leq_fwd_length … H2d) -H2d
- lapply (leq_fwd_length … H3) -H3
- elim (cpx_inv_lref1 … H2) -H2
- [ #H destruct /2 width=1 by lleq_free/
- | -L1s * #I #K1d #V1 #V2 #HLK1d
- lapply (ldrop_fwd_length_lt2 … HLK1d) -HLK1d #H
- elim (lt_refl_false … i) /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
- ]
-| #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3
- lapply (leq_fwd_length … H3) -H3 #HL2sd
- lapply (cpx_inv_gref1 … H2) -H2
- #H destruct /2 width=1 by lleq_gref/
-| #a #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
- elim (cpx_inv_bind1 … H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct
- /5 width=5 by lpx_pair, lleq_cpx_trans_leq, lleq_bind, leq_pair, leq_succ/
- | #T2 #HT12 #HT2X #H1 #H2 destruct >(minus_plus_m_m d 1)
- /4 width=9 by lpx_pair, lleq_inv_lift_ge, ldrop_ldrop, leq_pair, leq_succ/
- ]
-| #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
- elim (cpx_inv_flat1 … H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by lleq_flat/
- | #HT1X #H destruct /2 width=1 by/
- | #HV1X #H destruct /2 width=1 by/
- | #a #V2 #W1 #W2 #T0 #T2 #HV12 #HW12 #HT02 #H1 #H2 #H3 destruct
- lapply (IHT1 … (ⓛ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H
- elim (lleq_inv_bind … H) -H -HW12 -HT02 #HW2 #HT2
- /4 width=1 by lleq_beta, lleq_flat, lleq_bind/
- | #a #V0 #V2 #W1 #W2 #T0 #T2 #HV10 #HV02 #HW12 #HT02 #H1 #H2 #H3 destruct
- lapply (IHT1 … (ⓓ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H
- elim (lleq_inv_bind … H) -H -HW12 -HT02
- /5 width=9 by lleq_lift_ge, lleq_flat, lleq_bind, ldrop_ldrop/
- ]
-]
-qed-.
-
-lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2.
-#h #g #G #L2 #T1 #T2 #HT12 #L1 #HT1 lapply (lleq_fwd_length … HT1)
-/3 width=13 by lleq_cpx_conf_leq_dx, leq_O_Y/
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/relocation/lleq_lleq.ma".
+include "basic_2/substitution/lleq_alt.ma".
include "basic_2/reduction/lpx_ldrop.ma".
(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
(* Properties on lazy equivalence for local environments ********************)
lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[0, T1] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[0, T2] L2.
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1
#K0 #V0 #H1KL1 #_ #H destruct
elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 //
- #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
+ #I1 #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct
/2 width=4 by fqu_lref_O, ex3_intro/
| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H
[ elim (lleq_inv_bind … H)
qed-.
lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[0, T1] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[0, T2] L2.
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
elim (fquq_inv_gen … H) -H
[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
qed-.
lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[0, T1] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[0, T2] L2.
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1
/3 width=4 by fqu_fqup, ex3_intro/
qed-.
lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[0, T1] L1 →
- ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[0, T2] L2.
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 →
+ ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1
elim (fqus_inv_gen … H) -H
[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/lleq_lleq.ma".
-include "basic_2/relocation/fqu.ma".
-
-(* SUPCLOSURE ***************************************************************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ →
- ∀L1. L1 ⋕[0, T] L2 →
- ∃∃K1. ⦃G1, L1, T⦄ ⊃ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2.
-#G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
-[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H //
- #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1
- #H destruct /2 width=3 by fqu_lref_O, ex2_intro/
-| * [ #a ] #I #G #L2 #V #T #L1 #H
- [ elim (lleq_inv_bind … H)
- | elim (lleq_inv_flat … H)
- ] -H
- /2 width=3 by fqu_pair_sn, ex2_intro/
-| #a #I #G #L2 #V #T #L1 #H elim (lleq_inv_bind_O … H) -H
- #H3 #H4 /2 width=3 by fqu_bind_dx, ex2_intro/
-| #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H
- /2 width=3 by fqu_flat_dx, ex2_intro/
-| #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12
- elim (ldrop_O1_le (e+1) L1)
- [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
- | lapply (ldrop_fwd_length_le2 … HLK2) -K2
- lapply (lleq_fwd_length … HL12) -T -U //
- ]
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/fqu_lleq.ma".
-include "basic_2/relocation/fquq_alt.ma".
-
-(* OPTIONAL SUPCLOSURE ******************************************************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃⸮ ⦃G2, K2, U⦄ →
- ∀L1. L1 ⋕[0, T] L2 →
- ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2.
-#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H
-[ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/
-| * #HG #HL #HT destruct /2 width=3 by ex2_intro/
-]
-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 "ground_2/ynat/ynat_plus.ma".
-include "basic_2/grammar/leq.ma".
-include "basic_2/relocation/ldrop.ma".
-
-(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
-
-lemma ldrop_leq_conf_ge: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
- ∀I,K,V,i. ⇩[O, i]L1 ≡ K.ⓑ{I}V → d + e ≤ i →
- ⇩[O, i]L2 ≡ K.ⓑ{I}V.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #d #e #J #K #W #i #H elim (ldrop_inv_atom1 … H) -H
- #H destruct
-| #I #L1 #L2 #V #HL12 #IHL12 #J #K #W #i #H #_ elim (ldrop_inv_O1_pair1 … H) -H
- * #H1 #H2
- [ -IHL12 lapply (leq_inv_O2 … HL12) -HL12
- #H3 destruct //
- | -HL12 /4 width=1 by ldrop_ldrop_lt, yle_inj/
- ]
-| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #IHL12 #J #K #W #i #H1 >yplus_succ_swap
- #Hei elim (yle_inv_inj2 … Hei) -Hei
- #x #Hei #H elim (yplus_inv_inj … H) -H normalize
- #y #z >commutative_plus
- #H1 #H2 #H3 destruct elim (le_inv_plus_l … Hei) -Hei
- #Hzi #Hi lapply (ldrop_inv_ldrop1_lt … H1 ?) -H1
- /4 width=1 by ldrop_ldrop_lt, yle_inj/
-| #I #L1 #L2 #V #d #e #_ #IHL12 #J #K #W #i #H0 #Hdei elim (yle_inv_inj2 … Hdei) -Hdei
- #x #Hdei #H elim (yplus_inv_inj … H) -H
- #y #z >commutative_plus
- #H1 #H2 #H3 destruct elim (ysucc_inv_inj_dx … H2) -H2
- #x #H1 #H2 destruct elim (le_inv_plus_l … Hdei)
- #_ #Hi lapply (ldrop_inv_ldrop1_lt … H0 ?) -H0
- [2: #H0 @ldrop_ldrop_lt ] [2,3: /2 width=3 by lt_to_le_to_lt/ ]
- /4 width=3 by yle_inj, monotonic_pred/
-]
-qed-.
-
-lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
- ∀I1,K1,V1,i. ⇩[O, i]L1 ≡ K1.ⓑ{I1}V1 → d ≤ i → i < d + e →
- ∃∃I2,K2,V2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I2}V2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H
- #H destruct
-| #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) //
-| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O1 >yplus_O1
- #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
- [ #_ lapply (ldrop_inv_O2 … H) -H
- #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/
- | lapply (ldrop_inv_ldrop1_lt … H ?) -H //
- #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/
- #Hie lapply (ylt_inv_succ … Hie) -Hie
- #Hie elim (IHL12 … H) -IHL12 -H //
- >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/
- ]
-| #I #L1 #L2 #V #d #e #_ #IHL12 #J1 #K1 #W1 #i #H #Hdi lapply (ylt_yle_trans 0 … Hdi ?) //
- #Hi <(ylt_inv_O1 … Hi) >yplus_succ1 >yminus_succ elim (yle_inv_succ1 … Hdi) -Hdi
- #Hdi #_ #Hide lapply (ylt_inv_succ … Hide)
- #Hide lapply (ylt_inv_inj … Hi) -Hi
- #Hi lapply (ldrop_inv_ldrop1_lt … H ?) -H //
- #H elim (IHL12 … H) -IHL12 -H
- /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/
-]
-qed-.
-
-lemma ldrop_leq_conf_lt: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
- ∀I,K1,V,i. ⇩[O, i]L1 ≡ K1.ⓑ{I}V → i < d →
- ∃∃K2. K1 ≃[⫰(d-i), e] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I}V.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #d #e #J #K1 #W #i #H elim (ldrop_inv_atom1 … H) -H
- #H destruct
-| #I #L1 #L2 #V #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) //
-| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) //
-| #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K1 #W #i #H elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
- [ #_ lapply (ldrop_inv_O2 … H) -H
- #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_intro/
- | lapply (ldrop_inv_ldrop1_lt … H ?) -H //
- #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/
- #Hie lapply (ylt_inv_succ … Hie) -Hie
- #Hie elim (IHL12 … H) -IHL12 -H
- >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_intro/
- ]
-]
-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/lazyeq_4.ma".
-include "basic_2/relocation/ldrop.ma".
-
-(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
-
-inductive lleq: nat → term → relation lenv ≝
-| lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → lleq d (⋆k) L1 L2
-| lleq_skip: ∀I1,I2,L1,L2,K1,K2,V1,V2,d,i. i < d →
- ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 →
- lleq (d-i-1) V1 K1 K2 → lleq (d-i-1) V2 K1 K2 → lleq d (#i) L1 L2
-| lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ i →
- ⇩[0, i] L1 ≡ K1.ⓑ{I}V → ⇩[0, i] L2 ≡ K2.ⓑ{I}V →
- lleq 0 V K1 K2 → lleq d (#i) L1 L2
-| lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → lleq d (#i) L1 L2
-| lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → lleq d (§p) L1 L2
-| lleq_bind: ∀a,I,L1,L2,V,T,d.
- lleq d V L1 L2 → lleq (d+1) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
- lleq d (ⓑ{a,I}V.T) L1 L2
-| lleq_flat: ∀I,L1,L2,V,T,d.
- lleq d V L1 L2 → lleq d T L1 L2 → lleq d (ⓕ{I}V.T) L1 L2
-.
-
-interpretation
- "lazy equivalence (local environment)"
- 'LazyEq d T L1 L2 = (lleq d T L1 L2).
-
-(* Basic_properties *********************************************************)
-
-lemma lleq_sym: ∀d,T. symmetric … (lleq d T).
-#d #T #L1 #L2 #H elim H -d -T -L1 -L2
-/2 width=10 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
-qed-.
-
-(* Note this is: "∀d,T. reflexive … (lleq d T)" *)
-axiom lleq_refl: ∀T,L,d. L ⋕[d, T] L.
-(*
-#T #L @(f2_ind … rfw … L T) -L -T
-#n #IH #L * * /3 width=1 by lleq_sort, lleq_gref, lleq_bind, lleq_flat/
-#i #H elim (lt_or_ge i (|L|)) /2 width=1 by lleq_free/
-#HiL #d elim (lt_or_ge i d) /2 width=1 by lleq_skip/
-elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=7 by lleq_lref, ldrop_fwd_rfw/
-qed.
-*)
-
-lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[d1, T] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[d2, T] L2.
-#L1 #L2 #T #d1 #H elim H -L1 -L2 -T -d1
-/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, le_S_S/
-[ /5 width=10 by lleq_skip, lt_to_le_to_lt, monotonic_le_minus_l, monotonic_pred/ (**) (* a bit slow *)
-| #I #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (lt_or_ge i d2)
- [ -d1 /3 width=10 by lleq_skip/
- | /3 width=7 by lleq_lref, transitive_le/
- ]
-]
-qed-.
-
-lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[0, V] L2 → L1.ⓑ{I}V ⋕[0, T] L2.ⓑ{I}V →
- L1 ⋕[0, ⓑ{a,I}V.T] L2.
-/3 width=3 by lleq_ge, lleq_bind/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lleq_inv_lref_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀i. X = #i →
- ∨∨ |L1| ≤ i ∧ |L2| ≤ i
- | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 &
- ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 &
- K1 ⋕[d-i-1, V1] K2 &
- K1 ⋕[d-i-1, V2] K2 &
- i < d
- | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
- ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
- K1 ⋕[0, V] K2 & d ≤ i.
-#d #X #L1 #L2 * -d -X -L1 -L2
-[ #L1 #L2 #d #k #_ #j #H destruct
-| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hid #HLK1 #HLK2 #HV1 #HV2 #j #H destruct /3 width=10 by or3_intro1, ex5_6_intro/
-| #I #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #HK12 #j #H destruct /3 width=7 by or3_intro2, ex4_4_intro/
-| #L1 #L2 #d #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or3_intro0, conj/
-| #L1 #L2 #d #p #_ #j #H destruct
-| #a #I #L1 #L2 #V #T #d #_ #_ #j #H destruct
-| #I #L1 #L2 #V #T #d #_ #_ #j #H destruct
-]
-qed-.
-
-lemma lleq_inv_lref: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 →
- ∨∨ |L1| ≤ i ∧ |L2| ≤ i
- | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 &
- ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 &
- K1 ⋕[d-i-1, V1] K2 &
- K1 ⋕[d-i-1, V2] K2 &
- i < d
- | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
- ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
- K1 ⋕[0, V] K2 & d ≤ i.
-/2 width=3 by lleq_inv_lref_aux/ qed-.
-
-fact lleq_inv_bind_aux: ∀d,X,L1,L2. L1 ⋕[d,X] L2 → ∀a,I,V,T. X = ⓑ{a,I}V.T →
- L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V.
-#d #X #L1 #L2 * -d -X -L1 -L2
-[ #L1 #L2 #d #k #_ #b #J #W #U #H destruct
-| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #b #J #W #U #H destruct
-| #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #b #J #W #U #H destruct
-| #L1 #L2 #d #i #_ #_ #_ #b #J #W #U #H destruct
-| #L1 #L2 #d #p #_ #b #J #W #U #H destruct
-| #a #I #L1 #L2 #V #T #d #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/
-| #I #L1 #L2 #V #T #d #_ #_ #b #J #W #U #H destruct
-]
-qed-.
-
-lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ⋕[d, ⓑ{a,I}V.T] L2 →
- L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V.
-/2 width=4 by lleq_inv_bind_aux/ qed-.
-
-fact lleq_inv_flat_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀I,V,T. X = ⓕ{I}V.T →
- L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2.
-#d #X #L1 #L2 * -d -X -L1 -L2
-[ #L1 #L2 #d #k #_ #J #W #U #H destruct
-| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #J #W #U #H destruct
-| #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #J #W #U #H destruct
-| #L1 #L2 #d #i #_ #_ #_ #J #W #U #H destruct
-| #L1 #L2 #d #p #_ #J #W #U #H destruct
-| #a #I #L1 #L2 #V #T #d #_ #_ #J #W #U #H destruct
-| #I #L1 #L2 #V #T #d #HV #HT #J #W #U #H destruct /2 width=1 by conj/
-]
-qed-.
-
-lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[d, ⓕ{I}V.T] L2 →
- L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2.
-/2 width=4 by lleq_inv_flat_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → |L1| = |L2|.
-#L1 #L2 #T #d #H elim H -L1 -L2 -T -d //
-[ #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #HLK1 #HLK2 #_ #_ #HK12 #_
-| #I #L1 #L2 #K1 #K2 #V #d #i #_ #HLK1 #HLK2 #_ #IHK12
-]
-lapply (ldrop_fwd_length … HLK1) -HLK1
-lapply (ldrop_fwd_length … HLK2) -HLK2
-normalize //
-qed-.
-
-lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 →
- ∃K2. ⇩[0, i] L2 ≡ K2.
-#L1 #L2 #T #d #H #K1 #i #HLK1 lapply (lleq_fwd_length … H) -H
-#HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/
-qed-.
-
-lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[0, i] L2 ≡ K2 →
- ∃K1. ⇩[0, i] L1 ≡ K1.
-/3 width=6 by lleq_fwd_ldrop_sn, lleq_sym/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/ldrop_ldrop.ma".
-include "basic_2/relocation/lleq.ma".
-
-(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma lleq_inv_lref_dx: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 →
- ∀I,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I}V →
- (∃∃K1. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[0, V] K2 & d ≤ i) ∨
- ∃∃I1,K1,V1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 &
- K1 ⋕[d-i-1, V1] K2 & K1 ⋕[d-i-1, V] K2 &
- i < d.
-#L1 #L2 #d #i #H #I #K2 #V #HLK2 elim (lleq_inv_lref … H) -H *
-[ #_ #H elim (lt_refl_false i)
- lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2
- /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
-| #I1 #I2 #K11 #K22 #V1 #V2 #HLK11 #HLK22 #HV1 #HV2 #Hdi lapply (ldrop_mono … HLK22 … HLK2) -L2
- #H destruct /3 width=6 by ex4_3_intro, or_intror/
-| #I0 #K1 #K0 #V0 #HLK1 #HLK0 #HK10 #Hdi lapply (ldrop_mono … HLK0 … HLK2) -L2
- #H destruct /3 width=3 by ex3_intro, or_introl/
-]
-qed-.
-
-lemma lleq_inv_lref_sn: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 →
- ∀I,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V →
- (∃∃K2. ⇩[0, i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[0, V] K2 & d ≤ i) ∨
- ∃∃I2,K2,V2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 &
- K1 ⋕[d-i-1, V] K2 & K1 ⋕[d-i-1, V2] K2 &
- i < d.
-#L1 #L2 #d #i #HL12 #I #K1 #V #HLK1 elim (lleq_inv_lref_dx L2 … d … HLK1) -HLK1
-[1,2: * ] /4 width=6 by lleq_sym, ex4_3_intro, ex3_intro, or_introl, or_intror/
-qed-.
-
-lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → d ≤ i →
- ∀I,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I}V →
- ∃∃K1. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[0, V] K2.
-#L1 #L2 #d #i #H #Hdi #I #K2 #V #HLK2 elim (lleq_inv_lref … H) -H *
-[ #_ #H elim (lt_refl_false i)
- lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2
- /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
-| -HLK2 #I1 #I2 #K11 #K22 #V1 #V2 #_ #_ #_ #_ #H elim (lt_refl_false i)
- /2 width=3 by lt_to_le_to_lt/
-| #I0 #K1 #K0 #V0 #HLK1 #HLK0 #HK10 #_ lapply (ldrop_mono … HLK0 … HLK2) -L2
- #H destruct /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → d ≤ i →
- ∀I,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V →
- ∃∃K2. ⇩[0, i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[0, V] K2.
-#L1 #L2 #d #i #HL12 #Hdi #I #K1 #V #HLK1 elim (lleq_inv_lref_ge_dx L2 … Hdi … HLK1) -Hdi -HLK1
-/3 width=3 by lleq_sym, ex2_intro/
-qed-.
-
-fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[d0, T] L2 → ∀d. d0 = d + 1 →
- ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V →
- L1 ⋕[d, T] L2.
-#L1 #L2 #T #d0 #H elim H -L1 -L2 -T -d0
-/2 width=1 by lleq_sort, lleq_free, lleq_gref/
-[ #I1 #I2 #L1 #L2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HLK11 #HLK22 #HV1 #_ #IHV1 #IHV2 #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
- elim (le_to_or_lt_eq i d) /2 width=1 by lleq_skip, monotonic_pred/ -Hid0
- [ -HV1 #Hid
- lapply (ldrop_fwd_ldrop2 … HLK11) #H1
- lapply (ldrop_fwd_ldrop2 … HLK22) #H2
- lapply (ldrop_conf_ge … H1 … HLK1 ?) // -H1 -HLK1
- lapply (ldrop_conf_ge … H2 … HLK2 ?) // -H2 -HLK2
- <minus_plus /4 width=10 by lleq_skip, arith_i/
- | -IHV1 -IHV2 #H destruct
- lapply (ldrop_mono … HLK11 … HLK1) -HLK11 #H destruct
- lapply (ldrop_mono … HLK22 … HLK2) -HLK22 #H destruct
- /2 width=7 by lleq_lref/
- ]
-| #I #L1 #L2 #K11 #K22 #V #d0 #i #Hid0 #HLK11 #HLK22 #HV #_ #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
- /3 width=7 by lleq_lref, lt_to_le/
-| #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
- /4 width=6 by lleq_bind, ldrop_ldrop/
-| #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
- /3 width=6 by lleq_flat/
-]
-qed-.
-
-lemma lleq_inv_S: ∀T,L1,L2,d. L1 ⋕[d+1, T] L2 →
- ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V →
- L1 ⋕[d, T] L2.
-/2 width=6 by lleq_inv_S_aux/ qed-.
-
-lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[0, ⓑ{a,I}V.T] L2 →
- L1 ⋕[0, V] L2 ∧ L1.ⓑ{I}V ⋕[0, T] L2.ⓑ{I}V.
-#a #I #L1 #L2 #V #T #H elim (lleq_inv_bind … H) -H
-/3 width=6 by ldrop_pair, conj, lleq_inv_S/
-qed-.
-
-lemma lleq_inv_lift_le: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 →
- ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
- ∀T. ⇧[d, e] T ≡ U → d0 ≤ d → K1 ⋕[d0, T] K2.
-#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
-[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X
- lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e
- /2 width=1 by lleq_sort/
-| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HW1 #HW2 #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H
- * #Hid #H destruct [ -HW1 -HW2 | -IHW1 -IHW2 ]
- [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1
- elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2
- #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1
- @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 /3 width=6 by monotonic_le_minus_l2/ (**) (* full auto fails *)
- | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
- lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -Hid -L2
- #HK22 #HK11 @(lleq_skip … HK11 HK22) -HK11 -HK22
- /2 width=3 by lleq_ge, le_to_lt_to_lt/ (**) (* full auto fails *)
- ]
-| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #IHW #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H
- * #Hid #H destruct [ -HW | -IHW ]
- [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 #L1 #V #HKL1 #KL11 #HVW
- elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2 #L2 #V0 #HKL2 #KL22 #HV0
- lapply (lift_inj … HV0 … HVW) -HV0 #H destruct /3 width=12 by lleq_lref/
- | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
- lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0
- elim (le_inv_plus_l … Hid) -Hid /3 width=7 by lleq_lref, transitive_le/
- ]
-| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H
- * #_ #H destruct
- lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12)
- [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1
- lapply (ldrop_fwd_length_le4 … HLK2) -HLK2
- #HKL2 #HKL1 #HK12 @lleq_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *)
- | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H
- lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H
- /3 width=1 by lleq_free, le_plus_to_minus_r/
- ]
-| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X
- lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e
- /2 width=1 by lleq_gref/
-| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind2 … H) -H
- #V #T #HVW #HTU #H destruct /4 width=6 by lleq_bind, ldrop_skip, le_S_S/
-| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat2 … H) -H
- #V #T #HVW #HTU #H destruct /3 width=6 by lleq_flat/
-]
-qed-.
-
-lemma lleq_inv_lift_ge: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 →
- ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
- ∀T. ⇧[d, e] T ≡ U → d+e ≤ d0 → K1 ⋕[d0-e, T] K2.
-#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
-[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X
- lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d
- /2 width=1 by lleq_sort/
-| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HW1 #HW2 #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H
- * #Hid #H destruct [ -HW1 -HW2 | -IHW1 -IHW2 ]
- [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1
- elim (ldrop_conf_lt … HLK2 … HLK22) // -L2
- elim (le_inv_plus_l … Hded0) #Hdd0e #_
- #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1
- @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 [ /2 width=3 by lt_to_le_to_lt/ ] (**) (* explicit constructor *)
- >minus_minus_comm3 /3 width=6 by arith_k_sn/ (**) (* slow *)
- | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
- lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0
- elim (le_inv_plus_l … Hid) -Hid #_ #Hei
- #HK22 #HK11 @(lleq_skip … HK11 HK22) -HK11 -HK22 (**) (* explicit constructor *)
- [ /2 width=1 by monotonic_lt_minus_l/ ] >arith_b1 //
- ]
-| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H
- * #Hid #H destruct
- [ -I -L1 -L2 -K11 -K22 -W elim (le_plus_xySz_x_false e 0 d)
- /3 width=3 by transitive_le, le_to_lt_to_lt/
- | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
- lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0
- /3 width=7 by lleq_lref, monotonic_le_minus_l/
- ]
-| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H
- * #_ #H destruct
- lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12)
- [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1
- lapply (ldrop_fwd_length_le4 … HLK2) -HLK2
- #HKL2 #HKL1 #HK12 @lleq_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *)
- | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H
- lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H
- /3 width=1 by lleq_free, le_plus_to_minus_r/
- ]
-| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X
- lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d
- /2 width=1 by lleq_gref/
-| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_bind2 … H) -H
- #V #T #HVW #HTU #H destruct
- elim (le_inv_plus_l … Hded0) #_ #Hed0
- @lleq_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *)
- >plus_minus /3 width=5 by ldrop_skip, le_minus_to_plus/
-| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_flat2 … H) -H
- #V #T #HVW #HTU #H destruct /3 width=5 by lleq_flat/
-]
-qed-.
-
-lemma lleq_inv_lift_be: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 →
- ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
- ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ d + e → K1 ⋕[d, T] K2.
-#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
-[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_sort2 … H) -X
- lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e
- /2 width=1 by lleq_sort/
-| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #_ #_ #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H
- * #Hid #H destruct
- [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1
- elim (ldrop_conf_lt … HLK2 … HLK22) // -L2 -Hid0
- #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1
- @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 //
- /3 width=6 by arith_k_dx, monotonic_le_minus_l2/ (**) (* full auto fails *)
- | -I1 -I2 -L1 -L2 -K11 -K22 -W1 -W2 -Hd0 elim (lt_refl_false i)
- /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *)
- ]
-| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H
- * #Hid #H destruct
- [ -I -L1 -L2 -K11 -K22 -W -Hde elim (lt_refl_false i)
- /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *)
- | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1
- lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 -Hd0 -Hde
- elim (le_inv_plus_l … Hid) -Hid /2 width=7 by lleq_lref/
- ]
-| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H
- * #_ #H destruct
- lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12)
- [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1
- lapply (ldrop_fwd_length_le4 … HLK2) -HLK2
- #HKL2 #HKL1 #HK12 @lleq_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *)
- | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H
- lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H
- /3 width=1 by lleq_free, le_plus_to_minus_r/
- ]
-| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_gref2 … H) -X
- lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e
- /2 width=1 by lleq_gref/
-| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_bind2 … H) -H
- #V #T #HVW #HTU #H destruct
- @lleq_bind [ /2 width=5 by/ ] -IHW
- @(IHU … HTU) -IHU -HTU /2 width=1 by ldrop_skip, le_S_S/ (**) (* full auto too slow *)
-| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_flat2 … H) -H
- #V #T #HVW #HTU #H destruct /3 width=6 by lleq_flat/
-]
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma lleq_lift_le: ∀K1,K2,T,d0. K1 ⋕[d0, T] K2 →
- ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
- ∀U. ⇧[d, e] T ≡ U → d0 ≤ d → L1 ⋕[d0, U] L2.
-#K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0
-[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X
- lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
- /2 width=1 by lleq_sort/
-| #I1 #I2 #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #_ #_ #IHV1 #IHV2 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
- * #Hdi #H destruct
- [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1
- elim (ldrop_trans_lt … HLK2 … HK22) // -K2
- #K2 #W2 #HLK2 #HK22 #HVW2 #K1 #W1 #HLK1 #HK11 #HVW1 -Hdi
- @(lleq_skip … HLK1 HLK2) // /3 width=6 by monotonic_le_minus_l2/ (**) (* full auto fails *)
- | elim (lt_refl_false i) -I1 -I2 -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -e
- /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *)
- ]
-| #I #K1 #K2 #K11 #K22 #V #d0 #i #Hid0 #HK11 #HK22 #HV #IHV #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
- * #Hdi #H destruct [ -HV | -IHV ]
- [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 #K1 #W #HLK1 #HK11 #HVW
- elim (ldrop_trans_lt … HLK2 … HK22) // -Hdi -K2 #K2 #W2 #HLK2 #HK22 #HVW2
- lapply (lift_mono … HVW2 … HVW) -HVW2 #H destruct /3 width=12 by lleq_lref/
- | lapply (ldrop_trans_ge … HLK1 … HK11 ?) // -K1
- lapply (ldrop_trans_ge … HLK2 … HK22 ?) // -Hdi -K2
- /3 width=7 by lleq_lref, transitive_le/
- ]
-| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
- * #Hid #H destruct
- lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12
- [ /3 width=6 by lleq_free, ldrop_fwd_be/
- | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
- lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2
- @lleq_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *)
- ]
-| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X
- lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d -e
- /2 width=1 by lleq_gref/
-| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H
- #W #U #HVW #HTU #H destruct /4 width=6 by lleq_bind, ldrop_skip, le_S_S/
-| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H
- #W #U #HVW #HTU #H destruct /3 width=6 by lleq_flat/
-]
-qed-.
-
-lemma lleq_lift_ge: ∀K1,K2,T,d0. K1 ⋕[d0, T] K2 →
- ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
- ∀U. ⇧[d, e] T ≡ U → d ≤ d0 → L1 ⋕[d0+e, U] L2.
-#K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0
-[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X
- lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
- /2 width=1 by lleq_sort/
-| #I1 #I2 #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #hid0 #HK11 #HK22 #HV1 #HV2 #IHV1 #IHV2 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
- * #Hdi #H destruct [ -HV1 -HV2 | -IHV1 -IHV2 ]
- [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 #K1 #W1 #HLK1 #HK11 #HVW1
- elim (ldrop_trans_lt … HLK2 … HK22) // -K2 #K2 #W2 #HLK2 #HK22 #HVW2
- @(lleq_skip … HLK1 HLK2) -HLK1 -HLK2 (**) (* explicit constructor *)
- [ /2 width=3 by lt_to_le_to_lt/ ]
- >arith_i /3 width=5 by monotonic_le_minus_l2/
- | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1
- lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -K2
- /4 width=10 by lleq_skip, monotonic_lt_plus_l/
- ]
-| #I #K1 #K2 #K11 #K22 #V #d0 #i #Hid0 #HK11 #HK22 #HV #_ #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
- * #Hid #H destruct
- [ elim (lt_refl_false i) -I -L1 -L2 -K1 -K2 -K11 -K22 -V -e
- /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *)
- | lapply (ldrop_trans_ge … HLK1 … HK11 ?) // -K1
- lapply (ldrop_trans_ge … HLK2 … HK22 ?) // -Hid -K2
- /3 width=7 by lleq_lref, monotonic_le_plus_l/
- ]
-| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H
- * #Hid #H destruct
- lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12
- [ /3 width=6 by lleq_free, ldrop_fwd_be/
- | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
- lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2
- @lleq_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *)
- ]
-| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X
- lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d
- /2 width=1 by lleq_gref/
-| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H
- #W #U #HVW #HTU #H destruct /4 width=5 by lleq_bind, ldrop_skip, le_minus_to_plus/
-| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H
- #W #U #HVW #HTU #H destruct /3 width=5 by lleq_flat/
-]
-qed-.
-
-lemma lleq_be: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 →
- ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
- ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ d + e → L1 ⋕[d, U] L2.
-#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
-/2 width=1 by lleq_sort, lleq_free, lleq_gref/
-[ #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #_ #_ #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0de elim (lift_inv_lref2 … H) -H
- * #Hid #H destruct [ -Hid0 | -Hd0 ]
- [ elim (ldrop_conf_lt … HLK1 … HLK11) // -HLK1
- elim (ldrop_conf_lt … HLK2 … HLK22) // -HLK2
- #L2 #V2 #_ #HKL22 #HVW2 #L1 #V1 #_ #HKL21 #HVW1
- @(lleq_skip … HLK11 HLK22) -HLK11 -HLK22 //
- /3 width=8 by arith_k_dx, monotonic_le_minus_l2/ (**) (* full auto fails *)
- | -I1 -I2 -K11 -K22 -K1 -K2 -W1 -W2 elim (lt_refl_false … i) -L1 -L2
- @(lt_to_le_to_lt … Hid0) -Hid0 /2 width=3 by transitive_le/ (**) (* full auto too slow *)
- ]
-| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #_ #_ #X #H #Hd0 #_ elim (lift_inv_lref2 … H) -H
- * #Hid #H destruct
- [ -I -K1 -K2 -K11 -K22 -W elim (lt_refl_false i)
- @(lt_to_le_to_lt … Hid) -Hid /2 width=3 by transitive_le/ (**) (* full auto too slow *)
- | -d0 /3 width=7 by lleq_lref, le_plus_b/
- ]
-| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_bind2 … H) -H
- #V #T #HVW #HTU #H destruct
- @lleq_bind [ /2 width=8 by/ ] -IHW
- @(IHU … HTU) -IHU -HTU /2 width=2 by ldrop_skip, le_S_S/ (**) (* full auto too slow *)
-| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_flat2 … H) -H
- #V #T #HVW #HTU #H destruct /3 width=8 by lleq_flat/
-]
-qed-.
-
-axiom- lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[d, T] L2).
-(*
-#T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#n #IH #L1 * *
-[ #k #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, lleq_sort/
-| #i #H1 #L2 elim (eq_nat_dec (|L1|) (|L2|))
- [ #HL12 #d elim (lt_or_ge i d) /3 width=1 by lleq_skip, or_introl/
- #Hdi elim (lt_or_ge i (|L1|))
- #HiL1 elim (lt_or_ge i (|L2|)) /3 width=1 by or_introl, lleq_free/
- #HiL2 elim (ldrop_O1_lt … HiL2)
- #I2 #K2 #V2 #HLK2 elim (ldrop_O1_lt … HiL1)
- #I1 #K1 #V1 #HLK1 elim (eq_bind2_dec I2 I1)
- [ #H2 elim (eq_term_dec V2 V1)
- [ #H3 elim (IH K1 V1 … K2 0) destruct
- /3 width=7 by lleq_lref, ldrop_fwd_rfw, or_introl/
- ]
- ]
- -IH #H3 @or_intror
- #H elim (lleq_inv_lref … H) -H [1,3,4,6,7,9: * ]
- [1,3,5,7,8,9: /3 width=4 by lt_to_le_to_lt, lt_refl_false/ ]
- #I0 #X1 #X2 #V0 #HLX1 #HLX2 #HX12
- lapply (ldrop_mono … HLX1 … HLK1) -HLX1 -HLK1
- lapply (ldrop_mono … HLX2 … HLK2) -HLX2 -HLK2
- #H #H0 destruct /2 width=1 by/
- ]
-| #p #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, lleq_gref/
-| #a #I #V #T #Hn #L2 #d destruct
- elim (IH L1 V … L2 d) /2 width=1 by/
- elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V) (d+1)) -IH /3 width=1 by or_introl, lleq_bind/
- #H1 #H2 @or_intror
- #H elim (lleq_inv_bind … H) -H /2 width=1 by/
-| #I #V #T #Hn #L2 #d destruct
- elim (IH L1 V … L2 d) /2 width=1 by/
- elim (IH L1 T … L2 d) -IH /3 width=1 by or_introl, lleq_flat/
- #H1 #H2 @or_intror
- #H elim (lleq_inv_flat … H) -H /2 width=1 by/
-]
--n /4 width=3 by lleq_fwd_length, or_intror/
-qed-.
-*)
-(* Main properties **********************************************************)
-
-axiom- lleq_trans: ∀d,T. Transitive … (lleq d T).
-(*
-#d #T #L1 #L #H elim H -d -T -L1 -L
-/4 width=5 by lleq_fwd_length, lleq_gref, lleq_sort, trans_eq/
-[ #L1 #L #d #i #Hid #HL1 #L2 #H lapply (lleq_fwd_length … H)
- #HL2 elim (lleq_inv_lref … H) -H /2 width=1 by lleq_skip/
-| #I #L1 #L #K1 #K #V #d #i #Hdi #HLK1 #HLK #_ #IHK1 #L2 #H elim (lleq_inv_lref … H) -H
- [ -HLK1 -IHK1 * #HLi #_ elim (lt_refl_false i)
- /3 width=5 by ldrop_fwd_length_lt2, lt_to_le_to_lt/ (**) (* slow *)
- | -K1 -K #Hid elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
- | * #I0 #K0 #K2 #V0 #HLK0 #HLK2 #HK12 lapply (ldrop_mono … HLK0 … HLK) -L
- #H destruct /3 width=7 by lleq_lref/
- ]
-| #L1 #L #d #i #HL1i #HLi #HL #L2 #H lapply (lleq_fwd_length … H)
- #HL2 elim (lleq_inv_lref … H) -H /2 width=1 by lleq_free/
-| #a #I #L1 #L #V #T #d #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_bind … H) -H
- /3 width=1 by lleq_bind/
-| #I #L1 #L #V #T #d #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_flat … H) -H
- /3 width=1 by lleq_flat/
-]
-qed-.
-*)
-theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ⋕[d, T] L1→ L ⋕[d, T] L2 → L1 ⋕[d, T] L2.
-/3 width=3 by lleq_trans, lleq_sym/ qed-.
-
-theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ⋕[d, T] L → L2 ⋕[d, T] L → L1 ⋕[d, T] L2.
-/3 width=3 by lleq_trans, lleq_sym/ qed-.
]
qed.
+lemma lsuby_sym: ∀d,e,L1,L2. L1 ⊑×[d, e] L2 → |L1| = |L2| → L2 ⊑×[d, e] L1.
+#d #e #L1 #L2 #H elim H -d -e -L1 -L2
+[ #L1 #d #e #H >(length_inv_zero_dx … H) -L1 //
+| /2 width=1 by lsuby_length/
+| #I1 #I2 #L1 #L2 #V #e #_ #IHL12 #H lapply (injective_plus_l … H)
+ /3 width=1 by lsuby_pair/
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #H lapply (injective_plus_l … H)
+ /3 width=1 by lsuby_succ/
+]
+qed-.
+
(* Basic inversion lemmas ***************************************************)
fact lsuby_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → L1 = ⋆ → L2 = ⋆.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/relocation/fqu_lleq.ma".
-include "basic_2/substitution/fqup.ma".
-
-(* PLUS-ITERATED SUPCLOSURE *************************************************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃+ ⦃G2, K2, U⦄ →
- ∀L1. L1 ⋕[0, T] L2 →
- ∃∃K1. ⦃G1, L1, T⦄ ⊃+ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2.
-#G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
-[ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2
- /3 width=3 by fqu_fqup, ex2_intro/
-| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12 elim (IHTU … HL12) -L2
- #K1 #HTU #HK1 elim (lleq_fqu_trans … HU2 … HK1) -K
- /3 width=5 by fqup_strap1, ex2_intro/
-]
-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/substitution/fqup_lleq.ma".
-include "basic_2/substitution/fqus_alt.ma".
-
-(* STAR-ITERATED SUPCLOSURE *************************************************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃* ⦃G2, K2, U⦄ →
- ∀L1. L1 ⋕[0, T] L2 →
- ∃∃K1. ⦃G1, L1, T⦄ ⊃* ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2.
-#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H
-[ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/
-| * #HG #HL #HT destruct /2 width=3 by ex2_intro/
-]
-qed-.
#HU0 elim (cpys_up … HU0 … HTU) // -HU0 /4 width=5 by cpys_weak/
qed-.
+lemma lsuby_lleq_trans: ∀L2,L,T,d. L2 ⋕[T, d] L →
+ ∀L1. L1 ⊑×[d, ∞] L2 → |L1| = |L2| → L1 ⋕[T, d] L.
+#L2 #L #T #d * #HL2 #IH #L1 #HL12 #H @conj // -HL2
+#U elim (IH U) -IH #Hdx #Hsn @conj #HTU
+[ @Hdx -Hdx -Hsn @(lsuby_cpys_trans … HTU) -HTU
+ /2 width=1 by lsuby_sym/ (**) (* full auto does not work *)
+| -H -Hdx /3 width=3 by lsuby_cpys_trans/
+]
+qed-.
+
+lemma lleq_lsuby_trans: ∀L,L1,T,d. L ⋕[T, d] L1 →
+ ∀L2. L1 ⊑×[d, ∞] L2 → |L1| = |L2| → L ⋕[T, d] L2.
+/5 width=4 by lsuby_lleq_trans, lleq_sym, lsuby_sym/ qed-.
+
+lemma lleq_lsuby_repl: ∀L1,L2,T,d. L1 ⋕[T, d] L2 →
+ ∀K1. K1 ⊑×[d, ∞] L1 → |K1| = |L1| →
+ ∀K2. L2 ⊑×[d, ∞] K2 → |L2| = |K2| →
+ K1 ⋕[T, d] K2.
+/3 width=4 by lleq_lsuby_trans, lsuby_lleq_trans/ qed-.
+
(* Basic forward lemmas *****************************************************)
lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|.
/3 width=9 by lleqa_inv_lleq/
qed-.
-(* Advanced properties ******************************************************)
-
-lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2.
-#L1 #L2 #T #d1 #H @(lleq_ind_alt … H) -L1 -L2 -T -d1
-/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, yle_succ/
-[ /3 width=3 by lleq_skip, ylt_yle_trans/
-| #I1 #I2 #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (ylt_split i d2)
- [ lapply (lleq_fwd_length … HV) #HK12 #Hid2
- lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2)
- normalize in ⊢ (%→%→?); -I1 -I2 -V -d1 /2 width=1 by lleq_skip/
- | /3 width=8 by lleq_lref, yle_trans/
- ]
-]
-qed-.
-
-lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[V, 0] L2 → L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V →
- L1 ⋕[ⓑ{a,I}V.T, 0] L2.
-/3 width=3 by lleq_ge, lleq_bind/ qed.
-
(* Advanced inversion lemmas ************************************************)
fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[T, d0] L2 → ∀d. d0 = d + 1 →
#a #I #L1 #L2 #V #T #H elim (lleq_inv_bind … H) -H
/3 width=7 by ldrop_pair, conj, lleq_inv_S/
qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2.
+#L1 #L2 #T #d1 #H @(lleq_ind_alt … H) -L1 -L2 -T -d1
+/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, yle_succ/
+[ /3 width=3 by lleq_skip, ylt_yle_trans/
+| #I1 #I2 #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (ylt_split i d2)
+ [ lapply (lleq_fwd_length … HV) #HK12 #Hid2
+ lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2)
+ normalize in ⊢ (%→%→?); -I1 -I2 -V -d1 /2 width=1 by lleq_skip/
+ | /3 width=8 by lleq_lref, yle_trans/
+ ]
+]
+qed-.
+
+lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[V, 0] L2 → L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V →
+ L1 ⋕[ⓑ{a,I}V.T, 0] L2.
+/3 width=3 by lleq_ge, lleq_bind/ qed.
+
+lemma lleq_bind_repl_SO: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V →
+ ∀J,W. L1.ⓑ{J}W ⋕[T, 1] L2.ⓑ{J}W.
+#I #L1 #L2 #V #T #HT #J #W lapply (lleq_ge … HT 1 ?) // -HT
+#HT @(lleq_lsuby_repl … HT) /2 width=1 by lsuby_succ/ (**) (* full auto fails *)
+qed-.
+
+lemma lleq_bind_repl_O: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V →
+ ∀J,W. L1 ⋕[W, 0] L2 → L1.ⓑ{J}W ⋕[T, 0] L2.ⓑ{J}W.
+/3 width=7 by lleq_bind_repl_SO, lleq_inv_S/ 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/substitution/fqus_alt.ma".
+include "basic_2/substitution/lleq_alt.ma".
+
+(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
+
+(* Properties on supclosure and derivatives *********************************)
+
+lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ →
+ ∀L1. L1 ⋕[T, 0] L2 →
+ ∃∃K1. ⦃G1, L1, T⦄ ⊃ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+#G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
+[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H //
+ #I1 #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1
+ #H destruct /2 width=3 by fqu_lref_O, ex2_intro/
+| * [ #a ] #I #G #L2 #V #T #L1 #H
+ [ elim (lleq_inv_bind … H)
+ | elim (lleq_inv_flat … H)
+ ] -H
+ /2 width=3 by fqu_pair_sn, ex2_intro/
+| #a #I #G #L2 #V #T #L1 #H elim (lleq_inv_bind_O … H) -H
+ #H3 #H4 /2 width=3 by fqu_bind_dx, ex2_intro/
+| #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H
+ /2 width=3 by fqu_flat_dx, ex2_intro/
+| #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12
+ elim (ldrop_O1_le (e+1) L1)
+ [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
+ | lapply (ldrop_fwd_length_le2 … HLK2) -K2
+ lapply (lleq_fwd_length … HL12) -T -U //
+ ]
+]
+qed-.
+
+lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃⸮ ⦃G2, K2, U⦄ →
+ ∀L1. L1 ⋕[T, 0] L2 →
+ ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H
+[ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/
+| * #HG #HL #HT destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃+ ⦃G2, K2, U⦄ →
+ ∀L1. L1 ⋕[T, 0] L2 →
+ ∃∃K1. ⦃G1, L1, T⦄ ⊃+ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+#G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
+[ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2
+ /3 width=3 by fqu_fqup, ex2_intro/
+| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12 elim (IHTU … HL12) -L2
+ #K1 #HTU #HK1 elim (lleq_fqu_trans … HU2 … HK1) -K
+ /3 width=5 by fqup_strap1, ex2_intro/
+]
+qed-.
+
+lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃* ⦃G2, K2, U⦄ →
+ ∀L1. L1 ⋕[T, 0] L2 →
+ ∃∃K1. ⦃G1, L1, T⦄ ⊃* ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2.
+#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H
+[ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/
+| * #HG #HL #HT destruct /2 width=3 by ex2_intro/
+]
+qed-.
}
]
[ { "context-sensitive extended reduction" * } {
- [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_leq" + "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
- [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_cix" * ]
+ [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
+ [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_lleq" + "cpx_cix" * ]
}
]
[ { "context-sensitive extended irreducible forms" * } {
class "yellow"
[ { "substitution" * } {
[ { "lazy equivalence for local environments" * } {
- [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_lleq" * ]
+ [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ]
}
]
[ { "contxt-sensitive extended multiple substitution" * } {
}
]
[ { "iterated structural successor for closures" * } {
- [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_lleq" + "fqus_fqus" * ]
- [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_lleq" + "fqup_fqup" * ]
+ [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_fqus" * ]
+ [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
}
]
[ { "generic local env. slicing" * } {
}
]
[ { "structural successor for closures" * } {
- [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" "fquq_lleq" * ]
- [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_lleq" * ]
+ [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ]
+ [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" * ]
}
]
[ { "global env. slicing" * } {
}
]
[ { "basic local env. slicing" * } {
- [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_leq" + "ldrop_ldrop" * ]
+ [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
}
]
[ { "basic term relocation" * } {
]
class "red"
[ { "grammar" * } {
- [ { "equivalence for local environments" * } {
- [ "leq ( ? ≃[?,?] ? )" * ]
- }
- ]
[ { "pointwise extension of a relation" * } {
[ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ]
}
projects / helm.git / commitdiff