From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 6 Jul 2022 12:23:57 +0000 (+0200)
Subject: partial commit in delayed_updating
X-Git-Tag: make_still_working~50
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=306205b6853874cf485152222593b57249c6e7fa

partial commit in delayed_updating

+ reversing paths in component "syntax"
+ some renaming
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
index 9f8238432..1eb11fc03 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
@@ -24,8 +24,8 @@ include "ground/xoa/ex_5_3.ma".
 (* BY-DEPTH DELAYED (BDD) TERM **********************************************)
 
 inductive bdd: 𝒫❨prototerm❩ ≝
-| bdd_oref: ∀n. bdd (⧣n)
-| bdd_iref: ∀t,n. bdd t → bdd (𝛕n.t)
+| bdd_oref: ∀k. bdd (⧣k)
+| bdd_iref: ∀t,k. bdd t → bdd (𝛕k.t)
 | bdd_abst: ∀t. bdd t → bdd (𝛌.t)
 | bdd_appl: ∀u,t. bdd u → bdd t → bdd (＠u.t)
 | bdd_conv: ∀t1,t2. t1 ⇔ t2 → bdd t1 → bdd t2
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
index 98e63f06b..6a607559c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
@@ -35,7 +35,7 @@ inductive label: Type[0] ≝
 
 interpretation
   "variable reference by depth (label)"
-  'NodeLabelD p = (label_d p).
+  'NodeLabelD k = (label_d k).
 
 interpretation
   "mark (label)"
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
index 2d8abe304..39ac9c46c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
@@ -21,7 +21,8 @@ include "delayed_updating/syntax/label.ma".
 
 (* PATH *********************************************************************)
 
-(* Note: a path is a list of labels *) 
+(* Note: a path is a list of labels *)
+(* Note: constructed from the leaf (right end) to the root (left end) *)
 definition path ≝ list label.
 
 interpretation
@@ -29,13 +30,13 @@ interpretation
   'ElementE = (list_empty label).
 
 interpretation
-  "left cons (paths)"
-  'BlackHalfCircleRight l p = (list_lcons label l p).
+  "right cons (paths)"
+  'BlackHalfCircleLeft p l = (list_lcons label l p).
 
 interpretation
   "append (paths)"
-  'BlackCircle l1 l2 = (list_append label l1 l2).
+  'BlackCircle p q = (list_append label q p).
 
 interpretation
-  "right cons (paths)"
-  'BlackHalfCircleLeft p l = (list_append label p (list_lcons label l (list_empty label))).
+  "left cons (paths)"
+  'BlackHalfCircleRight l p = (list_append label p (list_lcons label l (list_empty label))).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
index 474bbcbda..eff4eb16b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -40,53 +40,58 @@ interpretation
 lemma depth_empty: 𝟎 = ♭𝐞.
 // qed.
 
-lemma depth_d_sn (q) (n): ♭q = ♭(𝗱n◗q).
+lemma depth_d_dx (p) (k):
+      ♭p = ♭(p◖𝗱k).
 // qed.
 
-lemma depth_m_sn (q): ♭q = ♭(𝗺◗q).
+lemma depth_m_dx (p):
+      ♭p = ♭(p◖𝗺).
 // qed.
 
-lemma depth_L_sn (q): ↑♭q = ♭(𝗟◗q).
+lemma depth_L_dx (p):
+      ↑♭p = ♭(p◖𝗟).
 // qed.
 
-lemma depth_A_sn (q): ♭q = ♭(𝗔◗q).
+lemma depth_A_dx (p):
+      ♭p = ♭(p◖𝗔).
 // qed.
 
-lemma depth_S_sn (q): ♭q = ♭(𝗦◗q).
+lemma depth_S_dx (p):
+      ♭p = ♭(p◖𝗦).
 // qed.
 
 (* Main constructions *******************************************************)
 
