- dependences on ceq and ceq_ext fixed

- lfeq (was lleq) reintroduced
- some renaming

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma
index 8f247592c9b7472e57862a5d346a72abe4a4fc93..53782a58dca04b261b8e92865ce60abe3fb76609 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma
@@ -12,29 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(*
 include "basic_2/static/lfeq.ma".
-*)
 include "basic_2/static/lfxs_lfxs.ma".
 include "basic_2/i_static/tc_lfxs_fqup.ma".
 
-include "basic_2/notation/relations/lazyeqsn_3.ma".
-
-definition ceq_ext: relation3 lenv bind bind ≝
-                    cext2 (λL,T1,T2. T1 = T2).
-
-definition lfeq: relation3 term lenv lenv ≝
-                 lfxs (λL,T1,T2. T1 = T2).
-
-interpretation
-   "syntactic equivalence on referred entries (local environment)"
-   'LazyEqSn T L1 L2 = (lfeq T L1 L2).
-
-axiom lfeq_lfxs_trans: ∀R,L1,L,T. L1 ≡[T] L →
-                       ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
-
-axiom cext2_inv_LTC: ∀R,L,I1,I2. cext2 (LTC … R) L I1 I2 → LTC … (cext2 R) L I1 I2.
 (*
+axiom cext2_inv_LTC: ∀R,L,I1,I2. cext2 (LTC … R) L I1 I2 → LTC … (cext2 R) L I1 I2.
+
 #R #L #I1 #I2 * -I1 -I2
 [ /2 width=1 by ext2_unit, inj/
 | #I #V1 #V2 #HV12 
@@ -51,9 +35,10 @@ lemma pippo: ∀RN,RP. (∀L. reflexive … (RP L)) →
 [ @step [3: 
 *)
 
+(*
 axiom lexs_frees_confluent_LTC_sn: ∀RN,RP. lexs_frees_confluent RN RP →
                                    lexs_frees_confluent (LTC … RN) RP.
-(*
+
 #RN #RP #HR #f1 #L1 #T #Hf1 #L2 #H  
 *)
 (* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_cext2.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_cext2.ma
new file mode 100644 (file)
index 0000000..f2a857d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_cext2.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/drops.ma".
+
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Properties with the extension to binders of a context-sensitive relation *)
+
+lemma cext2_d_liftable2_sn: ∀R. d_liftable2_sn … lifts R →
+                            d_liftable2_sn … liftsb (cext2 R).
+#R #HR #K #I1 #I2 * -I1 -I2 #I [| #T1 #T2 #HT12 ]
+#b #f #L #HLK #Z1 #H
+[ lapply (liftsb_inv_unit_sn … H)
+| lapply (liftsb_inv_pair_sn … H) * #U1 #HTU1
+] -H #H destruct /3 width=3 by ext2_unit, ex2_intro/
+elim (HR … HT12 … HLK … HTU1) -HR -b -K -T1 /3 width=3 by ext2_pair, ex2_intro/
+qed-. 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ext2.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ext2.ma
deleted file mode 100644 (file)
index 58e5358..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ext2.ma
+++ /dev/null
@@ -1,30 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/relocation/drops.ma".
-
-(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
-
-(* Properties with the extension to binders of a context-sensitive relation *)
-
-lemma cext2_d_liftable2_sn: ∀R. d_liftable2_sn … lifts R →
-                            d_liftable2_sn … liftsb (cext2 R).
-#R #HR #K #I1 #I2 * -I1 -I2 #I [| #T1 #T2 #HT12 ]
-#b #f #L #HLK #Z1 #H
-[ lapply (liftsb_inv_unit_sn … H)
-| lapply (liftsb_inv_pair_sn … H) * #U1 #HTU1
-] -H #H destruct /3 width=3 by ext2_unit, ex2_intro/
-elim (HR … HT12 … HLK … HTU1) -HR -b -K -T1 /3 width=3 by ext2_pair, ex2_intro/
-qed-. 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma
index 1442fa5525610a1e9a7801787d7edef22e25782f..cc3e75b0a5107964bdd5b503c9e8904aca6fa0d4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lazyeqsn_3.ma".
-include "basic_2/syntax/lenv_ceq.ma".
+include "basic_2/syntax/ceq_ext.ma".
 include "basic_2/relocation/lexs.ma".
 
 (* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma
index 434efb1376ab94c06fe1d1511d0794966786524f..b47bfc3e97602befc0c3796e93d783b859fc6c9b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/syntax/lenv_ext2.ma".
+include "basic_2/syntax/cext2.ma".
 include "basic_2/rt_transition/cpm.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR BINDERS **********************)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma
index e250ab490e6eb8616d80019823278e9c9d468449..16e73c92b636dbe6cfe92422fe4cc3ec723a27b3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/syntax/lenv_ext2.ma".
+include "basic_2/syntax/cext2.ma".
 include "basic_2/rt_transition/cpx.ma".
 
 (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR BINDERS ***********)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
index 8a770328f0758d0c063c21648c4058cabbb20915..df8af706d8069925c41640b541b76bc67726ab0d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
@@ -195,11 +195,3 @@ lemma lfdeq_fwd_flat_dx: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → L1 
 lemma lfdeq_fwd_dx: ∀h,o,I2,L1,K2. ∀T:term. L1 ≛[h, o, T] K2.ⓘ{I2} →
                     ∃∃I1,K1. L1 = K1.ⓘ{I1}.
 /2 width=5 by lfxs_fwd_dx/ qed-.
-
-(* Basic_2A1: removed theorems 10:
-              lleq_ind lleq_fwd_lref
-              lleq_fwd_drop_sn lleq_fwd_drop_dx
-              lleq_skip lleq_lref lleq_free
-              lleq_Y lleq_ge_up lleq_ge
-               
-*)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma
new file mode 100644 (file)
index 0000000..cc3fce3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lazyeqsn_3.ma".
+include "basic_2/static/lfxs.ma".
+
+(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
+
+(* Basic_2A1: was: lleq *)
+definition lfeq: relation3 term lenv lenv ≝
+                 lfxs ceq.
+
+interpretation
+   "syntactic equivalence on referred entries (local environment)"
+   'LazyEqSn T L1 L2 = (lfeq T L1 L2).
+
+(***************************************************)
+
+axiom lfeq_lfxs_trans: ∀R,L1,L,T. L1 ≡[T] L →
+                       ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
+
+(* Basic_2A1: removed theorems 10:
+              lleq_ind lleq_fwd_lref
+              lleq_fwd_drop_sn lleq_fwd_drop_dx
+              lleq_skip lleq_lref lleq_free
+              lleq_Y lleq_ge_up lleq_ge
+               
+*)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index 8fddc58967479ca39416bd6778be5ab544949dc5..9c0cc9c4a2ae74c7192ec287ed326945f0c41f67 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -14,7 +14,7 @@
 
 include "ground_2/relocation/rtmap_id.ma".
 include "basic_2/notation/relations/relationstar_4.ma".
-include "basic_2/syntax/lenv_ext2.ma".
+include "basic_2/syntax/cext2.ma".
 include "basic_2/relocation/lexs.ma".
 include "basic_2/static/frees.ma".
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
index 0eec7d41e3e49378704310c3e4df385b9a2e1b99..99b1ece949863003c3d475e1bdfb47e2f7127c28 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/relocation/drops_cext2.ma".
 include "basic_2/relocation/drops_lexs.ma".
-include "basic_2/relocation/drops_ext2.ma".
 include "basic_2/static/frees_drops.ma".
 include "basic_2/static/lfxs.ma".
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext.ma
new file mode 100644 (file)
index 0000000..f898401
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cext2.ma".
+
+(* CONTEXT-AWARE SYNTACTIC EQUIVALENCE FOR BINDERS **************************)
+
+definition ceq_ext: lenv → relation bind ≝
+                    cext2 ceq.
+
+(* Basic properties *********************************************************)
+
+lemma ceq_ext_refl (L): reflexive … (ceq_ext L).
+/2 width=1 by ext2_refl/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ceq_ext_inv_eq: ∀L,I1,I2. ceq_ext L I1 I2 → I1 = I2.
+#L #I1 #I2 * -I1 -I2 //
+qed-.   

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma
index 440bddba45d7b3a06c2d0b08c8807c2262c0fcde..2ab3768a0f10e0ed5e38f82c38309c7274867268 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/syntax/lenv_ceq.ma".
+include "basic_2/syntax/ceq_ext.ma".
 
-(* CONTEXT-DEPENDENT SYNTACTIC EQUIVALENCE FOR BINDERS **********************)
+(* CONTEXT-AWARE SYNTACTIC EQUIVALENCE FOR BINDERS **************************)
 
 (* Main properties **********************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/cext2.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/cext2.ma
new file mode 100644 (file)
index 0000000..6595ba7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/cext2.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ext2.ma".
+include "basic_2/syntax/lenv.ma".
+
+(* EXTENSION TO BINDERS OF A CONTEXT-SENSITIVE RELATION FOR TERMS ***********)
+
+definition cext2: (lenv → relation term) → lenv → relation bind ≝
+                  λR,L. ext2 (R L).
+
+(* Basic properties *********************************************************)
+
+lemma cext2_sym: ∀R. (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
+                 ∀L1,L2,I1,I2. cext2 R L1 I1 I2 → cext2 R L2 I2 I1.
+#R #HR #L1 #L2 #I1 #I2 * /3 width=2 by ext2_pair/
+qed-.
+
+lemma cext2_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
+                ∀L,I1,I2. cext2 R1 L I1 I2 → cext2 R2 L I1 I2.
+#R1 #R2 #HR #L #I1 #I2 * /3 width=2 by ext2_unit, ext2_pair/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma
deleted file mode 100644 (file)
index 8ae1e81..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma
+++ /dev/null
@@ -1,31 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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".
-
-(* EXTENSION TO BINDERS OF A CONTEXT-SENSITIVE RELATION FOR TERMS ***********)
-
-definition ceq_ext: lenv → relation bind ≝
-                    cext2 ceq.
-
-(* Basic properties *********************************************************)
-
-lemma ceq_ext_refl (L): reflexive … (ceq_ext L).
-/2 width=1 by ext2_refl/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma ceq_ext_inv_eq: ∀L,I1,I2. ceq_ext L I1 I2 → I1 = I2.
-#L #I1 #I2 * -I1 -I2 //
-qed-.   

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ext2.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ext2.ma
deleted file mode 100644 (file)
index 6595ba7..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ext2.ma
+++ /dev/null
@@ -1,33 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/ext2.ma".
-include "basic_2/syntax/lenv.ma".
-
-(* EXTENSION TO BINDERS OF A CONTEXT-SENSITIVE RELATION FOR TERMS ***********)
-
-definition cext2: (lenv → relation term) → lenv → relation bind ≝
-                  λR,L. ext2 (R L).
-
-(* Basic properties *********************************************************)
-
-lemma cext2_sym: ∀R. (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
-                 ∀L1,L2,I1,I2. cext2 R L1 I1 I2 → cext2 R L2 I2 I1.
-#R #HR #L1 #L2 #I1 #I2 * /3 width=2 by ext2_pair/
-qed-.
-
-lemma cext2_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
-                ∀L,I1,I2. cext2 R1 L I1 I2 → cext2 R2 L I1 I2.
-#R1 #R2 #HR #L #I1 #I2 * /3 width=2 by ext2_unit, ext2_pair/
-qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma
index 7cfeee246eead25381c8e18722462693c0dba6aa..93a3be18d31c3edc803e4a17429ad650e249b30b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/stareq_5.ma".
+include "basic_2/syntax/cext2.ma".
 include "basic_2/syntax/tdeq.ma".
-include "basic_2/syntax/lenv_ext2.ma".
 
 (* EXTENDED DEGREE-BASED EQUIVALENCE ****************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index d960b585944b286b4ae599fea8d048796b78b074..7d4282e13b0e3879ebdd02e74fea389b298cf3c3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -170,6 +170,9 @@ table {
              [ "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
           }
         ]
+        [ { "syntactic equivalence on referred entries" * } {
+             [ "lfeq ( ? ≡[?] ? )" * ]
+          }
         [ { "generic extension on referred entries" * } {
              [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ]
           }
@@ -207,7 +210,7 @@ table {
    [ { "relocation" * } {
         [ { "generic slicing for local environments" * } {
              [ "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ]
-             [ "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_ext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
+             [ "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
           }
         ]
         [ { "generic relocation" * } {
@@ -356,7 +359,7 @@ class "italic"            { 1 }
           }
         ]
         [ { "pointwise extension of a relation" * } {
-             [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
+             [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
           }
         ]
              [ "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ]