--- /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/llor.ma".
+include "basic_2/computation/cpxs_lleq.ma".
+include "basic_2/computation/lpxs_ldrop.ma".
+include "basic_2/computation/lpxs_cpxs.ma".
+include "basic_2/computation/lpxs_lpxs.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+axiom llor_fwd_sort: ∀L1,L2,L,d,k. L1 ⩖ [⋆k, d] L2 ≡ L → L = L2.
+
+axiom llor_fwd_lref: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L →
+ ∨∨ (|L| ≤ i ∧ L = L2)
+ | (yinj i < d ∧ L = L2)
+ | ∃∃I1,I2,K1,K2,K,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 &
+ ⇩[i] L2 ≡ K2.ⓑ{I2}V2 &
+ ⇩[i] L ≡ K.ⓑ{I2}V1 &
+ L2 ≃[yinj 0, yinj i] L &
+ K1 ⩖[V1, yinj 0] K2 ≡ K &
+ d ≤ yinj i.
+
+
+axiom llor_fwd_lref_lt: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → i < d → L = L2.
+
+axiom llor_inv_lref_be: ∀L1,L2,L,d,i. L1 ⩖ [#i, d] L2 ≡ L → d ≤ i →
+ ∀I1,I2,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ ∃∃K. ⇩[i] L ≡ K.ⓑ{I2}V1 & L2 ≃[0, i] L &
+ K1 ⩖[V1, 0] K2 ≡ K.
+
+axiom llor_fwd_gref: ∀L1,L2,L,d,p. L1 ⩖ [§p, d] L2 ≡ L → L = L2.
+
+axiom llor_inv_bind: ∀a,I,L1,L2,L,V,T,d. L1 ⩖ [ⓑ{a,I}V.T, d] L2 ≡ L →
+ ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1.ⓑ{I}V ⩖ [T, ⫯d] L0.ⓑ{I}V ≡ L.ⓑ{I}V.
+
+axiom llor_inv_flat: ∀I,L1,L2,L,V,T,d. L1 ⩖ [ⓕ{I}V.T, d] L2 ≡ L →
+ ∃∃L0. L1 ⩖ [V, d] L2 ≡ L0 & L1 ⩖ [T, d] L0 ≡ L.
+
+axiom llor_fwd_length_13: ∀L1,L2,L,T,d. L1 ⩖ [T, d] L2 ≡ L → |L1| = |L|.
+
+(* Properties obn lazy union for local environments *************************)
+
+lemma lpxs_llor_sn: ∀h,g,G,L1s,L0,L1d,T,d. L1s ⩖[T, d] L0 ≡ L1d →
+ ∀L2s,L2d. L2s ⩖[T, d] L0 ≡ L2d →
+ ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d.
+#h #g #G #L1s #L0 #L1d #T #d #H elim H -L1s -L0 -L1d -T -d
+[ #L1s #L0 #d #k #_ #L2s #L2d #H #_ >(llor_fwd_sort … H) //
+| #L1s #L0 #d #i #_ #Hid #L2s #L2d #H #_ >(llor_fwd_lref_lt … H) //
+| #I1s #I0 #L1s #L0 #L1d #K1s #K0 #K1d #V1s #V0 #d #i #Hdi #HLK1s #HLK0 #HLK1d #HL01d #HV1s #IHV1s #L2s #L2d #H #HL12s
+ elim (lpxs_ldrop_conf … HLK1s … HL12s) -L1s #Y #H #HLK2s
+ elim (lpxs_inv_pair1 … H) -H #K2s #V2s #HK12s #HV12s #H destruct
+ elim (llor_inv_lref_be … H … HLK2s HLK0) // -L2s -HLK0 -Hdi #K2d #HLK2d #HL02d #HV2s
+ lapply (leq_canc_sn … HL01d … HL02d) -L0 #HL12d
+ lapply (IHV1s … K2d … HK12s) -IHV1s -HK12s [2: #HK12d
+
+
+
+
+[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d
+ elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
+ elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
+ elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct
+ lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d
+ lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d
+ lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s
+ elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H
+ lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY
+ lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H
+ lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY
+ >(leq_inv_O_Y … HL2sY) -HL2sY //
+
+
+
+
+
+lemma lleq_lpxs_trans_llor: ∀h,g,G,L1s,L2s,L2d,T,d. L2d ⩖[T, d] L1s ≡ L2s →
+ ∀L1d. L1s ⋕[T, d] L1d → ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s.
+#h #g #G #L1s #L2s #L2d #T #d #H elim H -L1s -L2s -L2d -T -d //
+[ #I2d #I1s #L2d #L1s #L2s #K2d #K1s #K2s #V2d #V1s #d #i #Hdi #HLK2d #HLK1s #HLK2s #HL12s #_ #IHV2s #L1d #HL1sd #HL12d
+ elim (lpxs_ldrop_trans_O1 … HL12d … HLK2d) -L2d #Y #HLK1d #H
+ elim (lpxs_inv_pair2 … H) -H #K1d #V1d #HK12d #HV12d #H destruct
+ elim (lleq_inv_lref_ge … HL1sd … HLK1s HLK1d) // -d -I2d #H #HV1d destruct
+ lapply (lleq_cpxs_conf_dx … HV12d … HV1d) #HV2d
+ lapply (lleq_cpxs_trans … HV12d … HV1d) -HV12d -HV1d #HV12d
+ lapply (IHV2s … HV2d HK12d) -L1d -K1d -K2d #HK12s
+ elim (ldrop_lpxs_trans h g G … HLK1s (K2s.ⓑ{I1s}V2d)) /2 width=1 by lpxs_pair/ -V1d -K1s #Y #HL1sY #HYK2s #H
+ lapply (leq_canc_sn … HL12s … H) -HL12s -H #HL2sY
+ lapply (ldrop_O_inj … HLK2s HYK2s) -I1s -K2s -V2d #H
+ lapply (leq_join … HL2sY … H) -HL2sY -H #HL2sY
+ >(leq_inv_O_Y … HL2sY) -HL2sY //
+(*
+| #a #I #L2d #L1s #L0 #L2s #V #T #d #H0 #_ #IHV #IHT #L1d #H #HL12d
+ elim (lleq_inv_bind … H) -H #HV #HT
+*)
+| #I #L2d #L1s #LV #LT #L2s #V #T #d #H0 #_ #_ #IHV #IHT #IH #L1d #H #HL12d
+ elim (lleq_inv_flat … H) -H #HV #HT
+ lapply (IHV … HV HL12d) -HV #H1
+ lapply (IHT … HT HL12d) #H2
+
+
+
+ @(lpxs_trans … LV) /2 width=3 by/ -IHV
+ lapply (IHT … HL12d) // -IHT #H @(IH … H) -IH -H
+
+ @(IH … HL12d) -IHT -IHV
+
+ /4 width=5 by lpxs_trans/
+
+
+lemma lleq_lpx_conf_llor: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 →
+ ∀K2. K1 ⩖[T, d] L2 ≡ K2 → ⦃G, L2⦄ ⊢ ➡[h, g] K2.
+#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d
+[ #L1 #L2 #d #k #HL12 #K1 #HLK1 #K2 #H
projects / helm.git / blobdiff