From 797a607af83f82102033270087722a7e59ddcd17 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 8 Sep 2022 13:02:59 +0200
Subject: [PATCH] partial update in delayed_updating

+ we add reference by depth with offset
+ component "syntax" updated
+ some improvements
+ height parked for now
---
 .../height/path_closed_height.etc}            |  0
 .../height/path_height.etc}                   |  0
 .../sharp_1.ma => etc/height/sharp_1.etc}     |  0
 .../lambdadelta/delayed_updating/names.txt    |  1 +
 .../notation/functions/nodelabel_d_1.ma       |  4 +-
 .../notation/functions/nodelabel_d_2.ma       | 19 +++++
 .../notation/functions/tau_3.ma               | 19 +++++
 .../delayed_updating/syntax/label.ma          | 18 +++--
 .../syntax/path_closed_structure.ma           | 16 ++--
 .../delayed_updating/syntax/path_depth.ma     | 22 ++++--
 .../delayed_updating/syntax/path_inner.ma     | 65 +++++-----------
 .../delayed_updating/syntax/path_structure.ma | 75 +++++++++++++++----
 .../syntax/path_structure_inner.ma            |  3 +-
 .../syntax/prototerm_constructors.ma          | 16 ++++
 .../syntax/prototerm_proper_constructors.ma   |  5 ++
 15 files changed, 176 insertions(+), 87 deletions(-)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{syntax/path_closed_height.ma => etc/height/path_closed_height.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{syntax/path_height.ma => etc/height/path_height.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/sharp_1.ma => etc/height/sharp_1.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_2.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_3.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_height.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_height.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_height.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_height.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/sharp_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/sharp_1.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/sharp_1.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/height/sharp_1.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/names.txt b/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
index aee943494..cd980b568 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
@@ -1,6 +1,7 @@
 METAVARIABLES
 
   b         : balanced path
+  d         : depth
   f, g      : update function
   h, k      : reference index by depth
   l         : label
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma
index 15767cf59..5a6343c5a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( 𝗱 break term 70 a )"
+notation "hvbox( 𝗱 break term 70 k )"
   non associative with precedence 70
-  for @{ 'NodeLabelD $a }.
+  for @{ 'NodeLabelD $k }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_2.ma
new file mode 100644
index 000000000..823902606
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝗱 ❨ break term 46 k, break term 46 d ❩ )"
+  non associative with precedence 70
+  for @{ 'NodeLabelD $k $d }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_3.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_3.ma
new file mode 100644
index 000000000..204dd898e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_3.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝛕 ❨ break term 46 k, break term 46 d ❩. break term 70 t )"
+  non associative with precedence 70
+  for @{ 'Tau $k $d $t }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
index 6a607559c..7106e0b0b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
@@ -16,8 +16,9 @@
  * Initial invocation: - Patience on me to gain peace and perfection! -
  *)
 
-include "ground/arith/pnat.ma".
+include "ground/arith/nat.ma".
 include "delayed_updating/notation/functions/nodelabel_d_1.ma".
+include "delayed_updating/notation/functions/nodelabel_d_2.ma".
 include "delayed_updating/notation/functions/nodelabel_m_0.ma".
 include "delayed_updating/notation/functions/edgelabel_l_0.ma".
 include "delayed_updating/notation/functions/edgelabel_a_0.ma".
@@ -26,17 +27,22 @@ include "delayed_updating/notation/functions/edgelabel_s_0.ma".
 (* LABEL ********************************************************************)
 
 inductive label: Type[0] ≝
-| label_d: pnat → label
-| label_m: label
-| label_L: label
-| label_A: label
-| label_S: label
+| label_d : pnat → label
+| label_d2: pnat → nat → label
+| label_m : label
+| label_L : label
+| label_A : label
+| label_S : label
 .
 
 interpretation
   "variable reference by depth (label)"
   'NodeLabelD k = (label_d k).
 
+interpretation
+  "variable reference by depth with offset (label)"
+  'NodeLabelD k d = (label_d2 k d).
+
 interpretation
   "mark (label)"
   'NodeLabelM = (label_m).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_structure.ma
index 90522f905..99b0a9235 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_structure.ma
@@ -12,22 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/syntax/path_closed_height.ma".
+include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_depth.ma".
 
 (* CLOSED CONDITION FOR PATH ************************************************)
 
 (* Constructions with structure *********************************************)
 
-lemma path_closed_structure_height (p) (n):
-      p ϵ 𝐂❨n❩ → ⊗p ϵ 𝐂❨♯p+n❩.
-#p #n #Hn elim Hn -Hn //
-#p #n #_ #IH [ <nplus_succ_dx ]
+lemma path_closed_structure_depth (p):
+      ⊗p ϵ 𝐂❨♭p❩.
+#p elim p -p // *
 /2 width=1 by pcc_L_dx, pcc_A_dx, pcc_S_dx/
 qed.
-
-lemma path_closed_structure_depth (p) (n):
-      p ϵ 𝐂❨n❩ → ⊗p ϵ 𝐂❨♭p❩.
-#p #n #Hp <path_closed_depth
-/2 width=3 by path_closed_structure_height/
-qed.
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 eff4eb16b..2e638b8ac 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -23,11 +23,12 @@ match p with
 [ list_empty     ⇒ 𝟎
 | list_lcons l q ⇒
   match l with
-  [ label_d _ ⇒ depth q
-  | label_m   ⇒ depth q
-  | label_L   ⇒ ↑(depth q)
-  | label_A   ⇒ depth q
-  | label_S   ⇒ depth q
+  [ label_d k    ⇒ depth q
+  | label_d2 k d ⇒ depth q
+  | label_m      ⇒ depth q
+  | label_L      ⇒ ↑(depth q)
+  | label_A      ⇒ depth q
+  | label_S      ⇒ depth q
   ]
 ].
 
@@ -44,6 +45,10 @@ lemma depth_d_dx (p) (k):
       ♭p = ♭(p◖𝗱k).
 // qed.
 
+lemma depth_d2_dx (p) (k) (d):
+      ♭p = ♭(p◖𝗱❨k,d❩).
+// qed.
+
 lemma depth_m_dx (p):
       ♭p = ♭(p◖𝗺).
 // qed.
@@ -65,8 +70,9 @@ lemma depth_S_dx (p):
 theorem depth_append (p) (q):
         (♭p)+(♭q) = ♭(p●q).
 #p #q elim q -q //
-* [ #k ] #q #IH <list_append_lcons_sn
+* [ #k | #k #d ] #q #IH <list_append_lcons_sn
 [ <depth_d_dx <depth_d_dx //
+| <depth_d2_dx <depth_d2_dx //
 | <depth_m_dx <depth_m_dx //
 | <depth_L_dx <depth_L_dx //
 | <depth_A_dx <depth_A_dx //
@@ -80,6 +86,10 @@ lemma depth_d_sn (p) (k):
       ♭p = ♭(𝗱k◗p).
 // qed.
 
+lemma depth_d2_sn (p) (k) (d):
+      ♭p = ♭(𝗱❨k,d❩◗p).
+// qed.
+
 lemma depth_m_sn (p):
       ♭p = ♭(𝗺◗p).
 // 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 0db6d2f65..25678301b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -15,81 +15,54 @@
 include "delayed_updating/syntax/path.ma".
 include "delayed_updating/notation/functions/class_i_0.ma".
 include "ground/lib/subset.ma".
+include "ground/generated/insert_eq_1.ma".
 
 (* INNER CONDITION FOR PATH *************************************************)
 
-definition pic: predicate path ≝
-           λp. ∀q,k. q◖𝗱k = p → ⊥
+inductive pic: predicate path ≝
+| pic_empty: (𝐞) ϵ pic
+| pic_m_dx (p): p◖𝗺 ϵ pic
+| pic_L_dx (p): p◖𝗟 ϵ pic
+| pic_A_dx (p): p◖𝗔 ϵ pic
+| pic_S_dx (p): p◖𝗦 ϵ pic
 .
 
 interpretation
   "inner condition (path)"
   'ClassI = (pic).
 
-(* Basic constructions ******************************************************)
-
-lemma pic_empty:
-      (𝐞) ϵ 𝐈.
-#q #k #H0 destruct
-qed.
-
-lemma pic_m_dx (p):
-      p◖𝗺 ϵ 𝐈.
-#p #q #k #H0 destruct
-qed.
-
-lemma pic_L_dx (p):
-      p◖𝗟 ϵ 𝐈.
-#p #q #k #H0 destruct
-qed.
-
-lemma pic_A_dx (p):
-      p◖𝗔 ϵ 𝐈.
-#p #q #k #H0 destruct
-qed.
-
-lemma pic_S_dx (p):
-      p◖𝗦 ϵ 𝐈.
-#p #q #k #H0 destruct
-qed.
-
 (* Basic inversions ********************************************************)
 
 lemma pic_inv_d_dx (p) (k):
       p◖𝗱k ϵ 𝐈 → ⊥.
-#p #k #H0 @H0 -H0 //
+#p #k @(insert_eq_1 … (p◖𝗱k))
+#q * -q [|*: #q ] #H0 destruct
+qed-.
+
+lemma pic_inv_d2_dx (p) (k) (d):
+      p◖𝗱❨k,d❩ ϵ 𝐈 → ⊥.
+#p #k #d @(insert_eq_1 … (p◖𝗱❨k,d❩))
+#q * -q [|*: #q ] #H0 destruct
 qed-.
 
 (* Constructions with path_lcons ********************************************)
 
 lemma pic_m_sn (p):
       p ϵ 𝐈 → 𝗺◗p ϵ 𝐈.
-* [| * [ #k ] #p #Hp <list_cons_shift ] //
-[ #_ <list_cons_comm //
-| elim (pic_inv_d_dx … Hp)
-]
+#p * -p //
 qed.
 
 lemma pic_L_sn (p):
       p ϵ 𝐈 → 𝗟◗p ϵ 𝐈.
-* [| * [ #k ] #p #Hp <list_cons_shift ] //
-[ #_ <list_cons_comm //
-| elim (pic_inv_d_dx … Hp)
-]
+#p * -p //
 qed.
 
 lemma pic_A_sn (p):
       p ϵ 𝐈 → 𝗔◗p ϵ 𝐈.
-* [| * [ #k ] #p #Hp <list_cons_shift ] //
-[ #_ <list_cons_comm //
-| elim (pic_inv_d_dx … Hp)
-]
+#p * -p //
 qed.
 
 lemma pic_S_sn (p):
       p ϵ 𝐈 → 𝗦◗p ϵ 𝐈.
-* [| * [ #k ] #p #Hp <list_cons_shift ] //
-[ #_ <list_cons_comm //
-| elim (pic_inv_d_dx … Hp)
-]
+#p * -p //
 qed.
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 3b91954fd..95c728682 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -23,11 +23,12 @@ match p with
 [ list_empty     ⇒ 𝐞
 | list_lcons l q ⇒
    match l with
-   [ label_d k ⇒ structure q
-   | label_m   ⇒ structure q
-   | label_L   ⇒ (structure q)◖𝗟
-   | label_A   ⇒ (structure q)◖𝗔
-   | label_S   ⇒ (structure q)◖𝗦
+   [ label_d k    ⇒ structure q
+   | label_d2 k d ⇒ structure q
+   | label_m      ⇒ structure q
+   | label_L      ⇒ (structure q)◖𝗟
+   | label_A      ⇒ (structure q)◖𝗔
+   | label_S      ⇒ (structure q)◖𝗦
    ]
 ].
 
@@ -45,6 +46,10 @@ lemma structure_d_dx (p) (k):
       ⊗p = ⊗(p◖𝗱k).
 // qed.
 
+lemma structure_d2_dx (p) (k) (d):
+      ⊗p = ⊗(p◖𝗱❨k,d❩).
+// qed.
+
 lemma structure_m_dx (p):
       ⊗p = ⊗(p◖𝗺).
 // qed.
@@ -65,20 +70,27 @@ lemma structure_S_dx (p):
 
 theorem structure_idem (p):
         ⊗p = ⊗⊗p.
-#p elim p -p [| * [ #k ] #p #IH ] //
+#p elim p -p //
+* [ #k | #k #d ] #p #IH //
 qed.
 
 theorem structure_append (p) (q):
         ⊗p●⊗q = ⊗(p●q).
-#p #q elim q -q [| * [ #k ] #q #IH ]
-[||*: <list_append_lcons_sn ] //
+#p #q elim q -q //
+* [ #k | #k #d ] #q #IH //
+<list_append_lcons_sn //
 qed.
 
 (* Constructions with path_lcons ********************************************)
 
 lemma structure_d_sn (p) (k):
       ⊗p = ⊗(𝗱k◗p).
-#p #n <structure_append //
+#p #k <structure_append //
+qed.
+
+lemma structure_d2_sn (p) (k) (d):
+      ⊗p = ⊗(𝗱❨k,d❩◗p).
+#p #k #d <structure_append //
 qed.
 
 lemma structure_m_sn (p):
@@ -105,9 +117,23 @@ qed.
 
 lemma eq_inv_d_dx_structure (h) (q) (p):
       q◖𝗱h = ⊗p → ⊥.
-#h #q #p elim p -p [| * [ #k ] #p #IH ]
+#h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0 /2 width=1 by/
+| <structure_d2_dx #H0 /2 width=1 by/
+| <structure_m_dx #H0 /2 width=1 by/
+| <structure_L_dx #H0 destruct
+| <structure_A_dx #H0 destruct
+| <structure_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_d2_dx_structure (d) (h) (q) (p):
+      q◖𝗱❨h,d❩ = ⊗p → ⊥.
+#d #h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+[ <structure_empty #H0 destruct
+| <structure_d_dx #H0 /2 width=1 by/
+| <structure_d2_dx #H0 /2 width=1 by/
 | <structure_m_dx #H0 /2 width=1 by/
 | <structure_L_dx #H0 destruct
 | <structure_A_dx #H0 destruct
@@ -117,9 +143,10 @@ qed-.
 
 lemma eq_inv_m_dx_structure (q) (p):
       q◖𝗺 = ⊗p → ⊥.
-#q #p elim p -p [| * [ #k ] #p #IH ]
+#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0 /2 width=1 by/
+| <structure_d2_dx #H0 /2 width=1 by/
 | <structure_m_dx #H0 /2 width=1 by/
 | <structure_L_dx #H0 destruct
 | <structure_A_dx #H0 destruct
@@ -130,11 +157,14 @@ qed-.
 lemma eq_inv_L_dx_structure (q) (p):
       q◖𝗟 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗟◗r2 = p.
-#q #p elim p -p [| * [ #k ] #p #IH ]
+#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
+| <structure_d2_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
@@ -148,11 +178,14 @@ qed-.
 lemma eq_inv_A_dx_structure (q) (p):
       q◖𝗔 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗔◗r2 = p.
-#q #p elim p -p [| * [ #k ] #p #IH ]
+#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
+| <structure_d2_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
@@ -166,11 +199,14 @@ qed-.
 lemma eq_inv_S_dx_structure (q) (p):
       q◖𝗦 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗦◗r2 = p.
-#q #p elim p -p [| * [ #k ] #p #IH ]
+#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
+| <structure_d2_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
@@ -186,10 +222,11 @@ qed-.
 theorem eq_inv_append_structure (p) (q) (r):
         p●q = ⊗r →
         ∃∃r1,r2.p = ⊗r1 & q = ⊗r2 & r1●r2 = r.
-#p #q elim q -q [| * [ #k ] #q #IH ] #r
+#p #q elim q -q [| * [ #k | #k #d ] #q #IH ] #r
 [ <list_append_empty_sn #H0 destruct
   /2 width=5 by ex3_2_intro/
 | #H0 elim (eq_inv_d_dx_structure … H0)
+| #H0 elim (eq_inv_d2_dx_structure … H0)
 | #H0 elim (eq_inv_m_dx_structure … H0)
 | #H0 elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
@@ -216,6 +253,14 @@ elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 elim (eq_inv_d_dx_structure … H0)
 qed-.
 
+lemma eq_inv_d2_sn_structure (d) (h) (q) (p):
+      (𝗱❨h,d❩◗q) = ⊗p → ⊥.
+#d #h #q #p >list_cons_comm #H0
+elim (eq_inv_append_structure … H0) -H0 #r1 #r2
+<list_cons_comm #H0 #H1 #H2 destruct
+elim (eq_inv_d2_dx_structure … H0)
+qed-.
+
 lemma eq_inv_m_sn_structure (q) (p):
       (𝗺 ◗q) = ⊗p → ⊥.
 #q #p >list_cons_comm #H0
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 99ed6a323..4de1097bb 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
@@ -23,8 +23,9 @@ lemma structure_pic (p):
       ⊗p ϵ 𝐈.
 #p elim p -p
 [ <structure_empty //
-| * [ #k ] #p #IH
+| * [ #k | #k #d ] #p #IH
   [ <structure_d_dx //
+  | <structure_d2_dx //
   | <structure_m_dx //
   | <structure_L_dx //
   | <structure_A_dx //
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 5bb66e16a..8bffdb64a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
@@ -16,6 +16,7 @@ include "delayed_updating/syntax/prototerm.ma".
 include "delayed_updating/notation/functions/m_hook_1.ma".
 include "delayed_updating/notation/functions/hash_1.ma".
 include "delayed_updating/notation/functions/tau_2.ma".
+include "delayed_updating/notation/functions/tau_3.ma".
 include "delayed_updating/notation/functions/lamda_1.ma".
 include "delayed_updating/notation/functions/at_2.ma".
 
@@ -47,6 +48,10 @@ interpretation
   "inner variable reference by depth (prototerm)"
   'Tau k t = (prototerm_node_1_2 (label_d k) label_m t).
 
+interpretation
+  "inner variable reference by depth with offset (prototerm)"
+  'Tau k d t = (prototerm_node_1_2 (label_d2 k d) label_m t).
+
 interpretation
   "name-free functional abstraction (prototerm)"
   'Lamda t = (prototerm_node_1 label_L t).
@@ -61,6 +66,10 @@ lemma in_comp_iref (t) (q) (k):
       q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t.
 /2 width=3 by ex2_intro/ qed.
 
+lemma in_comp_iref2 (t) (q) (k) (d):
+      q ϵ t → 𝗱❨k,d❩◗𝗺◗q ϵ 𝛕❨k,d❩.t.
+/2 width=3 by ex2_intro/ qed.
+
 (* Basic inversions *********************************************************)
 
 lemma in_comp_inv_iref (t) (p) (k):
@@ -70,6 +79,13 @@ lemma in_comp_inv_iref (t) (p) (k):
 /2 width=3 by ex2_intro/
 qed-.
 
+lemma in_comp_inv_iref2 (t) (p) (k) (d):
+      p ϵ 𝛕❨k,d❩.t →
+      ∃∃q. 𝗱❨k,d❩◗𝗺◗q = p & q ϵ t.
+#t #p #k #d * #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_proper_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
index f7f921bcf..c5a27617a 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
@@ -23,3 +23,8 @@ lemma ppc_iref (t) (k):
       (𝛕k.t) ϵ 𝐏.
 #t #k #p * #q #Hq #H0 destruct //
 qed.
+
+lemma ppc_iref2 (t) (k) (d):
+      (𝛕❨k,d❩.t) ϵ 𝐏.
+#t #k #d #p * #q #Hq #H0 destruct //
+qed.
-- 
2.39.2