+++ /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 f ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'LazyEq $f $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L1 ≡ [ break term 46 h , break term 46 o , break term 46 T ] break term 46 L2 )"
+notation "hvbox( L ⊢ break term 46 T1 ≡ [ break term 46 h , break term 46 o ] break term 46 T2 )"
non associative with precedence 45
- for @{ 'LazyEq $h $o $T $L1 $L2 }.
+ for @{ 'LazyEq $h $o $L $T1 $T2 }.
+++ /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( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≡ [ break term 46 h , break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'LazyEq $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
--- /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 f ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LazyEqSn $f $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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ≡ [ break term 46 h , break term 46 o , break term 46 T ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LazyEqSn $h $o $T $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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≡ [ break term 46 h , break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'LazyEqSn $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
#I #K #V1 #V2 #HLK lapply (drops_mono … Hi … HLK) -L #H destruct
qed.
+lemma cnx_lref_unit: ∀h,o,I,G,L,K,i. ⬇*[i] L ≡ K.ⓤ{I} → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃#i⦄.
+#h #o #I #G #L #K #i #HLK #X #H elim (cpx_inv_lref1_drops … H) -H // *
+#Z #Y #V1 #V2 #HLY lapply (drops_mono … HLK … HLY) -L #H destruct
+qed.
+
(* Basic_2A1: includes: cnx_lift *)
lemma cnx_lifts: ∀h,o,G. d_liftable1 … (cnx h o G).
#h #o #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H
/3 width=4 by cpg_delta, cpg_ell, ex_intro/
qed.
-lemma cpx_lref: ∀h,I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T →
- â¬\86*[1] T â\89¡ U â\86\92 â¦\83G, K.â\93\91{I}V⦄ ⊢ #⫯i ⬈[h] U.
-#h #I #G #K #V #T #U #i *
+lemma cpx_lref: ∀h,I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T →
+ â¬\86*[1] T â\89¡ U â\86\92 â¦\83G, K.â\93\98{I}⦄ ⊢ #⫯i ⬈[h] U.
+#h #I #G #K #T #U #i *
/3 width=4 by cpg_lref, ex_intro/
qed.
| ∃∃s. T2 = ⋆(next h s) & J = Sort s
| ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓑ{I}V1 & J = LRef 0
- | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2 &
- L = K.ⓑ{I}V & J = LRef (⫯i).
+ | ∃∃I,K,T,i. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2 &
+ L = K.ⓘ{I} & J = LRef (⫯i).
#h #J #G #L #T2 * #c #H elim (cpg_inv_atom1 … H) -H *
-/4 width=9 by or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex4_5_intro, ex4_4_intro, ex2_intro, ex_intro/
+/4 width=8 by or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex4_4_intro, ex2_intro, ex_intro/
qed-.
lemma cpx_inv_sort1: ∀h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ⬈[h] T2 →
lemma cpx_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈[h] T2 →
T2 = #(⫯i) ∨
- ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
+ ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2 & L = K.ⓘ{I}.
#h #G #L #T2 #i * #c #H elim (cpg_inv_lref1 … H) -H *
-/4 width=7 by ex3_4_intro, ex_intro, or_introl, or_intror/
+/4 width=6 by ex3_3_intro, ex_intro, or_introl, or_intror/
qed-.
lemma cpx_inv_gref1: ∀h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ⬈[h] T2 → T2 = §l.
/4 width=3 by ex2_intro, ex_intro, or_intror, or_introl/
qed-.
-lemma cpx_inv_lref1_pair: ∀h,I,G,K,V,T2,i. ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈[h] T2 →
+lemma cpx_inv_lref1_bind: ∀h,I,G,K,T2,i. ⦃G, K.ⓘ{I}⦄ ⊢ #⫯i ⬈[h] T2 →
T2 = #(⫯i) ∨
∃∃T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2.
-#h #I #G #L #V #T2 #i * #c #H elim (cpg_inv_lref1_pair … H) -H *
+#h #I #G #L #T2 #i * #c #H elim (cpg_inv_lref1_bind … H) -H *
/4 width=3 by ex2_intro, ex_intro, or_introl, or_intror/
qed-.
(∀G,L,s. R G L (⋆s) (⋆(next h s))) →
(∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → R G K V1 V2 →
⬆*[1] V2 ≡ W2 → R G (K.ⓑ{I}V1) (#0) W2
- ) → (∀I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → R G K (#i) T →
- â¬\86*[1] T â\89¡ U â\86\92 R G (K.â\93\91{I}V) (#⫯i) (U)
+ ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → R G K (#i) T →
+ â¬\86*[1] T â\89¡ U â\86\92 R G (K.â\93\98{I}) (#⫯i) (U)
) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →
R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
(* Properties with generic slicing for local environments *******************)
(* Basic_2A1: includes: cpx_lift *)
-lemma cpx_lifts_sn: ∀h,G. d_liftable2_sn (cpx h G).
+lemma cpx_lifts_sn: ∀h,G. d_liftable2_sn … lifts (cpx h G).
#h #G #K #T1 #T2 * #cT #HT12 #b #f #L #HLK #U1 #HTU1
elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
/3 width=4 by ex2_intro, ex_intro/
qed-.
-lemma cpx_lifts_bi: ∀h,G. d_liftable2_bi (cpx h G).
-/3 width=9 by cpx_lifts_sn, d_liftable2_sn_bi/ qed-.
+lemma cpx_lifts_bi: ∀h,G. d_liftable2_bi … lifts (cpx h G).
+#h #G #K #T1 #T2 * /3 width=10 by cpg_lifts_bi, ex_intro/
+qed-.
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: includes: cpx_inv_lift1 *)
-lemma cpx_inv_lifts_sn: ∀h,G. d_deliftable2_sn (cpx h G).
+lemma cpx_inv_lifts_sn: ∀h,G. d_deliftable2_sn … lifts (cpx h G).
#h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1
elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
/3 width=4 by ex2_intro, ex_intro/
qed-.
-lemma cpx_inv_lifts_bi: ∀h,G. d_deliftable2_bi (cpx h G).
-/3 width=9 by cpx_inv_lifts_sn, d_deliftable2_sn_bi/ qed-.
+lemma cpx_inv_lifts_bi: ∀h,G. d_deliftable2_bi …lifts (cpx h G).
+#h #G #L #U1 #U2 * /3 width=10 by cpg_inv_lifts_bi, ex_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/syntax/lenv_ext2.ma".
+include "basic_2/rt_transition/cpx.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR BINDERS ***********)
+
+definition cpx_ext (h) (G): relation3 lenv bind bind ≝
+ cext2 (cpx h G).
+
+interpretation
+ "uncounted context-sensitive parallel rt-transition (binder)"
+ 'PRedTy h G L I1 I2 = (cpx_ext h G L I1 I2).
include "basic_2/relocation/lifts_tdeq.ma".
include "basic_2/s_computation/fqus_fqup.ma".
include "basic_2/rt_transition/cpx_drops.ma".
+include "basic_2/rt_transition/cpx_lsubr.ma".
(* Properties on supclosure *************************************************)
-lemma fqu_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+lemma fqu_cpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
-#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄.
+#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=3 by cpx_pair_sn, cpx_bind, cpx_flat, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, ex2_intro/
[ #I #G #L2 #V2 #X2 #HVX2
elim (lifts_total X2 (𝐔❴1❵))
/3 width=3 by fqu_drop, cpx_delta, ex2_intro/
-| #I #G #L2 #V #T2 #X2 #HTX2 #U2 #HTU2
- elim (cpx_lifts_sn … HTU2 (Ⓣ) … (L2.ⓑ{I}V) … HTX2)
+| /5 width=4 by lsubr_cpx_trans, cpx_bind, lsubr_unit, fqu_clear, ex2_intro/
+| #I #G #L2 #T2 #X2 #HTX2 #U2 #HTU2
+ elim (cpx_lifts_sn … HTU2 (Ⓣ) … (L2.ⓘ{I}) … HTX2)
/3 width=3 by fqu_drop, drops_refl, drops_drop, ex2_intro/
]
qed-.
-lemma fquq_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+lemma fquq_cpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
-#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄.
+#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H
[ #HT12 #U2 #HTU2 elim (fqu_cpx_trans … HT12 … HTU2) /3 width=3 by fqu_fquq, ex2_intro/
| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
]
qed-.
-lemma fqup_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+lemma fqup_cpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
-#h #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄.
+#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
[ #G2 #L2 #T2 #H12 #U2 #HTU2 elim (fqu_cpx_trans … H12 … HTU2) -T2
/3 width=3 by fqu_fqup, ex2_intro/
| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
]
qed-.
-lemma fqus_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+lemma fqus_cpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
-#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_fqup … H) -H
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄.
+#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_fqup … H) -H
[ #HT12 #U2 #HTU2 elim (fqup_cpx_trans … HT12 … HTU2) /3 width=3 by fqup_fqus, ex2_intro/
| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
]
qed-.
-lemma fqu_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+lemma fqu_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄.
+#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❴1❵)
#U2 #HVU2 @(ex3_intro … U2)
[1,3: /3 width=7 by cpx_delta, fqu_drop/
[1,3: /2 width=4 by fqu_bind_dx, cpx_bind/
| #H elim (tdeq_inv_pair … H) -H /2 width=1 by/
]
+| #p #I #G #L #V #T1 #Hb #T2 #HT12 #H0 @(ex3_intro … (ⓑ{p,I}V.T2))
+ [1,3: /4 width=4 by lsubr_cpx_trans, cpx_bind, lsubr_unit, fqu_clear/
+ | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
| #I #G #L #V #T1 #T2 #HT12 #H0 @(ex3_intro … (ⓕ{I}V.T2))
[1,3: /2 width=4 by fqu_flat_dx, cpx_flat/
| #H elim (tdeq_inv_pair … H) -H /2 width=1 by/
]
-| #I #G #L #V #T1 #U1 #HTU1 #T2 #HT12 #H0
- elim (cpx_lifts_sn â\80¦ HT12 (â\93\89) â\80¦ (L.â\93\91{I}V) … HTU1) -HT12
+| #I #G #L #T1 #U1 #HTU1 #T2 #HT12 #H0
+ elim (cpx_lifts_sn â\80¦ HT12 (â\93\89) â\80¦ (L.â\93\98{I}) … HTU1) -HT12
/4 width=6 by fqu_drop, drops_refl, drops_drop, tdeq_inv_lifts_bi, ex3_intro/
]
qed-.
-lemma fquq_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+lemma fquq_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄.
+#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12
[ #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2
/3 width=4 by fqu_fquq, ex3_intro/
| * #HG #HL #HT destruct /3 width=4 by ex3_intro/
]
qed-.
-lemma fqup_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+lemma fqup_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄.
+#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2
/3 width=4 by fqu_fqup, ex3_intro/
| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2
]
qed-.
-lemma fqus_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+lemma fqus_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄.
+#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12
[ #H12 elim (fqup_cpx_trans_ntdeq … H12 … HTU2 H) -T2
/3 width=4 by fqup_fqus, ex3_intro/
| * #HG #HL #HT destruct /3 width=4 by ex3_intro/
include "basic_2/notation/relations/predtysn_5.ma".
include "basic_2/static/lfxs.ma".
-include "basic_2/rt_transition/cpx.ma".
+include "basic_2/rt_transition/cpx_ext.ma".
(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
lemma lfpx_atom: ∀h,I,G. ⦃G, ⋆⦄ ⊢ ⬈[h, ⓪{I}] ⋆.
/2 width=1 by lfxs_atom/ qed.
-lemma lfpx_sort: ∀h,I,G,L1,L2,V1,V2,s.
- â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, â\8b\86s] L2 â\86\92 â¦\83G, L1.â\93\91{I}V1â¦\84 â\8a¢ â¬\88[h, â\8b\86s] L2.â\93\91{I}V2.
+lemma lfpx_sort: ∀h,I1,I2,G,L1,L2,s.
+ â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, â\8b\86s] L2 â\86\92 â¦\83G, L1.â\93\98{I1}â¦\84 â\8a¢ â¬\88[h, â\8b\86s] L2.â\93\98{I2}.
/2 width=1 by lfxs_sort/ qed.
-lemma lfpx_zero: ∀h,I,G,L1,L2,V.
- ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, #0] L2.ⓑ{I}V.
-/2 width=1 by lfxs_zero/ qed.
+lemma lfpx_pair: ∀h,I,G,L1,L2,V1,V2.
+ ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 → ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, #0] L2.ⓑ{I}V2.
+/2 width=1 by lfxs_pair/ qed.
-lemma lfpx_lref: ∀h,I,G,L1,L2,V1,V2,i.
- â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, #i] L2 â\86\92 â¦\83G, L1.â\93\91{I}V1â¦\84 â\8a¢ â¬\88[h, #⫯i] L2.â\93\91{I}V2.
+lemma lfpx_lref: ∀h,I1,I2,G,L1,L2,i.
+ â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, #i] L2 â\86\92 â¦\83G, L1.â\93\98{I1}â¦\84 â\8a¢ â¬\88[h, #⫯i] L2.â\93\98{I2}.
/2 width=1 by lfxs_lref/ qed.
-lemma lfpx_gref: ∀h,I,G,L1,L2,V1,V2,l.
- â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, §l] L2 â\86\92 â¦\83G, L1.â\93\91{I}V1â¦\84 â\8a¢ â¬\88[h, §l] L2.â\93\91{I}V2.
+lemma lfpx_gref: ∀h,I1,I2,G,L1,L2,l.
+ â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, §l] L2 â\86\92 â¦\83G, L1.â\93\98{I1}â¦\84 â\8a¢ â¬\88[h, §l] L2.â\93\98{I2}.
/2 width=1 by lfxs_gref/ qed.
-lemma lfpx_pair_repl_dx: ∀h,I,G,L1,L2,T,V,V1.
- â¦\83G, L1.â\93\91{I}Vâ¦\84 â\8a¢ â¬\88[h, T] L2.â\93\91{I}V1 →
- ∀V2. ⦃G, L1⦄ ⊢ V ⬈[h] V2 →
- â¦\83G, L1.â\93\91{I}Vâ¦\84 â\8a¢ â¬\88[h, T] L2.â\93\91{I}V2.
-/2 width=2 by lfxs_pair_repl_dx/ qed-.
+lemma lfpx_bind_repl_dx: ∀h,I,I1,G,L1,L2,T.
+ â¦\83G, L1.â\93\98{I}â¦\84 â\8a¢ â¬\88[h, T] L2.â\93\98{I1} →
+ ∀I2. ⦃G, L1⦄ ⊢ I ⬈[h] I2 →
+ â¦\83G, L1.â\93\98{I}â¦\84 â\8a¢ â¬\88[h, T] L2.â\93\98{I2}.
+/2 width=2 by lfxs_bind_repl_dx/ qed-.
(* Basic inversion lemmas ***************************************************)
/2 width=3 by lfxs_inv_atom_dx/ qed-.
lemma lfpx_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
- ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+ ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
+ | ∃∃I1,I2,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 &
+ Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
/2 width=1 by lfxs_inv_sort/ qed-.
-
+(*
lemma lfpx_inv_zero: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ⬈[h, #0] Y2 →
(Y1 = ⋆ ∧ Y2 = ⋆) ∨
∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 &
⦃G, L1⦄ ⊢ V1 ⬈[h] V2 &
Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
/2 width=1 by lfxs_inv_zero/ qed-.
-
+*)
lemma lfpx_inv_lref: ∀h,G,Y1,Y2,i. ⦃G, Y1⦄ ⊢ ⬈[h, #⫯i] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
- ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+ ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
+ | ∃∃I1,I2,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 &
+ Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
/2 width=1 by lfxs_inv_lref/ qed-.
lemma lfpx_inv_gref: ∀h,G,Y1,Y2,l. ⦃G, Y1⦄ ⊢ ⬈[h, §l] Y2 →
- (Y1 = ⋆ ∧ Y2 = ⋆) ∨
- ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 &
- Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+ ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
+ | ∃∃I1,I2,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 &
+ Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
/2 width=1 by lfxs_inv_gref/ qed-.
lemma lfpx_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 →
(* Advanced inversion lemmas ************************************************)
-lemma lfpx_inv_sort_pair_sn: ∀h,I,G,Y2,L1,V1,s. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, ⋆s] Y2 →
- ∃∃L2,V2. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 & Y2 = L2.ⓑ{I}V2.
-/2 width=2 by lfxs_inv_sort_pair_sn/ qed-.
+lemma lfpx_inv_sort_bind_sn: ∀h,I1,G,Y2,L1,s. ⦃G, L1.ⓘ{I1}⦄ ⊢ ⬈[h, ⋆s] Y2 →
+ ∃∃I2,L2. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 & Y2 = L2.ⓘ{I2}.
+/2 width=2 by lfxs_inv_sort_bind_sn/ qed-.
-lemma lfpx_inv_sort_pair_dx: ∀h,I,G,Y1,L2,V2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] L2.ⓑ{I}V2 →
- ∃∃L1,V1. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 & Y1 = L1.ⓑ{I}V1.
-/2 width=2 by lfxs_inv_sort_pair_dx/ qed-.
+lemma lfpx_inv_sort_bind_dx: ∀h,I2,G,Y1,L2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] L2.ⓘ{I2} →
+ ∃∃I1,L1. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 & Y1 = L1.ⓘ{I1}.
+/2 width=2 by lfxs_inv_sort_bind_dx/ qed-.
lemma lfpx_inv_zero_pair_sn: ∀h,I,G,Y2,L1,V1. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, #0] Y2 →
∃∃L2,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 &
Y1 = L1.ⓑ{I}V1.
/2 width=1 by lfxs_inv_zero_pair_dx/ qed-.
-lemma lfpx_inv_lref_pair_sn: ∀h,I,G,Y2,L1,V1,i. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, #⫯i] Y2 →
- ∃∃L2,V2. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 & Y2 = L2.ⓑ{I}V2.
-/2 width=2 by lfxs_inv_lref_pair_sn/ qed-.
+lemma lfpx_inv_lref_bind_sn: ∀h,I1,G,Y2,L1,i. ⦃G, L1.ⓘ{I1}⦄ ⊢ ⬈[h, #⫯i] Y2 →
+ ∃∃I2,L2. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 & Y2 = L2.ⓘ{I2}.
+/2 width=2 by lfxs_inv_lref_bind_sn/ qed-.
-lemma lfpx_inv_lref_pair_dx: ∀h,I,G,Y1,L2,V2,i. ⦃G, Y1⦄ ⊢ ⬈[h, #⫯i] L2.ⓑ{I}V2 →
- ∃∃L1,V1. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 & Y1 = L1.ⓑ{I}V1.
-/2 width=2 by lfxs_inv_lref_pair_dx/ qed-.
+lemma lfpx_inv_lref_bind_dx: ∀h,I2,G,Y1,L2,i. ⦃G, Y1⦄ ⊢ ⬈[h, #⫯i] L2.ⓘ{I2} →
+ ∃∃I1,L1. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 & Y1 = L1.ⓘ{I1}.
+/2 width=2 by lfxs_inv_lref_bind_dx/ qed-.
-lemma lfpx_inv_gref_pair_sn: ∀h,I,G,Y2,L1,V1,l. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, §l] Y2 →
- ∃∃L2,V2. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 & Y2 = L2.ⓑ{I}V2.
-/2 width=2 by lfxs_inv_gref_pair_sn/ qed-.
+lemma lfpx_inv_gref_bind_sn: ∀h,I1,G,Y2,L1,l. ⦃G, L1.ⓘ{I1}⦄ ⊢ ⬈[h, §l] Y2 →
+ ∃∃I2,L2. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 & Y2 = L2.ⓘ{I2}.
+/2 width=2 by lfxs_inv_gref_bind_sn/ qed-.
-lemma lfpx_inv_gref_pair_dx: ∀h,I,G,Y1,L2,V2,l. ⦃G, Y1⦄ ⊢ ⬈[h, §l] L2.ⓑ{I}V2 →
- ∃∃L1,V1. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 & Y1 = L1.ⓑ{I}V1.
-/2 width=2 by lfxs_inv_gref_pair_dx/ qed-.
+lemma lfpx_inv_gref_bind_dx: ∀h,I2,G,Y1,L2,l. ⦃G, Y1⦄ ⊢ ⬈[h, §l] L2.ⓘ{I2} →
+ ∃∃I1,L1. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 & Y1 = L1.ⓘ{I1}.
+/2 width=2 by lfxs_inv_gref_bind_dx/ qed-.
(* Basic forward lemmas *****************************************************)
[ #H destruct /3 width=1 by aaa_zero/
| -HV12 * /4 width=7 by aaa_lifts, drops_refl, drops_drop/
]
-| #I #G #L1 #V1 #B #i #_ #IH #X2 #HX #Y #HY
- elim (lfpx_inv_lref_pair_sn … HY) -HY #L2 #W2 #HL12 #H destruct
- elim (cpx_inv_lref1_pair … HX) -HX
+| #I #G #L1 #B #i #_ #IH #X2 #HX #Y #HY
+ elim (lfpx_inv_lref_bind_sn … HY) -HY #I2 #L2 #HL12 #H destruct
+ elim (cpx_inv_lref1_bind … HX) -HX
[ #H destruct /3 width=1 by aaa_lref/
| * /4 width=7 by aaa_lifts, drops_refl, drops_drop/
]
elim (lfpx_inv_bind … HL12) -HL12 #HV #HT
elim (cpx_inv_abbr1 … HX) -HX *
[ #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=2 by lfpx_pair_repl_dx, aaa_abbr/
+ /5 width=2 by lfpx_bind_repl_dx, aaa_abbr, ext2_pair/
| #T2 #HT12 #HXT2 #H destruct -IHV
/4 width=7 by aaa_inv_lifts, drops_drop, drops_refl/
]
| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12
elim (lfpx_inv_bind … HL12) -HL12 #HV #HT
elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=2 by lfpx_pair_repl_dx, aaa_abst/
+ /5 width=2 by lfpx_bind_repl_dx, aaa_abst, ext2_pair/
| #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12
elim (lfpx_inv_flat … HL12) -HL12 #HV #HT
elim (cpx_inv_appl1 … H) -H *
lemma lfpx_drops_trans: ∀h,G. dropable_dx (cpx h G).
/2 width=5 by lfxs_dropable_dx/ qed-.
-lemma lfpx_inv_lref_sn: ∀h,G,L1,L2,i. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 →
- ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & ⦃G, K1⦄ ⊢ ⬈[h, V1] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2.
-/2 width=3 by lfxs_inv_lref_sn/ qed-.
+lemma lfpx_inv_lref_pair_sn: ∀h,G,L1,L2,i. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 →
+ ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & ⦃G, K1⦄ ⊢ ⬈[h, V1] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2.
+/2 width=3 by lfxs_inv_lref_pair_sn/ qed-.
-lemma lfpx_inv_lref_dx: ∀h,G,L1,L2,i. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & ⦃G, K1⦄ ⊢ ⬈[h, V1] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2.
-/2 width=3 by lfxs_inv_lref_dx/ qed-.
+lemma lfpx_inv_lref_pair_dx: ∀h,G,L1,L2,i. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & ⦃G, K1⦄ ⊢ ⬈[h, V1] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2.
+/2 width=3 by lfxs_inv_lref_pair_dx/ qed-.
lemma lfpx_pair: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L.ⓑ{I}V2.
/2 width=1 by lfxs_pair/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lfpx_inv_bind_void: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 →
+ ⦃G, L1⦄ ⊢ ⬈[h, V] L2 ∧ ⦃G, L1.ⓧ⦄ ⊢ ⬈[h, T] L2.ⓧ.
+/2 width=3 by lfxs_inv_bind_void/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lfpx_fwd_bind_dx_void: ∀h,p,I,G,L1,L2,V,T.
+ ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 → ⦃G, L1.ⓧ⦄ ⊢ ⬈[h, T] L2.ⓧ.
+/2 width=4 by lfxs_fwd_bind_dx_void/ qed-.
include "basic_2/static/lsubf_frees.ma".
include "basic_2/static/lfxs.ma".
include "basic_2/rt_transition/cpx_drops.ma".
+include "basic_2/rt_transition/cpx_ext.ma".
(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
(* Properties with context-sensitive free variables *************************)
(* Basic_2A1: uses: lpx_cpx_frees_trans *)
+(* check sle_refl *)
lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
- ∀L2. L1 ⪤*[cpx h G, cfull, f1] L2 →
+ ∀L2. L1 ⪤*[cpx_ext h G, cfull, f1] L2 →
∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1.
-#h #G #L1 #T1 @(fqup_wf_ind_eq … G L1 T1) -G -L1 -T1
+#h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1
#G0 #L0 #U0 #IH #G #L1 * *
[ -IH #s #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct
lapply (frees_inv_sort … H1) -H1 #Hg1
elim (cpx_inv_sort1 … H0) -H0 #H destruct
- /3 width=3 by frees_sort_gen, sle_refl, ex2_intro/
+ /3 width=3 by frees_sort, sle_refl, ex2_intro/
| #i #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct
elim (frees_inv_lref_drops … H1) -H1 *
- [ -IH #HL1 #Hg1
+ [ -IH #f1 #HL1 #Hf1 #H destruct
elim (cpx_inv_lref1_drops … H0) -H0
[ #H destruct
- /5 width=9 by frees_lref_atom, drops_atom2_lexs_conf, coafter_isuni_isid, sle_refl, ex2_intro/
- | * -H2 -Hg1 #I #K1 #V1 #V2 #HLK1
+ /4 width=9 by frees_atom_drops, drops_atom2_lexs_conf, sle_refl, ex2_intro/
+ | * -H2 -Hf1 #I #K1 #V1 #V2 #HLK1
lapply (drops_TF … HLK1) -HLK1 #HLK1
lapply (drops_mono … HLK1 … HL1) -L1 #H destruct
]
| #f1 #I #K1 #V1 #Hf1 #HLK1 #H destruct
elim (cpx_inv_lref1_drops … H0) -H0
[ #H destruct
- elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #K2 #V2 #HLK2 #HK12 #HV12
+ elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #Z #K2 #HLK2 #HK12 #H
+ elim (ext2_inv_pair_sn … H) -H #V2 #HV12 #H destruct
elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -L1 -K1 -V1 #f2 #Hf2 #Hf21
- /4 width=7 by frees_lref_pushs, frees_lref_pair, drops_refl, sle_next, ex2_intro, sle_pushs/
- | * #J #Y #X #V2 #H #HV12 #HVU2
+ /4 width=7 by frees_lref_pushs, frees_pair_drops, drops_refl, sle_pushs, sle_next, ex2_intro/
+ | * #Z #Y #X #V2 #H #HV12 #HVU2
lapply (drops_mono … H … HLK1) -H #H destruct
- elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #K2 #V0 #HLK2 #HK12 #_
+ elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #I2 #K2 #HLK2 #HK12 #H
+ elim (ext2_inv_pair_sn … H) -H #V0 #_ #H destruct
lapply (drops_isuni_fwd_drop2 … HLK2) // -V0 #HLK2
elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -I -L1 -K1 -V1 #f2 #Hf2 #Hf21
lapply (frees_lifts … Hf2 … HLK2 … HVU2 ??) /4 width=7 by sle_weak, ex2_intro, sle_pushs/
]
+ | #f1 #I #K1 #HLK1 #Hf1 #H destruct
+ elim (cpx_inv_lref1_drops … H0) -H0
+ [ -IH #H destruct
+ elim (lexs_drops_conf_next … H2 … HLK1) -H2 -HLK1 [ |*: // ] #Z #K2 #HLK2 #_ #H
+ lapply (ext2_inv_unit_sn … H) -H #H destruct
+ /3 width=3 by frees_unit_drops, sle_refl, ex2_intro/
+ | * -H2 -Hf1 #Z #Y1 #X1 #X2 #HLY1
+ lapply (drops_mono … HLK1 … HLY1) -L1 #H destruct
+ ]
]
| -IH #l #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct
lapply (frees_inv_gref … H1) -H1 #Hg1
lapply (cpx_inv_gref1 … H0) -H0 #H destruct
- /3 width=3 by frees_gref_gen, sle_refl, ex2_intro/
+ /3 width=3 by frees_gref, sle_refl, ex2_intro/
| #p #I #V1 #T1 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct
elim (frees_inv_bind … H1) -H1 #gV1 #gT1 #HgV1 #HgT1 #Hg1
elim (cpx_inv_bind1 … H0) -H0 *
[ #V2 #T2 #HV12 #HT12 #H destruct
lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
- lapply (lexs_inv_tl … I … HL12T … HV12 ?) // -HL12T #HL12T
+ lapply (lexs_inv_tl … (BPair I V1) (BPair I V2) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T
elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/
/4 width=10 by frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/
| #T2 #HT12 #HUT2 #H0 #H1 destruct -HgV1
lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
- lapply (lexs_inv_tl … Abbr … V1 V1 HL12T ??) // -HL12T #HL12T
+ lapply (lexs_inv_tl … (BPair Abbr V1) (BPair Abbr V1) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T
elim (IH … HgT1 … HL12T … HT12) // -L1 -T1 #gT2 #HgT2 #HgT21
lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] -V1 -T2
/5 width=6 by sor_inv_sle_dx, sle_trans, sle_tl, ex2_intro/
lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2
lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W
lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
- lapply (lexs_inv_tl … Abst … HL12T … HW12 ?) // -HL12T #HL12T
+ lapply (lexs_inv_tl … (BPair Abst W1) (BPair Abst W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T
elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_
- lapply (sor_trans2 … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1
- lapply (sor_sym … Hg0) -Hg0 #Hg0
+ lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1
+ lapply (sor_comm … Hg0) -Hg0 #Hg0
elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21
elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
- elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_
- elim (lsubf_frees_trans … HgT2 (⫯gVT2) … (L2.ⓓⓝW2.V2))
- [2: /4 width=4 by lsubf_refl, lsubf_beta, sor_inv_sle_dx, sor_inv_sle_sn, sle_inv_tl_sn/ ]
- -HgT2 #gT0 #HgT0 #HgT20
+ elim (sor_isfin_ex (⫱gT2) gV2) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_
+ elim (lsubf_beta_tl_dx … HgV2 … HgVT2 … W2) [ |*: /1 width=3 by lsubf_refl/ ] #gT0 #HL2 #HgT02
+ lapply (lsubf_frees_trans … HgT2 … HL2) -HgT2 -HL2 #HgT0
+ lapply (sor_comm … HgVT2) -HgVT2 #HgVT2 (**) (* this should be removed *)
elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H
elim (sor_isfin_ex gV0 (⫱gT0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
- @(ex2_intro … g2)
- [ @(frees_bind … Hg2) /2 width=5 by frees_flat/
- | -L2 @(sor_inv_sle … Hg2) -Hg2
- [ /3 width=11 by sor_inv_sle_sn_trans, monotonic_sle_sor/
- | @sle_xn_tl [2:|*: // ] @(sle_trans … HgT20) -HgT20
- /4 width=8 by monotonic_sle_sor, sor_inv_sle_dx_trans, sle_tl, sle_next/
- ] (**) (* full auto too slow *)
- ]
+ @(ex2_intro … g2) /3 width=5 by frees_flat, frees_bind/ -h -p -G -L1 -L2 -V1 -V2 -W1 -W2 -T1 -T2
+ @(sor_inv_sle … Hg2) -Hg2
+ [ /3 width=11 by sor_inv_sle_sn_trans, monotonic_sle_sor/
+ | @(sle_trans … HgT02) -HgT02
+ /3 width=8 by monotonic_sle_sor, sor_inv_sle_dx_trans, sle_tl/
+ ] (**) (* full auto too slow *)
| #p #V2 #V #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #H0 #H1 #H destruct
elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0
lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2
lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W
lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
- lapply (lexs_inv_tl … Abbr … HL12T … HW12 ?) // -HL12T #HL12T
+ lapply (lexs_inv_tl … (BPair Abbr W1) (BPair Abbr W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T
elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_
- lapply (sor_trans2 … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1
+ lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1
elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21
elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
elim (sor_isfin_ex (↑gV2) gT2) /3 width=3 by frees_fwd_isfin, isfin_push/ #gV0 #HgV0 #H
elim (sor_isfin_ex gW2 (⫱gV0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
- lapply (sor_trans2 … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2
+ lapply (sor_assoc_sn … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2
lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??)
- [4: lapply (sor_sym … Hg) |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 (**) (* full auto too slow *)
+ [4: lapply (sor_comm … Hg) |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 (**) (* full auto too slow *)
/4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/
]
]
(* Basic_2A1: uses: cpx_frees_trans *)
lemma cpx_frees_conf: ∀h,G. R_frees_confluent (cpx h G).
-/3 width=7 by cpx_frees_conf_lfpx, lexs_refl/ qed-.
+/4 width=7 by cpx_frees_conf_lfpx, lexs_refl, ext2_refl/ qed-.
(* Basic_2A1: uses: lpx_frees_trans *)
-lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx h G) cfull.
+lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx_ext h G) cfull.
/2 width=7 by cpx_frees_conf_lfpx/ qed-.
elim (lfdeq_inv_zero_pair_sn … H2) -H2 #K2 #X2 #HK02 #HX2 #H destruct
elim (IH X2 … HK01 … HK02) // -K0 -V0 #V #HV1 #HV2
elim (tdeq_lifts_sn … HV1 … HVW1) -V1 /3 width=5 by cpx_delta, ex2_intro/
-| #I #G #K0 #V0 #V1 #W1 #i #_ #IH #HVW1 #T2 #H0 #L1 #H1 #L2 #H2
+| #I0 #G #K0 #V1 #W1 #i #_ #IH #HVW1 #T2 #H0 #L1 #H1 #L2 #H2
>(tdeq_inv_lref1 … H0) -H0
- elim (lfpx_inv_lref_pair_sn … H1) -H1 #K1 #X1 #HK01 #H destruct
- elim (lfdeq_inv_lref_pair_sn … H2) -H2 #K2 #X2 #HK02 #H destruct
- elim (IH … HK01 … HK02) [|*: //] -K0 -V0 #V #HV1 #HV2
+ elim (lfpx_inv_lref_bind_sn … H1) -H1 #I1 #K1 #HK01 #H destruct
+ elim (lfdeq_inv_lref_bind_sn … H2) -H2 #I2 #K2 #HK02 #H destruct
+ elim (IH … HK01 … HK02) [|*: //] -K0 #V #HV1 #HV2
elim (tdeq_lifts_sn … HV1 … HVW1) -V1 /3 width=5 by cpx_lref, ex2_intro/
| #p #I #G #L0 #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X0 #H0 #L1 #H1 #L2 #H2
elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct
elim (lfpx_inv_bind … H1) -H1 #HL01 #H1
elim (lfdeq_inv_bind … H2) -H2 #HL02 #H2
- lapply (lfdeq_pair_repl_dx … H2 … HV02) -H2 #H2
+ lapply (lfdeq_bind_repl_dx … H2 (BPair I V2) ?) -H2 /2 width=1 by ext2_pair/ #H2
elim (IHV … HV02 … HL01 … HL02) -IHV -HV02 -HL01 -HL02
elim (IHT … HT02 … H1 … H2) -L0 -T0
/3 width=5 by cpx_bind, tdeq_pair, ex2_intro/
elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct
elim (lfpx_inv_bind … H1) -H1 #HL01 #H1
elim (lfdeq_inv_bind … H2) -H2 #HL02 #H2
- lapply (lfdeq_pair_repl_dx … H2 … HV02) -H2 -HV02 #H2
+ lapply (lfdeq_bind_repl_dx … H2 (BPair Abbr V2) ?) -H2 /2 width=1 by ext2_pair/ -HV02 #H2
elim (IH … HT02 … H1 … H2) -L0 -T0 #T #HT1
elim (tdeq_inv_lifts_sn … HT1 … HUT1) -T1
/3 width=5 by cpx_zeta, ex2_intro/
elim (lfpx_inv_bind … H1) -H1 #H1LW0 #H1LT0
elim (lfdeq_inv_flat … H2) -H2 #H2LV0 #H2
elim (lfdeq_inv_bind … H2) -H2 #H2LW0 #H2LT0
- lapply (lfdeq_pair_repl_dx … H2LT0 … HW02) -H2LT0 #H2LT0
+ lapply (lfdeq_bind_repl_dx … H2LT0 (BPair Abst W2) ?) -H2LT0 /2 width=1 by ext2_pair/ #H2LT0
elim (IHV … HV02 … H1LV0 … H2LV0) -IHV -HV02 -H1LV0 -H2LV0
elim (IHW … HW02 … H1LW0 … H2LW0) -IHW -HW02 -H1LW0 -H2LW0
elim (IHT … HT02 … H1LT0 … H2LT0) -L0 -V0 -T0
elim (lfpx_inv_bind … H1) -H1 #H1LW0 #H1LT0
elim (lfdeq_inv_flat … H2) -H2 #H2LV0 #H2
elim (lfdeq_inv_bind … H2) -H2 #H2LW0 #H2LT0
- lapply (lfdeq_pair_repl_dx … H2LT0 … HW02) -H2LT0 #H2LT0
+ lapply (lfdeq_bind_repl_dx … H2LT0 (BPair Abbr W2) ?) -H2LT0 /2 width=1 by ext2_pair/ #H2LT0
elim (IHV … HV02 … H1LV0 … H2LV0) -IHV -HV02 -H1LV0 -H2LV0 #V #HV1
elim (IHW … HW02 … H1LW0 … H2LW0) -IHW -HW02 -H1LW0 -H2LW0
elim (IHT … HT02 … H1LT0 … H2LT0) -L0 -V0 -T0
]
qed-.
-lemma cpx_tdeq_conf: ∀h,o,G,L,T0,T1. ⦃G, L⦄ ⊢ T0 ⬈[h] T1 →
+lemma cpx_tdeq_conf: ∀h,o,G,L. ∀T0:term. ∀T1. ⦃G, L⦄ ⊢ T0 ⬈[h] T1 →
∀T2. T0 ≡[h, o] T2 →
∃∃T. T1 ≡[h, o] T & ⦃G, L⦄ ⊢ T2 ⬈[h] T.
#h #o #G #L #T0 #T1 #HT01 #T2 #HT02
/2 width=3 by lfxs_refl, ex2_intro/
qed-.
-lemma tdeq_cpx_trans: ∀h,o,G,L,T2,T0. T2 ≡[h, o] T0 →
+lemma tdeq_cpx_trans: ∀h,o,G,L,T2. ∀T0:term. T2 ≡[h, o] T0 →
∀T1. ⦃G, L⦄ ⊢ T0 ⬈[h] T1 →
∃∃T. ⦃G, L⦄ ⊢ T2 ⬈[h] T & T ≡[h, o] T1.
#h #o #G #L #T2 #T0 #HT20 #T1 #HT01
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazyeq_8.ma".
+include "basic_2/notation/relations/lazyeqsn_8.ma".
include "basic_2/syntax/genv.ma".
include "basic_2/static/lfdeq.ma".
interpretation
"degree-based equivalence on referred entries (closure)"
- 'LazyEq h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2).
+ 'LazyEqSn h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2).
(* Basic properties *********************************************************)
∨∨ ∃∃g. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ & 𝐈⦃g⦄ & f = ↑*[i] ⫯g
| ∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≡ g &
⬇*[i] L ≡ K.ⓑ{I}V & f = ↑*[i] ⫯g
- | ∃∃g,I,K. ⬇*[i] L ≡ K.ⓤ{I} & f = ↑*[i] ⫯g.
+ | ∃∃g,I,K. ⬇*[i] L ≡ K.ⓤ{I} & 𝐈⦃g⦄ & f = ↑*[i] ⫯g.
#L elim L -L
[ #i #g | #L #I #IH * [ #g cases I -I [ #I | #I #V ] -IH | #i #g ] ] #H
[ elim (frees_inv_atom … H) -H #f #Hf #H destruct
/3 width=3 by or3_intro0, ex3_intro/
| elim (frees_inv_unit … H) -H #f #Hf #H destruct
- /4 width=3 by drops_refl, or3_intro2, ex2_3_intro/
+ /4 width=3 by drops_refl, or3_intro2, ex3_3_intro/
| elim (frees_inv_pair … H) -H #f #Hf #H destruct
/4 width=7 by drops_refl, or3_intro1, ex3_4_intro/
| elim (frees_inv_lref … H) -H #f #Hf #H destruct
elim (IH … Hf) -IH -Hf *
[ /4 width=3 by drops_drop, or3_intro0, ex3_intro/
| /4 width=7 by drops_drop, or3_intro1, ex3_4_intro/
- | /4 width=3 by drops_drop, or3_intro2, ex2_3_intro/
+ | /4 width=3 by drops_drop, or3_intro2, ex3_3_intro/
]
]
qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazyeq_5.ma".
+include "basic_2/notation/relations/lazyeqsn_5.ma".
include "basic_2/syntax/tdeq_ext.ma".
include "basic_2/static/lfxs.ma".
interpretation
"degree-based equivalence on referred entries (local environment)"
- 'LazyEq h o T L1 L2 = (lfdeq h o T L1 L2).
+ 'LazyEqSn h o T L1 L2 = (lfdeq h o T L1 L2).
interpretation
"degree-based ranged equivalence (local environment)"
- 'LazyEq h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2).
+ 'LazyEqSn h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2).
(*
definition lfdeq_transitive: predicate (relation3 lenv term term) ≝
λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[h, o, T1] L2 → R L1 T1 T2.
lemma lsubf_refl_eq: ∀f1,f2,L. f1 ≗ f2 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄.
/2 width=3 by lsubf_eq_repl_back2/ qed.
-lemma lsubf_tl_dx: ∀g1,f2,I,L1,L2. ⦃L1, g1⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ →
- ∃∃f1. ⦃L1.ⓘ{I}, f1⦄ ⫃𝐅* ⦃L2.ⓘ{I}, f2⦄ & g1 = ⫱f1.
+lemma lsubf_bind_tl_dx: ∀g1,f2,I,L1,L2. ⦃L1, g1⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ →
+ ∃∃f1. ⦃L1.ⓘ{I}, f1⦄ ⫃𝐅* ⦃L2.ⓘ{I}, f2⦄ & g1 = ⫱f1.
#g1 #f2 #I #L1 #L2 #H
elim (pn_split f2) * #g2 #H2 destruct
@ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *)
qed-.
+lemma lsubf_beta_tl_dx: ∀f,f0,g1,L1,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f0 ⋓ f ≡ g1 →
+ ∀f2,L2,W. ⦃L1, f0⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ →
+ ∃∃f1. ⦃L1.ⓓⓝW.V, f1⦄ ⫃𝐅* ⦃L2.ⓛW, f2⦄ & ⫱f1 ⊆ g1.
+#f #f0 #g1 #L1 #V #Hf #Hg1 #f2
+elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct
+[ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/
+| @(ex2_intro … (⫯g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *)
+]
+qed-.
+
+(* Note: this might be moved *)
lemma lsubf_inv_sor_dx: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
∀f2l,f2r. f2l⋓f2r ≡ f2 →
∃∃f1l,f1r. ⦃L1, f1l⦄ ⫃𝐅* ⦃L2, f2l⦄ & ⦃L1, f1r⦄ ⫃𝐅* ⦃L2, f2r⦄ & f1l⋓f1r ≡ f1.
| /3 width=5 by lsubf_fwd_isid_dx, frees_gref/
| #f2V #f2T #f2 #p #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f1 #L1 #H12
elim (lsubf_inv_sor_dx … H12 … Hf2) -f2 #f1V #g1T #HV #HT #Hf1
- elim (lsubf_tl_dx … (BPair I V) … HT) -HT #f1T #HT #H destruct
+ elim (lsubf_bind_tl_dx … (BPair I V) … HT) -HT #f1T #HT #H destruct
/3 width=5 by frees_bind/
| #f2V #f2T #f2 #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f1 #L1 #H12
elim (lsubf_inv_sor_dx … H12 … Hf2) -f2 /3 width=5 by frees_flat/
.
interpretation
- "degree-based equivalence (terms)"
+ "context-free degree-based equivalence (term)"
'LazyEq h o T1 T2 = (tdeq h o T1 T2).
(* Basic inversion lemmas ***************************************************)
(* *)
(**************************************************************************)
+include "basic_2/notation/relations/lazyeq_5.ma".
include "basic_2/syntax/tdeq.ma".
include "basic_2/syntax/lenv_ext2.ma".
(* EXTENDED DEGREE-BASED EQUIVALENCE ****************************************)
-definition cdeq: ∀h. sd h → relation3 lenv term term ≝
- λh,o,L. tdeq h o.
-
definition tdeq_ext: ∀h. sd h → relation bind ≝
λh,o. ext2 (tdeq h o).
+definition cdeq: ∀h. sd h → relation3 lenv term term ≝
+ λh,o,L. tdeq h o.
+
definition cdeq_ext: ∀h. sd h → relation3 lenv bind bind ≝
λh,o. cext2 (cdeq h o).
interpretation
- "degree-based equivalence (binder)"
+ "context-free degree-based equivalence (binder)"
'LazyEq h o I1 I2 = (tdeq_ext h o I1 I2).
+
+interpretation
+ "context-dependent degree-based equivalence (term)"
+ 'LazyEq h o L T1 T2 = (cdeq h o L T1 T2).
+
+interpretation
+ "context-dependent degree-based equivalence (binder)"
+ 'LazyEq h o L I1 I2 = (cdeq_ext h o L I1 I2).
]
}
]
+*)
class "cyan"
[ { "rt-transition" * } {
(*
[ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ]
}
]
+*)
[ { "uncounted context-sensitive rt-transition" * } {
[ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
[ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ]
+ [ "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
[ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ]
}
]
-*)
[ { "counted context-sensitive rt-transition" * } {
[ "cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
}
projects / helm.git / commitdiff