L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V.
/2 width=2 by llpx_sn_fwd_bind_O_dx/ qed-.
-(* Properties on relocation *************************************************)
-
-lemma lleq_lift_le: ∀K1,K2,T,lt. K1 ≡[T, lt] K2 →
- ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 →
- ∀U. ⬆[l, k] T ≡ U → lt ≤ l → L1 ≡[U, lt] L2.
-/3 width=10 by llpx_sn_lift_le, lift_mono/ qed-.
-
-lemma lleq_lift_ge: ∀K1,K2,T,lt. K1 ≡[T, lt] K2 →
- ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 →
- ∀U. ⬆[l, k] T ≡ U → l ≤ lt → L1 ≡[U, lt+k] L2.
-/2 width=9 by llpx_sn_lift_ge/ qed-.
-
-(* Inversion lemmas on relocation *******************************************)
-
-lemma lleq_inv_lift_le: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 →
- ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 →
- ∀T. ⬆[l, k] T ≡ U → lt ≤ l → K1 ≡[T, lt] K2.
-/3 width=10 by llpx_sn_inv_lift_le, ex2_intro/ qed-.
-
-lemma lleq_inv_lift_be: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 →
- ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 →
- ∀T. ⬆[l, k] T ≡ U → l ≤ lt → lt ≤ l + k → K1 ≡[T, l] K2.
-/2 width=11 by llpx_sn_inv_lift_be/ qed-.
-
-lemma lleq_inv_lift_ge: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 →
- ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 →
- ∀T. ⬆[l, k] T ≡ U → l + k ≤ lt → K1 ≡[T, lt-k] K2.
-/2 width=9 by llpx_sn_inv_lift_ge/ qed-.
-
(* Inversion lemmas on negated lazy quivalence for local environments *******)
lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,l. (L1 ≡[ⓑ{a,I}V.T, l] 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/multiple/fqus_alt.ma".
-include "basic_2/multiple/lleq_drop.ma".
-
-(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
-
-(* Properties on supclosure *************************************************)
-
-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 //
- #K1 #H1 #H2 lapply (drop_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 #k #HLK2 #HTU #L1 #HL12
- elim (drop_O1_le (Ⓕ) (k+1) L1)
- [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
- | lapply (drop_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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/lfdeq_fqus.ma".
+include "basic_2/rt_transition/cpx_lfdeq.ma".
+include "basic_2/rt_transition/lfpx_lfdeq.ma".
+include "basic_2/rt_transition/fpb.ma".
+
+(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
+
+(* Properties with degree-based equivalence for local environments **********)
+
+(* Basic_2A1: was just: lleq_fpb_trans *)
+lemma lfdeq_fpb_trans: ∀h,o,F,K1,K2,T. K1 ≡[h, o, T] K2 →
+ ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, o] ⦃G, L2, U⦄ →
+ ∃∃L1,U0. ⦃F, K1, T⦄ ≻[h, o] ⦃G, L1, U0⦄ & U0 ≡[h, o] U & L1 ≡[h, o, U] L2.
+#h #o #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U
+[ #G #L2 #U #H2 elim (lfdeq_fqu_trans … H2 … HT) -K2
+ /3 width=5 by fpb_fqu, ex3_2_intro/
+| #U #HTU #HnTU elim (lfdeq_cpx_trans … HT … HTU) -HTU
+ /5 width=10 by fpb_cpx, cpx_lfdeq_conf_sn, tdeq_trans, tdeq_lfdeq_conf_sn, ex3_2_intro/
+| #L2 #HKL2 #HnKL2 elim (lfdeq_lfpx_trans … HKL2 … HT) -HKL2
+ /6 width=5 by fpb_lfpx, lfdeq_canc_sn, ex3_2_intro/ (* 2 lleq_canc_sn *)
+]
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/multiple/lleq_fqus.ma".
-include "basic_2/multiple/lleq_lleq.ma".
-include "basic_2/reduction/lpx_lleq.ma".
-include "basic_2/reduction/fpb.ma".
-
-(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_fpb_trans: ∀h,o,F,K1,K2,T. K1 ≡[T, 0] K2 →
- ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, o] ⦃G, L2, U⦄ →
- ∃∃L1. ⦃F, K1, T⦄ ≻[h, o] ⦃G, L1, U⦄ & L1 ≡[U, 0] L2.
-#h #o #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U
-[ #G #L2 #U #H2 elim (lleq_fqu_trans … H2 … HT) -K2
- /3 width=3 by fpb_fqu, ex2_intro/
-| /4 width=10 by fpb_cpx, cpx_lleq_conf_sn, lleq_cpx_trans, ex2_intro/
-| #L2 #HKL2 #HnKL2 elim (lleq_lpx_trans … HKL2 … HT) -HKL2
- /6 width=3 by fpb_lpx, lleq_canc_sn, ex2_intro/ (* 2 lleq_canc_sn *)
-]
-qed-.
(**************************************************************************)
include "basic_2/relocation/lifts_tdeq.ma".
+include "basic_2/static/lfxs_lfxs.ma".
include "basic_2/static/lfdeq_fqup.ma".
-include "basic_2/rt_transition/lfpx.ma".
+include "basic_2/rt_transition/lfpx_frees.ma".
+include "basic_2/rt_transition/lfpx.ma". (**) (* should be in lfpx_frees.ma *)
(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
/3 width=3 by lfdeq_sym, tdeq_sym, ex2_intro/
qed-.
-include "basic_2/static/lfxs_lfxs.ma".
+lemma lfpx_lfdeq_conf: ∀h,o,G,T. confluent2 … (lfpx h G T) (lfdeq h o T).
+/3 width=6 by lfpx_frees_conf, cpx_tdeq_conf_lexs, frees_lfdeq_conf_lexs, lfxs_conf/ qed-.
-axiom lfpx_lfdeq_conf: ∀h,o,G,T. confluent2 … (lfpx h G T) (lfdeq h o T).
-(*
-#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
-@lfxs_conf
-*)
(* Basic_2A1: was just: lleq_lpx_trans *)
lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 →
∀L1. L1 ≡[h, o, T] L2 →
∃∃K1. ⦃G, L1⦄ ⊢ ⬈[h, T] K1 & K1 ≡[h, o, T] K2.
#h #o #G #T #L2 #K2 #HLK2 #L1 #HL12
elim (lfpx_lfdeq_conf … o … HLK2 L1)
-/3 width=3 by lfdeq_sym, ex2_intro/
+/3 width=3 by lfdeq_sym, ex2_intro/
qed-.
(*
(* Properties with supclosure ***********************************************)
cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma
cpr.ma cpr_drops.ma
lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma
-fpb.ma
+fpb.ma fpb_lfdeq.ma
fpbq.ma fpbq_aaa.ma
]
qed-.
+lemma frees_tdeq_conf: ∀h,o,f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f →
+ ∀T2. T1 ≡[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≡ f.
+/3 width=7 by frees_tdeq_conf_lexs, lexs_refl/ qed-.
+
+lemma frees_lfdeq_conf_lexs: ∀h,o. lexs_frees_confluent (cdeq h o) cfull.
+/3 width=7 by frees_tdeq_conf_lexs, ex2_intro/ qed-.
+
+lemma tdeq_lfdeq_conf_sn: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o).
+#h #o #L1 #T1 #T2 #HT12 #L2 *
+/3 width=5 by frees_tdeq_conf, ex2_intro/
+qed-.
+
lemma lfdeq_sym: ∀h,o,T. symmetric … (lfdeq h o T).
#h #o #T #L1 #L2 *
/4 width=7 by frees_tdeq_conf_lexs, lfxs_sym, tdeq_sym, ex2_intro/
lemma lfdeq_fwd_pair_sn: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ②{I}V.T] L2 → L1 ≡[h, o, V] L2.
/2 width=3 by lfxs_fwd_pair_sn/ qed-.
+lemma lfdeq_fwd_dx: ∀h,o,I,L1,K2,V2. ∀T:term. L1 ≡[h, o, T] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. L1 = K1.ⓑ{I}V1.
+/2 width=5 by lfxs_fwd_dx/ qed-.
+
(* Basic_2A1: removed theorems 30:
lleq_ind lleq_inv_bind lleq_inv_flat lleq_fwd_length lleq_fwd_lref
lleq_fwd_drop_sn lleq_fwd_drop_dx
--- /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/lifts_tdeq.ma".
+include "basic_2/static/lfxs_drops.ma".
+include "basic_2/static/lfdeq_fqup.ma".
+
+(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******)
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_2A1: includes: lleq_lift_le lleq_lift_ge *)
+lemma lfdeq_lifts: ∀h,o. dedropable_sn (cdeq h o).
+/3 width=5 by lfxs_liftable_dedropable, tdeq_lifts/ qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_2A1: restricts: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
+lemma lfdeq_inv_lifts: ∀h,o. dropable_sn (cdeq h o).
+/2 width=5 by lfxs_dropable_sn/ qed-.
+
+(* Note: missing in basic_2A1 *)
+lemma lfdeq_inv_lifts_dx: ∀h,o. dropable_dx (cdeq h o).
+/2 width=5 by lfxs_dropable_dx/ qed-.
+
+(* Note: missing in basic_2A1 *)
+lemma lfdeq_inv_lifts_bi: ∀h,o,L1,L2,U. L1 ≡[h, o, U] L2 →
+ ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 →
+ ∀T. ⬆*[i] T ≡ U → K1 ≡[h, o, T] K2.
+/2 width=8 by lfxs_inv_lifts_bi/ qed-.
+
+lemma lfdeq_inv_lref_sn: ∀h,o,L1,L2,i. L1 ≡[h, o, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 →
+ ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ≡[h, o, V1] K2 & V1 ≡[h, o] V2.
+/2 width=3 by lfxs_inv_lref_sn/ qed-.
+
+lemma lfdeq_inv_lref_dx: ∀h,o,L1,L2,i. L1 ≡[h, o, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & K1 ≡[h, o, V1] K2 & V1 ≡[h, o] V2.
+/2 width=3 by lfxs_inv_lref_dx/ qed-.
lemma lfdeq_refl: ∀h,o,T. reflexive … (lfdeq h o T).
/2 width=1 by lfxs_refl/ qed.
+
+lemma lfdeq_pair: ∀h,o,V1,V2. V1 ≡[h, o] V2 →
+ ∀I,L. ∀T:term. L.ⓑ{I}V1 ≡[h, o, T] L.ⓑ{I}V2.
+/2 width=1 by lfxs_pair/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/s_computation/fqus_fqup.ma".
+include "basic_2/static/lfdeq_drops.ma".
+include "basic_2/static/lfdeq_lfdeq.ma".
+
+(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******)
+
+(* Properties with supclosure ***********************************************)
+
+lemma fqu_tdeq_conf: ∀h,o,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, T1⦄ →
+ ∀U2. U1 ≡[h, o] U2 →
+ ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐ ⦃G2, L, T2⦄ & L2 ≡[h, o, T1] L & T1 ≡[h, o] T2.
+#h #o #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1
+[ #I #G #L #W #X #H >(tdeq_inv_lref1 … H) -H
+ /2 width=5 by fqu_lref_O, ex3_2_intro/
+| #I #G #L #W1 #U1 #X #H
+ elim (tdeq_inv_pair1 … H) -H #W2 #U2 #HW12 #_ #H destruct
+ /2 width=5 by fqu_pair_sn, ex3_2_intro/
+| #p #I #G #L #W1 #U1 #X #H
+ elim (tdeq_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
+ /3 width=5 by lfdeq_pair, fqu_bind_dx, ex3_2_intro/
+| #I #G #L #W1 #U1 #X #H
+ elim (tdeq_inv_pair1 … H) -H #W2 #U2 #_ #HU12 #H destruct
+ /2 width=5 by fqu_flat_dx, ex3_2_intro/
+| #I #G #L #W #T1 #U1 #HTU1 #U2 #HU12
+ elim (tdeq_inv_lifts … HU12 … HTU1) -U1 #T2 #HTU2 #HT12
+ /3 width=5 by fqu_drop, ex3_2_intro/
+]
+qed-.
+
+lemma tdeq_fqu_trans: ∀h,o,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, T1⦄ →
+ ∀U2. U2 ≡[h, o] U1 →
+ ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐ ⦃G2, L, T2⦄ & T2 ≡[h, o] T1 & L ≡[h, o, T1] L2.
+#h #o #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21
+elim (fqu_tdeq_conf … o … H12 U2) -H12
+/3 width=5 by lfdeq_sym, tdeq_sym, ex3_2_intro/
+qed-.
+
+(* Basic_2A1: was just: lleq_fqu_trans *)
+lemma lfdeq_fqu_trans: ∀h,o,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ →
+ ∀L1. L1 ≡[h, o, T] L2 →
+ ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐ ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2.
+#h #o #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
+[ #I #G #L2 #V2 #L1 #H elim (lfdeq_inv_zero_pair_dx … H) -H
+ #K1 #V1 #HV1 #HV12 #H destruct
+ /3 width=7 by tdeq_lfdeq_conf_sn, fqu_lref_O, ex3_2_intro/
+| * [ #p ] #I #G #L2 #V #T #L1 #H
+ [ elim (lfdeq_inv_bind … H)
+ | elim (lfdeq_inv_flat … H)
+ ] -H
+ /2 width=5 by fqu_pair_sn, ex3_2_intro/
+| #a #I #G #L2 #V #T #L1 #H elim (lfdeq_inv_bind … H) -H
+ /2 width=5 by fqu_bind_dx, ex3_2_intro/
+| #I #G #L2 #V #T #L1 #H elim (lfdeq_inv_flat … H) -H
+ /2 width=5 by fqu_flat_dx, ex3_2_intro/
+| #I #G #L2 #V2 #T #U #HTU #Y #HU
+ elim (lfdeq_fwd_dx … HU) #L1 #V1 #H destruct
+ /5 width=12 by lfdeq_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/
+]
+qed-.
+
+(* Basic_2A1: was just: lleq_fquq_trans *)
+lemma lfdeq_fquq_trans: ∀h,o,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮ ⦃G2, K2, U⦄ →
+ ∀L1. L1 ≡[h, o, T] L2 →
+ ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐⸮ ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2.
+#h #o #G1 #G2 #L2 #K2 #T #U #H elim H -H
+[ #H #L1 #HL12 elim (lfdeq_fqu_trans … H … HL12) -L2 /3 width=5 by fqu_fquq, ex3_2_intro/
+| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+(* Basic_2A1: was just: lleq_fqup_trans *)
+lemma lfdeq_fqup_trans: ∀h,o,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+ ⦃G2, K2, U⦄ →
+ ∀L1. L1 ≡[h, o, T] L2 →
+ ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐+ ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2.
+#h #o #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
+[ #G2 #K2 #U #HTU #L1 #HL12 elim (lfdeq_fqu_trans … HTU … HL12) -L2
+ /3 width=5 by fqu_fqup, ex3_2_intro/
+| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12
+ elim (IHTU … HL12) -L2 #K0 #U0 #HTU #HU0 #HK0
+ elim (lfdeq_fqu_trans … HU2 … HK0) -K #K1 #U1 #HU1 #HU12 #HK12
+ elim (tdeq_fqu_trans … HU1 … HU0) -U #K3 #U3 #HU03 #HU31 #HK31
+ @(ex3_2_intro … K3 U3) (**) (* full auto too slow *)
+ /3 width=5 by lfdeq_trans, tdeq_lfdeq_conf_sn, fqup_strap1, tdeq_trans/
+]
+qed-.
+
+(* Basic_2A1: was just: lleq_fqus_trans *)
+lemma lfdeq_fqus_trans: ∀h,o,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐* ⦃G2, K2, U⦄ →
+ ∀L1. L1 ≡[h, o, T] L2 →
+ ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐* ⦃G2, K1, U0⦄ & U0 ≡[h, o] U & K1 ≡[h, o, U] K2.
+#h #o #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H
+[ #H elim (lfdeq_fqup_trans … H … HL12) -L2 /3 width=5 by fqup_fqus, ex3_2_intro/
+| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/
qed-.
+lemma lfxs_fwd_dx: ∀R,I,L1,K2,T,V2. L1 ⦻*[R, T] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. L1 = K1.ⓑ{I}V1.
+#R #I #L1 #K2 #T #V2 * #f elim (pn_split f) * #g #Hg #_ #Hf destruct
+[ elim (lexs_inv_push2 … Hf) | elim (lexs_inv_next2 … Hf) ] -Hf #K1 #V1 #_ #_ #H destruct
+/2 width=3 by ex1_2_intro/
+qed-.
+
(* Basic_2A1: removed theorems 24:
llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref
llpx_sn_bind llpx_sn_flat
qed-.
(* Basic_2A1: was: llpx_sn_inv_lift_O *)
-lemma lfxs_inv_lift_bi: ∀R,L1,L2,U. L1 ⦻*[R, U] L2 →
- ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 →
- ∀T. ⬆*[i] T ≡ U → K1 ⦻*[R, T] K2.
+lemma lfxs_inv_lifts_bi: ∀R,L1,L2,U. L1 ⦻*[R, U] L2 →
+ ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 →
+ ∀T. ⬆*[i] T ≡ U → K1 ⦻*[R, T] K2.
#R #L1 #L2 #U #HL12 #K1 #K2 #i #HLK1 #HLK2 #T #HTU
elim (lfxs_dropable_sn … HLK1 … HL12 … HTU) -L1 -U // #Y #HK12 #HY
lapply (drops_mono … HY … HLK2) -L2 -i #H destruct //
/3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/
qed.
-theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull →
- R_confluent2_lfxs R R R R →
- ∀T. confluent … (lfxs R T).
-#R #H1R #H2R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
+theorem lfxs_conf: ∀R1,R2.
+ lexs_frees_confluent R1 cfull →
+ lexs_frees_confluent R2 cfull →
+ R_confluent2_lfxs R1 R2 R1 R2 →
+ ∀T. confluent2 … (lfxs R1 T) (lfxs R2 T).
+#R1 #R2 #HR1 #HR2 #HR12 #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01
elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ]
[ #L #HL1 #HL2
- elim (H1R … Hf … HL01) -HL01 #f1 #Hf1 #H1
- elim (H1R … Hf … HL02) -HL02 #f2 #Hf2 #H2
+ elim (HR1 … Hf … HL01) -HL01 #f1 #Hf1 #H1
+ elim (HR2 … Hf … HL02) -HL02 #f2 #Hf2 #H2
lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1
lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2
/3 width=5 by ex2_intro/
elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0
lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01
lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02
- elim (H2R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/
+ elim (HR12 … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/
]
qed-.
}
]
*)
- [ { "uncounted context-sensitive rt-transition" * } {
+ [ { "uncounted context-sensitive rt-computation" * } {
(*
[ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
[ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ]
[ { "rt-transition" * } {
[ { "parallel rst-transition" * } {
[ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
- [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" (* "fpb_lleq" + "fpb_fleq" *) * ]
+ [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" (* + "fpb_fleq" *) * ]
}
]
[ { "t-bound context-sensitive rt-transition" * } {
]
[ { "degree-based equivalence on referred entries" * } {
[ "ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
- [ "lfdeq ( ? ≡[?,?,?] ? )" "lfdeq_length" + "lfdeq_fqup" + "lfdeq_lfdeq" * ]
+ [ "lfdeq ( ? ≡[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
}
]
[ { "generic extension on referred entries" * } {
projects / helm.git / commitdiff