-theorem depth_append (p1) (p2):
-        (♭p2)+(♭p1) = ♭(p1●p2).
-#p1 elim p1 -p1 //
-* [ #n ] #p1 #IH #p2 <list_append_lcons_sn
-[ <depth_d_sn <depth_d_sn //
-| <depth_m_sn <depth_m_sn //
-| <depth_L_sn <depth_L_sn //
-| <depth_A_sn <depth_A_sn //
-| <depth_S_sn <depth_S_sn //
+theorem depth_append (p) (q):
+        (♭p)+(♭q) = ♭(p●q).
+#p #q elim q -q //
+* [ #k ] #q #IH <list_append_lcons_sn
+[ <depth_d_dx <depth_d_dx //
+| <depth_m_dx <depth_m_dx //
+| <depth_L_dx <depth_L_dx //
+| <depth_A_dx <depth_A_dx //
+| <depth_S_dx <depth_S_dx //
 ]
 qed.
 
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
 
-lemma depth_d_dx (p) (n):
-      ♭p = ♭(p◖𝗱n).
+lemma depth_d_sn (p) (k):
+      ♭p = ♭(𝗱k◗p).
 // qed.
 
-lemma depth_m_dx (p):
-      ♭p = ♭(p◖𝗺).
+lemma depth_m_sn (p):
+      ♭p = ♭(𝗺◗p).
 // qed.
 
-lemma depth_L_dx (p):
-      ↑♭p = ♭(p◖𝗟).
+lemma depth_L_sn (p):
+      ↑♭p = ♭(𝗟◗p).
 // qed.
 
-lemma depth_A_dx (p):
-      ♭p = ♭(p◖𝗔).
+lemma depth_A_sn (p):
+      ♭p = ♭(𝗔◗p).
 // qed.
 
-lemma depth_S_dx (p):
-      ♭p = ♭(p◖𝗦).
+lemma depth_S_sn (p):
+      ♭p = ♭(𝗦◗p).
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_labels.ma
index 1993633de..791a09a51 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_labels.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_labels.ma
@@ -22,5 +22,5 @@ include "delayed_updating/syntax/path_labels.ma".
 lemma depth_labels_L (n):
       n = ♭(𝗟∗∗n).
 #n @(nat_ind_succ … n) -n //
-#n #IH <labels_succ <depth_L_sn //
+#n #IH <labels_succ <depth_L_dx //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma
index 438c5e6a7..4610e4f69 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma
@@ -19,25 +19,25 @@ include "ground/arith/nat_pred_succ.ma".
 
 (* HEAD FOR PATH ************************************************************)
 
-rec definition path_head (m) (p) on p: path ≝
-match m with
+rec definition path_head (n) (p) on p: path ≝
+match n with
 [ nzero  ⇒ 𝐞
-| ninj o ⇒ 
+| ninj m ⇒
   match p with
-  [ list_empty     ⇒ 𝗟∗∗m
+  [ list_empty     ⇒ 𝗟∗∗n
   | list_lcons l q ⇒
     match l with
-    [ label_d n ⇒ l◗(path_head (m+n) q)
-    | label_m   ⇒ l◗(path_head m q)
-    | label_L   ⇒ l◗(path_head (↓o) q)
-    | label_A   ⇒ l◗(path_head m q)
-    | label_S   ⇒ l◗(path_head m q)
+    [ label_d k ⇒ (path_head (n+k) q)◖l
+    | label_m   ⇒ (path_head n q)◖l
+    | label_L   ⇒ (path_head (↓m) q)◖l
+    | label_A   ⇒ (path_head n q)◖l
+    | label_S   ⇒ (path_head n q)◖l
     ]
   ]
 ].
 
 interpretation
-  "head (reversed path)"
+  "head (path)"
   'DownArrowRight n p = (path_head n p).
 
 (* basic constructions ****************************************************)
@@ -50,26 +50,26 @@ lemma path_head_empty (n):
       (𝗟∗∗n) = ↳[n]𝐞.
 * // qed.
 
-lemma path_head_d_sn (p) (n) (m:pnat):
-      (𝗱m◗↳[↑n+m]p) = ↳[↑n](𝗱m◗p).
+lemma path_head_d_dx (p) (n) (k:pnat):
+      (↳[↑n+k]p)◖𝗱k = ↳[↑n](p◖𝗱k).
 // qed.
 
-lemma path_head_m_sn (p) (n):
-      (𝗺◗↳[↑n]p) = ↳[↑n](𝗺◗p).
+lemma path_head_m_dx (p) (n):
+      (↳[↑n]p)◖𝗺 = ↳[↑n](p◖𝗺).
 // qed.
 
-lemma path_head_L_sn (p) (n):
-      (𝗟◗↳[n]p) = ↳[↑n](𝗟◗p).
+lemma path_head_L_dx (p) (n):
+      (↳[n]p)◖𝗟 = ↳[↑n](p◖𝗟).
 #p #n
 whd in ⊢ (???%); //
 qed.
 
-lemma path_head_A_sn (p) (n):
-      (𝗔◗↳[↑n]p) = ↳[↑n](𝗔◗p).
+lemma path_head_A_dx (p) (n):
+      (↳[↑n]p)◖𝗔 = ↳[↑n](p◖𝗔).
 // qed.
 
-lemma path_head_S_sn (p) (n):
-      (𝗦◗↳[↑n]p) = ↳[↑n](𝗦◗p).
+lemma path_head_S_dx (p) (n):
+      (↳[↑n]p)◖𝗦 = ↳[↑n](p◖𝗦).
 // qed.
 
 (* Basic inversions *********************************************************)
@@ -82,51 +82,51 @@ qed-.
 lemma eq_inv_path_empty_head (p) (n):
       (𝐞) = ↳[n]p → 𝟎 = n.
 *
-[ #m <path_head_empty #H0
-  <(eq_inv_empty_labels … H0) -m //
-| * [ #n ] #p #n @(nat_ind_succ … n) -n // #m #_
-  [ <path_head_d_sn
-  | <path_head_m_sn
-  | <path_head_L_sn
-  | <path_head_A_sn
-  | <path_head_S_sn
+[ #n <path_head_empty #H0
+  <(eq_inv_empty_labels … H0) -n //
+| * [ #k ] #p #n @(nat_ind_succ … n) -n // #n #_
+  [ <path_head_d_dx
+  | <path_head_m_dx
+  | <path_head_L_dx
+  | <path_head_A_dx
+  | <path_head_S_dx
   ] #H0 destruct
 ]
 qed-.
 
-(* Constructions with list_append *******************************************)
+(* Constructions with path_append *******************************************)
 
 lemma path_head_refl_append (p) (q) (n):
-      q = ↳[n]q → q = ↳[n](q●p).
+      q = ↳[n]q → q = ↳[n](p●q).
 #p #q elim q -q
 [ #n #Hn <(eq_inv_path_empty_head … Hn) -Hn //
 | #l #q #IH #n @(nat_ind_succ … n) -n
-  [ #Hq | #n #_ cases l [ #m ] ]
+  [ #Hq | #n #_ cases l [ #k ] ]
   [ lapply (eq_inv_path_head_zero_dx … Hq) -Hq #Hq destruct
-  | <path_head_d_sn <path_head_d_sn
-  | <path_head_m_sn <path_head_m_sn
-  | <path_head_L_sn <path_head_L_sn
-  | <path_head_A_sn <path_head_A_sn
-  | <path_head_S_sn <path_head_S_sn
+  | <path_head_d_dx <path_head_d_dx
+  | <path_head_m_dx <path_head_m_dx
+  | <path_head_L_dx <path_head_L_dx
+  | <path_head_A_dx <path_head_A_dx
+  | <path_head_S_dx <path_head_S_dx
   ] #Hq
   elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
   /3 width=1 by eq_f/
 ]
 qed-.
 
-(* Inversions with list_append **********************************************)
+(* Inversions with path_append **********************************************)
 
 lemma eq_inv_path_head_refl_append (p) (q) (n):
-      q = ↳[n](q●p) → q = ↳[n]q.
+      q = ↳[n](p●q) → q = ↳[n]q.
 #p #q elim q -q
 [ #n #Hn <(eq_inv_path_empty_head … Hn) -p //
 | #l #q #IH #n @(nat_ind_succ … n) -n //
-  #n #_ cases l [ #m ]
-  [ <path_head_d_sn <path_head_d_sn
-  | <path_head_m_sn <path_head_m_sn
-  | <path_head_L_sn <path_head_L_sn
-  | <path_head_A_sn <path_head_A_sn
-  | <path_head_S_sn <path_head_S_sn
+  #n #_ cases l [ #k ]
+  [ <path_head_d_dx <path_head_d_dx
+  | <path_head_m_dx <path_head_m_dx
+  | <path_head_L_dx <path_head_L_dx
+  | <path_head_A_dx <path_head_A_dx
+  | <path_head_S_dx <path_head_S_dx
   ] #Hq
   elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
   /3 width=1 by eq_f/
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma
index c561797c1..6283e2c21 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma
@@ -24,12 +24,12 @@ lemma path_head_depth (p) (n):
       n + ♯(↳[n]p) = ♭↳[n]p.
 #p elim p -p // #l #p #IH
 #n @(nat_ind_succ … n) -n // #n #_
-cases l [ #m ]
-[ <path_head_d_sn <height_d_sn <depth_d_sn //
-| <path_head_m_sn <height_m_sn <depth_m_sn //
-| <path_head_L_sn <height_L_sn <depth_L_sn
+cases l [ #k ]
+[ <path_head_d_dx <height_d_dx <depth_d_dx <IH //
+| <path_head_m_dx <height_m_dx <depth_m_dx //
+| <path_head_L_dx <height_L_dx <depth_L_dx
   <nplus_succ_sn //
-| <path_head_A_sn <height_A_sn <depth_A_sn //
-| <path_head_S_sn <height_S_sn <depth_S_sn //
+| <path_head_A_dx <height_A_dx <depth_A_dx //
+| <path_head_S_dx <height_S_dx <depth_S_dx //
 ]
 qed-. (**) (* gets in the way with auto *)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_structure.ma
index e1605752c..37ca7be2c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_structure.ma
@@ -19,21 +19,21 @@ include "delayed_updating/syntax/path_structure_labels.ma".
 
 (* Constructions with structure *********************************************)
 
-lemma path_head_structure_height (p) (m):
-      ⊗↳[m]p = ↳[m+♯↳[m]p]⊗p.
+lemma path_head_structure_height (p) (n):
+      ⊗↳[n]p = ↳[n+♯↳[n]p]⊗p.
 #p elim p -p //
-#l #p #IH #m @(nat_ind_succ … m) -m //
-#m #_ cases l [ #n ]
-[ <height_d_sn <structure_d_sn //
-| <structure_m_sn //
-| <structure_L_sn //
-| <height_A_sn <structure_A_sn <nplus_succ_sn <path_head_A_sn //
-| <height_S_sn <structure_S_sn <nplus_succ_sn <path_head_S_sn //
+#l #p #IH #n @(nat_ind_succ … n) -n //
+#n #_ cases l [ #k ]
+[ <height_d_dx <structure_d_dx //
+| <structure_m_dx //
+| <structure_L_dx //
+| <height_A_dx <structure_A_dx <nplus_succ_sn <path_head_A_dx //
+| <height_S_dx <structure_S_dx <nplus_succ_sn <path_head_S_dx //
 ]
 qed.
 
-lemma path_head_structure_depth (p) (m):
-      ⊗↳[m]p = ↳[♭↳[m]p]⊗p.
-#p #m
+lemma path_head_structure_depth (p) (n):
+      ⊗↳[n]p = ↳[♭↳[n]p]⊗p.
+#p #n
 <path_head_depth //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma
index 73c7e21e9..934df56d0 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma
@@ -23,7 +23,7 @@ match p with
 [ list_empty     ⇒ 𝟎
 | list_lcons l q ⇒
   match l with
-  [ label_d n ⇒ n + height q
+  [ label_d k ⇒ height q + k
   | label_m   ⇒ height q
   | label_L   ⇒ height q
   | label_A   ⇒ height q
@@ -40,53 +40,58 @@ interpretation
 lemma height_empty: 𝟎 = ♯𝐞.
 // qed.
 
-lemma height_d_sn (q) (n): ninj n+♯q = ♯(𝗱n◗q).
+lemma height_d_dx (p) (k:pnat):
+      (♯p)+k = ♯(p◖𝗱k).
 // qed.
 
-lemma height_m_sn (q): ♯q = ♯(𝗺◗q).
+lemma height_m_dx (p):
+      (♯p) = ♯(p◖𝗺).
 // qed.
 
-lemma height_L_sn (q): ♯q = ♯(𝗟◗q).
+lemma height_L_dx (p):
+      (♯p) = ♯(p◖𝗟).
 // qed.
 
-lemma height_A_sn (q): ♯q = ♯(𝗔◗q).
+lemma height_A_dx (p):
+      (♯p) = ♯(p◖𝗔).
 // qed.
 
-lemma height_S_sn (q): ♯q = ♯(𝗦◗q).
+lemma height_S_dx (p):
+      (♯p) = ♯(p◖𝗦).
 // qed.
 
 (* Main constructions *******************************************************)
 
-theorem height_append (p1) (p2):
-        (♯p2+♯p1) = ♯(p1●p2).
-#p1 elim p1 -p1 //
-* [ #n ] #p1 #IH #p2 <list_append_lcons_sn
-[ <height_d_sn <height_d_sn //
-| <height_m_sn <height_m_sn //
-| <height_L_sn <height_L_sn //
-| <height_A_sn <height_A_sn //
-| <height_S_sn <height_S_sn //
+theorem height_append (p) (q):
+        (♯p+♯q) = ♯(p●q).
+#p #q elim q -q //
+* [ #k ] #q #IH <list_append_lcons_sn
+[ <height_d_dx <height_d_dx //
+| <height_m_dx <height_m_dx //
+| <height_L_dx <height_L_dx //
+| <height_A_dx <height_A_dx //
+| <height_S_dx <height_S_dx //
 ]
 qed.
 
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
 
-lemma height_d_dx (p) (n):
-      (♯p)+(ninj n) = ♯(p◖𝗱n).
+lemma height_d_sn (p) (k:pnat):
+      k+♯p = ♯(𝗱k◗p).
 // qed.
 
-lemma height_m_dx (p):
-      (♯p) = ♯(p◖𝗺).
+lemma height_m_sn (p):
+      ♯p = ♯(𝗺◗p).
 // qed.
 
-lemma height_L_dx (p):
-      (♯p) = ♯(p◖𝗟).
+lemma height_L_sn (p):
+      ♯p = ♯(𝗟◗p).
 // qed.
 
-lemma height_A_dx (p):
-      (♯p) = ♯(p◖𝗔).
+lemma height_A_sn (p):
+      ♯p = ♯(𝗔◗p).
 // qed.
 
-lemma height_S_dx (p):
-      (♯p) = ♯(p◖𝗦).
+lemma height_S_sn (p):
+      ♯p = ♯(𝗦◗p).
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height_labels.ma
index cf9a6d5c2..fb55c3606 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height_labels.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height_labels.ma
@@ -22,5 +22,5 @@ include "delayed_updating/syntax/path_labels.ma".
 lemma height_labels_L (n):
       (𝟎) = ♯(𝗟∗∗n).
 #n @(nat_ind_succ … n) -n //
-#n #IH <labels_succ <height_L_sn //
+#n #IH <labels_succ <height_L_dx //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
index 8e9fccefe..98501e8df 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -19,7 +19,7 @@ include "ground/lib/subset.ma".
 (* INNER CONDITION FOR PATH *************************************************)
 
 definition pic: predicate path ≝
-           λp. ∀q,n. q◖𝗱n = p → ⊥
+           λp. ∀q,k. q◖𝗱k = p → ⊥
 .
 
 interpretation
@@ -28,34 +28,34 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma pic_empty: 𝐞 ϵ 𝐈.
-#q #n #H0
-elim (eq_inv_list_empty_rcons ??? (sym_eq … H0))
+lemma pic_empty:
+      (𝐞) ϵ 𝐈.
+#q #k #H0 destruct
 qed.
 
-lemma pic_m_dx (p): p◖𝗺 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_m_dx (p):
+      p◖𝗺 ϵ 𝐈.
+#p #q #k #H0 destruct
 qed.
 
-lemma pic_L_dx (p): p◖𝗟 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_L_dx (p):
+      p◖𝗟 ϵ 𝐈.
+#p #q #k #H0 destruct
 qed.
 
-lemma pic_A_dx (p): p◖𝗔 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_A_dx (p):
+      p◖𝗔 ϵ 𝐈.
+#p #q #k #H0 destruct
 qed.
 
-lemma pic_S_dx (p): p◖𝗦 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_S_dx (p):
+      p◖𝗦 ϵ 𝐈.
+#p #q #k #H0 destruct
 qed.
 
 (* Basic inversions ********************************************************)
 
-lemma pic_inv_d_dx (p) (n):
-      p◖𝗱n ϵ 𝐈 → ⊥.
-#p #n #H0 @H0 -H0 //
+lemma pic_inv_d_dx (p) (k):
+      p◖𝗱k ϵ 𝐈 → ⊥.
+#p #k #H0 @H0 -H0 //
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma
index e7e1391da..7f0a71a8c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma
@@ -36,7 +36,7 @@ lemma labels_zero (l):
 // qed.
 
 lemma labels_succ (l) (n):
-      l◗(l∗∗n) = l∗∗(↑n).
+      (l∗∗n)◖l = l∗∗(↑n).
 #l #n
 <labels_unfold <labels_unfold <niter_succ //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
index ff6a53c39..5d2963362 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
@@ -29,13 +29,15 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma ppc_lcons (l) (q): l◗q ϵ 𝐏.
-#l #q #H0 destruct
+lemma ppc_rcons (p) (l):
+      p◖l ϵ 𝐏.
+#p #l #H0 destruct
 qed.
 
-lemma ppc_rcons (l) (q): q◖l ϵ 𝐏.
-#l #q #H
-elim (eq_inv_list_empty_rcons ??? H)
+lemma ppc_lcons (p) (l):
+      l◗p ϵ 𝐏.
+#p #l #H0
+elim (eq_inv_list_empty_rcons ??? H0)
 qed.
 
 (* Basic inversions ********************************************************)
@@ -45,16 +47,16 @@ lemma ppc_inv_empty:
 #H0 @H0 -H0 //
 qed-.
 
-lemma ppc_inv_lcons (p):
-      p ϵ 𝐏 → ∃∃l,q. l◗q = p.
+lemma ppc_inv_rcons (p):
+      p ϵ 𝐏 → ∃∃q,l. q◖l = p.
 *
 [ #H0 elim (ppc_inv_empty … H0)
 | #l #q #_ /2 width=3 by ex1_2_intro/
 ]
 qed-.
 
-lemma ppc_inv_rcons (p):
-      p ϵ 𝐏 → ∃∃q,l. q◖l = p.
+lemma ppc_inv_lcons (p):
+      p ϵ 𝐏 → ∃∃q,l. l◗q = p.
 #p @(list_ind_rcons … p) -p
 [ #H0 elim (ppc_inv_empty … H0)
 | #q #l #_ #_ /2 width=3 by ex1_2_intro/
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
index 0330665ad..a9d9dd18f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -22,11 +22,11 @@ match p with
 [ list_empty     ⇒ 𝐞
 | list_lcons l q ⇒
    match l with
-   [ label_d n ⇒ structure q
+   [ label_d k ⇒ structure q
    | label_m   ⇒ structure q
-   | label_L   ⇒ 𝗟◗structure q
-   | label_A   ⇒ 𝗔◗structure q
-   | label_S   ⇒ 𝗦◗structure q
+   | label_L   ⇒ (structure q)◖𝗟
+   | label_A   ⇒ (structure q)◖𝗔
+   | label_S   ⇒ (structure q)◖𝗦
    ]
 ].
 
@@ -40,62 +40,62 @@ lemma structure_empty:
       𝐞 = ⊗𝐞.
 // qed.
 
-lemma structure_d_sn (p) (n):
-      ⊗p = ⊗(𝗱n◗p).
+lemma structure_d_dx (p) (k):
+      ⊗p = ⊗(p◖𝗱k).
 // qed.
 
-lemma structure_m_sn (p):
-      ⊗p = ⊗(𝗺◗p).
+lemma structure_m_dx (p):
+      ⊗p = ⊗(p◖𝗺).
 // qed.
 
-lemma structure_L_sn (p):
-      (𝗟◗⊗p) = ⊗(𝗟◗p).
+lemma structure_L_dx (p):
+      (⊗p)◖𝗟 = ⊗(p◖𝗟).
 // qed.
 
-lemma structure_A_sn (p):
-      (𝗔◗⊗p) = ⊗(𝗔◗p).
+lemma structure_A_dx (p):
+      (⊗p)◖𝗔 = ⊗(p◖𝗔).
 // qed.
 
-lemma structure_S_sn (p):
-      (𝗦◗⊗p) = ⊗(𝗦◗p).
+lemma structure_S_dx (p):
+      (⊗p)◖𝗦 = ⊗(p◖𝗦).
 // qed.
 
 (* Main constructions *******************************************************)
 
 theorem structure_idem (p):
         ⊗p = ⊗⊗p.
-#p elim p -p [| * [ #n ] #p #IH ] //
+#p elim p -p [| * [ #k ] #p #IH ] //
 qed.
 
-theorem structure_append (p1) (p2):
-        ⊗p1●⊗p2 = ⊗(p1●p2).
-#p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
+theorem structure_append (p) (q):
+        ⊗p●⊗q = ⊗(p●q).
+#p #q elim q -q [| * [ #k ] #q #IH ]
 [||*: <list_append_lcons_sn ] //
 qed.
 
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
 
-lemma structure_d_dx (p) (n):
-      ⊗p = ⊗(p◖𝗱n).
+lemma structure_d_sn (p) (k):
+      ⊗p = ⊗(𝗱k◗p).
 #p #n <structure_append //
 qed.
 
-lemma structure_m_dx (p):
-      ⊗p = ⊗(p◖𝗺).
+lemma structure_m_sn (p):
+      ⊗p = ⊗(𝗺◗p).
 #p <structure_append //
 qed.
 
-lemma structure_L_dx (p):
-      (⊗p)◖𝗟 = ⊗(p◖𝗟).
+lemma structure_L_sn (p):
+      (𝗟◗⊗p) = ⊗(𝗟◗p).
 #p <structure_append //
 qed.
 
-lemma structure_A_dx (p):
-      (⊗p)◖𝗔 = ⊗(p◖𝗔).
+lemma structure_A_sn (p):
+      (𝗔◗⊗p) = ⊗(𝗔◗p).
 #p <structure_append //
 qed.
 
-lemma structure_S_dx (p):
-      (⊗p)◖𝗦 = ⊗(p◖𝗦).
+lemma structure_S_sn (p):
+      (𝗦◗⊗p) = ⊗(𝗦◗p).
 #p <structure_append //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
index 464821793..67b3e661f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
@@ -22,9 +22,9 @@ include "delayed_updating/syntax/path_depth.ma".
 lemma depth_structure (p):
       ♭p = ♭⊗p.
 #p elim p -p //
-* [ #n ] #p #IH //
-[ <structure_L_sn <depth_L_sn <depth_L_sn //
-| <structure_A_sn <depth_A_sn <depth_A_sn //
-| <structure_S_sn <depth_S_sn <depth_S_sn //
+* [ #k ] #p #IH //
+[ <structure_L_dx <depth_L_dx <depth_L_dx //
+| <structure_A_dx <depth_A_dx <depth_A_dx //
+| <structure_S_dx <depth_S_dx <depth_S_dx //
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
index 5c0e5e6eb..99ed6a323 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
@@ -21,9 +21,9 @@ include "delayed_updating/syntax/path_inner.ma".
 
 lemma structure_pic (p):
       ⊗p ϵ 𝐈.
-#p @(list_ind_rcons … p) -p
+#p elim p -p
 [ <structure_empty //
-| #p * [ #n ] #IH
+| * [ #k ] #p #IH
   [ <structure_d_dx //
   | <structure_m_dx //
   | <structure_L_dx //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
index 4d428e5ba..6406d1dd7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
@@ -30,12 +30,12 @@ interpretation
 
 (* Basic inversions *********************************************************)
 
-lemma preterm_in_root_append_inv_structure_empty_dx (t) (p) (r):
-      p●r ϵ ▵t → t ϵ 𝐓 →  𝐞 = ⊗r → 𝐞 = r.
-#t #p #r #Hpr #Ht #Hr
-lapply (Ht p ?? Hpr ?)
+lemma preterm_in_root_append_inv_structure_empty_dx (t) (p) (q):
+      p●q ϵ ▵t → t ϵ 𝐓 → 𝐞 = ⊗q → 𝐞 = q.
+#t #p #q #Hpq #Ht #Hq
+lapply (Ht p ?? Hpq ?)
 [ <structure_append //
 | /2 width=2 by prototerm_in_root_append_des_sn/
-| /2 width=3 by eq_inv_list_append_dx_sn_refl/
+| /2 width=3 by eq_inv_list_append_dx_dx_refl/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
index f026c769e..5bb66e16a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
@@ -41,11 +41,11 @@ interpretation
 
 interpretation
   "outer variable reference by depth (prototerm)"
-  'Hash n = (prototerm_node_0 (label_d n)).
+  'Hash k = (prototerm_node_0 (label_d k)).
 
 interpretation
   "inner variable reference by depth (prototerm)"
-  'Tau n t = (prototerm_node_1_2 (label_d n) label_m t).
+  'Tau k t = (prototerm_node_1_2 (label_d k) label_m t).
 
 interpretation
   "name-free functional abstraction (prototerm)"
@@ -57,18 +57,19 @@ interpretation
 
 (* Basic constructions *******************************************************)
 
-lemma in_comp_iref (t) (q) (n):
-      q ϵ t → 𝗱n◗𝗺◗q ϵ 𝛕n.t.
+lemma in_comp_iref (t) (q) (k):
+      q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t.
 /2 width=3 by ex2_intro/ qed.
 
 (* Basic inversions *********************************************************)
 
-lemma in_comp_inv_iref (t) (p) (n):
-      p ϵ 𝛕n.t →
-      ∃∃q. 𝗱n◗𝗺◗q = p & q ϵ t.
-#t #p #n * #q #Hq #Hp
+lemma in_comp_inv_iref (t) (p) (k):
+      p ϵ 𝛕k.t →
+      ∃∃q. 𝗱k◗𝗺◗q = p & q ϵ t.
+#t #p #k * #q #Hq #Hp
 /2 width=3 by ex2_intro/
 qed-.
+
 (* COMMENT
 lemma prototerm_in_root_inv_lcons_oref:
       ∀p,l,n. l◗p ϵ ▵#n →
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
index 46e945ede..4a83b790e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
@@ -19,7 +19,7 @@ include "ground/lib/subset_ext_equivalence.ma".
 
 (* Constructions with equivalence for prototerm *****************************)
 
-lemma iref_eq_repl (t1) (t2) (n):
-      t1 ⇔ t2 → 𝛕n.t1 ⇔ 𝛕n.t2.
+lemma iref_eq_repl (t1) (t2) (k):
+      t1 ⇔ t2 → 𝛕k.t1 ⇔ 𝛕k.t2.
 /2 width=1 by subset_equivalence_ext_f1_bi/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
index 309eb0024..f7f921bcf 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
@@ -19,7 +19,7 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 
 (* Constructions with prototerm constructors ********************************)
 
-lemma ppc_iref (t) (n):
-      (𝛕n.t) ϵ 𝐏.
-#t #n #p * #q #Hq #H0 destruct //
+lemma ppc_iref (t) (k):
+      (𝛕k.t) ϵ 𝐏.
+#t #k #p * #q #Hq #H0 destruct //
 qed.