From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 20 Dec 2022 00:10:07 +0000 (+0100)
Subject: update in delayed_updating
X-Git-Tag: make_still_working~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ea71486fd1aab2eae2bab42729a66ae775c7f248;p=helm.git

update in delayed_updating

+ excess added to closure condition for path
+ height for path restored
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc
deleted file mode 100644
index 72b6dead7..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc
+++ /dev/null
@@ -1,34 +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 "delayed_updating/syntax/path_closed.ma".
-include "delayed_updating/syntax/path_height.ma".
-include "delayed_updating/syntax/path_depth.ma".
-
-(* CLOSED CONDITION FOR PATH ************************************************)
-
-(* Destructions with height and depth ***************************************)
-
-lemma path_closed_des_depth (o) (q) (n):
-      q ϵ 𝐂❨o,n❩ → ♯q + n = ♭q.
-#o #q #n #Hq elim Hq -q -n //
-#q #n #_ #IH <nplus_succ_dx //
-qed-.
-
-lemma path_closed_des_succ_depth (o) (q) (n):
-      q ϵ 𝐂❨o,↑n❩ → ♭q = ↑↓♭q.
-#o #q #n #Hq
-<(path_closed_des_depth … Hq) -Hq
-<nplus_succ_dx <npred_succ //
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_height.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_height.etc
deleted file mode 100644
index 934df56d0..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_height.etc
+++ /dev/null
@@ -1,97 +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 "ground/arith/nat_plus.ma".
-include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/functions/sharp_1.ma".
-
-(* HEIGHT FOR PATH **********************************************************)
-
-rec definition height (p) on p: nat ≝
-match p with
-[ list_empty     ⇒ 𝟎
-| list_lcons l q ⇒
-  match l with
-  [ label_d k ⇒ height q + k
-  | label_m   ⇒ height q
-  | label_L   ⇒ height q
-  | label_A   ⇒ height q
-  | label_S   ⇒ height q
-  ]
-].
-
-interpretation
-  "height (path)"
-  'Sharp p = (height p).
-
-(* Basic constructions ******************************************************)
-
-lemma height_empty: 𝟎 = ♯𝐞.
-// qed.
-
-lemma height_d_dx (p) (k:pnat):
-      (♯p)+k = ♯(p◖𝗱k).
-// qed.
-
-lemma height_m_dx (p):
-      (♯p) = ♯(p◖𝗺).
-// qed.
-
-lemma height_L_dx (p):
-      (♯p) = ♯(p◖𝗟).
-// qed.
-
-lemma height_A_dx (p):
-      (♯p) = ♯(p◖𝗔).
-// qed.
-
-lemma height_S_dx (p):
-      (♯p) = ♯(p◖𝗦).
-// qed.
-
-(* Main constructions *******************************************************)
-
-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 path_lcons ********************************************)
-
-lemma height_d_sn (p) (k:pnat):
-      k+♯p = ♯(𝗱k◗p).
-// qed.
-
-lemma height_m_sn (p):
-      ♯p = ♯(𝗺◗p).
-// qed.
-
-lemma height_L_sn (p):
-      ♯p = ♯(𝗟◗p).
-// qed.
-
-lemma height_A_sn (p):
-      ♯p = ♯(𝗔◗p).
-// qed.
-
-lemma height_S_sn (p):
-      ♯p = ♯(𝗦◗p).
-// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/sharp_1.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/sharp_1.etc
deleted file mode 100644
index 678f73976..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/sharp_1.etc
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( ♯ break term 90 p )"
-  non associative with precedence 70
-  for @{ 'Sharp $p }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_c_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_c_2.ma
deleted file mode 100644
index 95e3eeb35..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_c_2.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( 𝐂❨ break term 46 b, break term 46 n ❩ )"
-  non associative with precedence 70
-  for @{ 'ClassC $b $n }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_c_3.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_c_3.ma
new file mode 100644
index 000000000..9c2aeadb2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_c_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 o, break term 46 n, break term 46 e ❩ )"
+  non associative with precedence 70
+  for @{ 'ClassC $o $n $e }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/sharp_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/sharp_1.ma
new file mode 100644
index 000000000..678f73976
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/sharp_1.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 90 p )"
+  non associative with precedence 70
+  for @{ 'Sharp $p }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
index 776696b24..841baabb0 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
@@ -26,7 +26,7 @@ include "ground/xoa/ex_6_5.ma".
 definition dbfr (r): relation2 prototerm prototerm ≝
            λt1,t2.
            ∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
-           ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
+           ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m,𝟎❩ & q ϵ 𝐂❨Ⓕ,n,𝟎❩ & r◖𝗱↑n ϵ t1 &
            t1[⋔r←𝛕↑(m+n).(t1⋔(p◖𝗦))] ⇔ t2
 .
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
index f0ffe995b..5225ef537 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
@@ -64,7 +64,7 @@ lemma dbfr_appl_sd (v1) (v2) (t) (r):
 qed.
 
 lemma dbfr_beta_0 (v) (t) (q) (n):
-      q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
+      q ϵ 𝐂❨Ⓕ,n,𝟎❩ → q◖𝗱↑n ϵ t →
       ＠v.𝛌.t ➡𝐝𝐛𝐟[𝗔◗𝗟◗q] ＠v.𝛌.(t[⋔q←𝛕↑n.v]).
 #v #t #q #n #Hn #Ht
 @(ex6_5_intro … (𝐞) (𝐞) q (𝟎) … Hn) -Hn
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
index 700440011..d0f0eb1c4 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
@@ -27,7 +27,7 @@ include "ground/xoa/ex_6_5.ma".
 definition ibfr (r): relation2 prototerm prototerm ≝
            λt1,t2.
            ∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
-           ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
+           ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m,𝟎❩ & q ϵ 𝐂❨Ⓕ,n,𝟎❩ & r◖𝗱↑n ϵ t1 &
            t1[⋔r←🠡[𝐮❨↑(m+n)❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
index 112a98c39..ca1375558 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
@@ -65,7 +65,7 @@ lemma ibfr_appl_sd (v1) (v2) (t) (r):
 qed.
 
 lemma ibfr_beta_0 (v) (t) (q) (n):
-      q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
+      q ϵ 𝐂❨Ⓕ,n,𝟎❩ → q◖𝗱↑n ϵ t →
       ＠v.𝛌.t ➡𝐢𝐛𝐟[𝗔◗𝗟◗q] ＠v.𝛌.(t[⋔q←🠡[𝐮❨↑n❩]v]).
 #v #t #q #n #Hn #Ht
 @(ex6_5_intro … (𝐞) (𝐞) q (𝟎) … Hn) -Hn
@@ -82,7 +82,7 @@ lemma ibfr_beta_0 (v) (t) (q) (n):
 qed.
 
 lemma ibfr_beta_1 (v) (v1) (t) (q) (n):
-      q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
+      q ϵ 𝐂❨Ⓕ,n,𝟎❩ → q◖𝗱↑n ϵ t →
       ＠v.＠v1.𝛌.𝛌.t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗q] ＠v.＠v1.𝛌.𝛌.(t[⋔q←🠡[𝐮❨↑↑n❩]v]).
 #v #v1 #t #q #n #Hn #Ht
 @(ex6_5_intro … (𝐞) (𝗔◗𝗟◗𝐞) q (𝟏) … Hn) -Hn
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma
index 980185f93..e60c4fd1c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma
@@ -20,21 +20,21 @@ include "ground/relocation/xap.ma".
 
 (* Constructions with pcc ***************************************************)
 
-lemma lift_path_closed (o) (f) (q) (n):
-      q ϵ 𝐂❨o,n❩ → 🠡[f]q ϵ 𝐂❨o,🠢[f]q＠❨n❩❩.
-#o #f #q #n #H0 elim H0 -q -n //
+lemma lift_path_closed (o) (e) (f) (q) (n):
+      q ϵ 𝐂❨o,n,e❩ → 🠡[f]q ϵ 𝐂❨o,🠢[f]q＠❨n❩,f＠❨e❩❩.
+#o #e #f #q #n #H0 elim H0 -q -n //
 #q #n [ #k #Ho ] #_ #IH
 /2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/
 /4 width=1 by pcc_d_dx, tr_xap_pos/
 qed.
 
 lemma lift_path_rmap_closed (o) (f) (p) (q) (n):
-      q ϵ 𝐂❨o,n❩ → 🠡[🠢[f]p]q ϵ 𝐂❨o,🠢[f](p●q)＠❨n❩❩.
+      q ϵ 𝐂❨o,n,𝟎❩ → 🠡[🠢[f]p]q ϵ 𝐂❨o,🠢[f](p●q)＠❨n❩,𝟎❩.
 /2 width=1 by lift_path_closed/
 qed.
 
 lemma lift_path_rmap_closed_L (o) (f) (p) (q) (n):
-      q ϵ 𝐂❨o,n❩ → 🠡[🠢[f](p◖𝗟)]q ϵ 𝐂❨o,🠢[f](p●𝗟◗q)＠§❨n❩❩.
+      q ϵ 𝐂❨o,n,𝟎❩ → 🠡[🠢[f](p◖𝗟)]q ϵ 𝐂❨o,🠢[f](p●𝗟◗q)＠§❨n❩,𝟎❩.
 #o #f #p #q #n #Hq
 lapply (lift_path_closed … (🠢[f](p◖𝗟)) … Hq) #Hq0
 lapply (pcc_L_sn … Hq) -Hq #Hq1
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
index 9e8a3a99e..ae7691988 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
@@ -22,35 +22,35 @@ include "ground/lib/stream_eq_eq.ma".
 (* Destructions with cpp ****************************************************)
 
 lemma tls_plus_lift_rmap_closed (o) (f) (q) (n):
-      q ϵ 𝐂❨o,n❩ →
+      q ϵ 𝐂❨o,n,𝟎❩ →
       ∀m. ⇂*[m]f ≗ ⇂*[m+n]🠢[f]q.
 #o #f #q #n #Hq elim Hq -q -n //
 qed-.
 
 lemma tls_lift_rmap_closed (o) (f) (q) (n):
-      q ϵ 𝐂❨o,n❩ →
+      q ϵ 𝐂❨o,n,𝟎❩ →
       f ≗ ⇂*[n]🠢[f]q.
 #o #f #q #n #H0
 /2 width=2 by tls_plus_lift_rmap_closed/
 qed-.
 
 lemma tls_lift_rmap_append_closed_dx (o) (f) (p) (q) (n):
-      q ϵ 𝐂❨o,n❩ →
-      🠢[f]p ≗ ⇂*[n]🠢[f](p●q).
+      q ϵ 𝐂❨o,n,𝟎❩ →
+      (🠢[f]p) ≗ ⇂*[n]🠢[f](p●q).
 #o #f #p #q #n #Hq
 /2 width=2 by tls_lift_rmap_closed/
 qed-.
 
 lemma tls_succ_lift_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
-      q ϵ 𝐂❨o,n❩ →
-      🠢[f]p ≗ ⇂*[↑n]🠢[f](p●𝗟◗q).
+      q ϵ 𝐂❨o,n,𝟎❩ →
+      (🠢[f]p) ≗ ⇂*[↑n]🠢[f](p●𝗟◗q).
 #o #f #p #q #n #Hq
 /3 width=2 by tls_lift_rmap_append_closed_dx, pcc_L_sn/
 qed-.
 
 lemma tls_succ_plus_lift_rmap_append_closed_bLq_dx (o1) (o2) (f) (p) (b) (q) (m) (n):
-      b ϵ 𝐂❨o1,m❩ → q ϵ 𝐂❨o2,n❩ →
-      🠢[f]p ≗ ⇂*[↑(m+n)]🠢[f](p●b●𝗟◗q).
+      b ϵ 𝐂❨o1,m,𝟎❩ → q ϵ 𝐂❨o2,n,𝟎❩ →
+      (🠢[f]p) ≗ ⇂*[↑(m+n)]🠢[f](p●b●𝗟◗q).
 #o1 #o2 #f #p #b #q #m #n #Hm #Hn
 >nplus_succ_dx <stream_tls_plus
 @(stream_eq_trans … (tls_lift_rmap_append_closed_dx … Hm))
@@ -58,8 +58,8 @@ lemma tls_succ_plus_lift_rmap_append_closed_bLq_dx (o1) (o2) (f) (p) (b) (q) (m)
 qed-.
 
 lemma nap_plus_lift_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n):
-      q ϵ 𝐂❨o,n❩ →
-      🠢[f]p＠❨m❩+🠢[f](p●𝗟◗q)＠§❨n❩ = 🠢[f](p●𝗟◗q)＠§❨m+n❩.
+      q ϵ 𝐂❨o,n,𝟎❩ →
+      (🠢[f]p＠❨m❩+🠢[f](p●𝗟◗q)＠§❨n❩) = 🠢[f](p●𝗟◗q)＠§❨m+n❩.
 #o #f #p #q #m #n #Hq
 <tr_nap_plus_dx_xap
 /4 width=2 by eq_f2, tr_xap_eq_repl, tls_succ_lift_rmap_append_closed_Lq_dx/
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma
index fd3b4086a..3597b29d8 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/functions/class_c_2.ma".
+include "delayed_updating/notation/functions/class_c_3.ma".
 include "ground/arith/nat_plus_pred.ma".
 include "ground/lib/subset.ma".
 include "ground/lib/bool_and.ma".
@@ -22,45 +22,55 @@ include "ground/xoa/ex_3_2.ma".
 
 (* CLOSED CONDITION FOR PATH ************************************************)
 
-inductive pcc (o): relation2 nat path ≝
+inductive pcc (o) (e): relation2 nat path ≝
 | pcc_empty:
-  pcc o (𝟎) (𝐞)
+  pcc o e e (𝐞)
 | pcc_d_dx (p) (n) (k):
   (Ⓣ = o → n = ↑↓n) →
-  pcc o (n+ninj k) p → pcc o n (p◖𝗱k)
+  pcc o e (n+ninj k) p → pcc o e n (p◖𝗱k)
 | pcc_m_dx (p) (n):
-  pcc o n p → pcc o n (p◖𝗺)
+  pcc o e n p → pcc o e n (p◖𝗺)
 | pcc_L_dx (p) (n):
-  pcc o n p → pcc o (↑n) (p◖𝗟)
+  pcc o e n p → pcc o e (↑n) (p◖𝗟)
 | pcc_A_dx (p) (n):
-  pcc o n p → pcc o n (p◖𝗔)
+  pcc o e n p → pcc o e n (p◖𝗔)
 | pcc_S_dx (p) (n):
-  pcc o n p → pcc o n (p◖𝗦)
+  pcc o e n p → pcc o e n (p◖𝗦)
 .
 
 interpretation
   "closed condition (path)"
-  'ClassC o n = (pcc o n).
+  'ClassC o n e = (pcc o e n).
 
 (* Advanced constructions ***************************************************)
 
-lemma pcc_false_d_dx (p) (n) (k:pnat):
-      p ϵ 𝐂❨Ⓕ,n+k❩ → p◖𝗱k ϵ 𝐂❨Ⓕ,n❩.
-#p #n #k #H0
+lemma pcc_false_d_dx (e) (p) (n) (k:pnat):
+      p ϵ 𝐂❨Ⓕ,n+k,e❩ → p◖𝗱k ϵ 𝐂❨Ⓕ,n,e❩.
+#e #p #n #k #H0
 @pcc_d_dx [| // ]
 #H0 destruct
 qed.
 
-lemma pcc_true_d_dx (p) (n:pnat) (k:pnat):
-      p ϵ 𝐂❨Ⓣ,n+k❩ → p◖𝗱k ϵ 𝐂❨Ⓣ,n❩.
+lemma pcc_true_d_dx (e) (p) (n:pnat) (k:pnat):
+      p ϵ 𝐂❨Ⓣ,n+k,e❩ → p◖𝗱k ϵ 𝐂❨Ⓣ,n,e❩.
 /2 width=1 by pcc_d_dx/
 qed.
 
+lemma pcc_plus_bi_dx (o) (e) (p) (n):
+      p ϵ 𝐂❨o,n,e❩ →
+      ∀m. p ϵ 𝐂❨o,n+m,e+m❩.
+#o #e #p #n #H0 elim H0 -p -n //
+#p #n [ #k #Ho ] #_ #IH #m
+[|*: /2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/ ]
+@pcc_d_dx // -IH #H0
+>Ho -Ho // <nplus_succ_sn //
+qed.
+
 (* Basic inversions ********************************************************)
 
-lemma pcc_inv_empty (o) (n):
-      (𝐞) ϵ 𝐂❨o,n❩ → 𝟎 = n.
-#o #n @(insert_eq_1 … (𝐞))
+lemma pcc_inv_empty (o) (e) (n):
+      (𝐞) ϵ 𝐂❨o,n,e❩ → e = n.
+#o #e #n @(insert_eq_1 … (𝐞))
 #x * -n //
 #p #n [ #k #_ ] #_ #H0 destruct
 qed-.
@@ -70,108 +80,108 @@ alias symbol "DownArrow" (instance 4) = "predecessor (non-negative integers)".
 alias symbol "UpArrow" (instance 3) = "successor (non-negative integers)".
 alias symbol "and" (instance 1) = "logical and".
 
-lemma pcc_inv_d_dx (o) (p) (n) (k):
-      p◖𝗱k ϵ 𝐂❨o, n❩ →
+lemma pcc_inv_d_dx (o) (e) (p) (n) (k):
+      p◖𝗱k ϵ 𝐂❨o,n,e❩ →
       ∧∧ (Ⓣ = o → n = ↑↓n)
-       & p ϵ 𝐂❨o, n+k❩.
-#o #p #n #h @(insert_eq_1 … (p◖𝗱h))
+       & p ϵ 𝐂❨o,n+k,e❩.
+#o #e #p #n #h @(insert_eq_1 … (p◖𝗱h))
 #x * -x -n
 [|*: #x #n [ #k #Ho ] #Hx ] #H0 destruct
 /3 width=1 by conj/
 qed-.
 
-lemma pcc_inv_m_dx (o) (p) (n):
-      p◖𝗺 ϵ 𝐂❨o,n❩ → p ϵ 𝐂❨o,n❩.
-#o #p #n @(insert_eq_1 … (p◖𝗺))
+lemma pcc_inv_m_dx (o) (e) (p) (n):
+      p◖𝗺 ϵ 𝐂❨o,n,e❩ → p ϵ 𝐂❨o,n,e❩.
+#o #e #p #n @(insert_eq_1 … (p◖𝗺))
 #x * -x -n
 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
 qed-.
 
-lemma pcc_inv_L_dx (o) (p) (n):
-      p◖𝗟 ϵ 𝐂❨o,n❩ →
-      ∧∧ p ϵ 𝐂❨o,↓n❩ & n = ↑↓n.
-#o #p #n @(insert_eq_1 … (p◖𝗟))
+lemma pcc_inv_L_dx (o) (e) (p) (n):
+      p◖𝗟 ϵ 𝐂❨o,n,e❩ →
+      ∧∧ p ϵ 𝐂❨o,↓n,e❩ & n = ↑↓n.
+#o #e #p #n @(insert_eq_1 … (p◖𝗟))
 #x * -x -n
 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct
 <npred_succ /2 width=1 by conj/
 qed-.
 
-lemma pcc_inv_A_dx (o) (p) (n):
-      p◖𝗔 ϵ 𝐂❨o,n❩ → p ϵ 𝐂❨o,n❩.
-#o #p #n @(insert_eq_1 … (p◖𝗔))
+lemma pcc_inv_A_dx (o) (e) (p) (n):
+      p◖𝗔 ϵ 𝐂❨o,n,e❩ → p ϵ 𝐂❨o,n,e❩.
+#o #e #p #n @(insert_eq_1 … (p◖𝗔))
 #x * -x -n
 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
 qed-.
 
-lemma pcc_inv_S_dx (o) (p) (n):
-      p◖𝗦 ϵ 𝐂❨o,n❩ → p ϵ 𝐂❨o,n❩.
-#o #p #n @(insert_eq_1 … (p◖𝗦))
+lemma pcc_inv_S_dx (o) (e) (p) (n):
+      p◖𝗦 ϵ 𝐂❨o,n,e❩ → p ϵ 𝐂❨o,n,e❩.
+#o #e #p #n @(insert_eq_1 … (p◖𝗦))
 #x * -x -n
 [|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
 qed-.
 
 (* Advanced destructions ****************************************************)
 
-lemma pcc_des_d_dx (o) (p) (n) (k):
-      p◖𝗱k ϵ 𝐂❨o,n❩ → p ϵ 𝐂❨o,n+k❩.
-#o #p #n #k #H0
+lemma pcc_des_d_dx (o) (e) (p) (n) (k):
+      p◖𝗱k ϵ 𝐂❨o,n,e❩ → p ϵ 𝐂❨o,n+k,e❩.
+#o #e #p #n #k #H0
 elim (pcc_inv_d_dx … H0) -H0 #H1 #H2 //
 qed-.
 
-lemma pcc_des_gen (o) (p) (n):
-      p ϵ 𝐂❨o,n❩ → p ϵ 𝐂❨Ⓕ,n❩.
-#o #p #n #H0 elim H0 -p -n //
+lemma pcc_des_gen (o) (e) (p) (n):
+      p ϵ 𝐂❨o,n,e❩ → p ϵ 𝐂❨Ⓕ,n,e❩.
+#o #e #p #n #H0 elim H0 -p -n //
 #p #n [ #k #Ho ] #_ #IH
 /2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx, pcc_false_d_dx/
 qed-.
 
 (* Advanced inversions ******************************************************)
 
-lemma pcc_inv_empty_succ (o) (n):
-      (𝐞) ϵ 𝐂❨o,↑n❩ → ⊥.
+lemma pcc_inv_empty_succ_zero (o) (n):
+      (𝐞) ϵ 𝐂❨o,↑n,𝟎❩ → ⊥.
 #o #n #H0
 lapply (pcc_inv_empty … H0) -H0 #H0
 /2 width=7 by eq_inv_zero_nsucc/
 qed-.
 
-lemma pcc_true_inv_d_dx_zero (p) (k):
-      p◖𝗱k ϵ 𝐂❨Ⓣ,𝟎❩ → ⊥.
-#p #k #H0
+lemma pcc_true_inv_d_dx_zero_sn (e) (p) (k):
+      p◖𝗱k ϵ 𝐂❨Ⓣ,𝟎, e❩ → ⊥.
+#e #p #k #H0
 elim (pcc_inv_d_dx … H0) -H0 #H0 #_
 elim (eq_inv_zero_nsucc … (H0 ?)) -H0 //
 qed-.
 
-lemma pcc_inv_L_dx_zero (o) (p):
-      p◖𝗟 ϵ 𝐂❨o,𝟎❩ → ⊥.
-#o #p #H0
+lemma pcc_inv_L_dx_zero_sn (o) (e) (p):
+      p◖𝗟 ϵ 𝐂❨o,𝟎,e❩ → ⊥.
+#o #e #p #H0
 elim (pcc_inv_L_dx … H0) -H0 #_ #H0
 /2 width=7 by eq_inv_zero_nsucc/
 qed-.
 
-lemma pcc_inv_L_dx_succ (o) (p) (n):
-      p◖𝗟 ϵ 𝐂❨o,↑n❩ → p ϵ 𝐂❨o,n❩.
-#o #p #n #H0
+lemma pcc_inv_L_dx_succ (o) (e) (p) (n):
+      p◖𝗟 ϵ 𝐂❨o,↑n,e❩ → p ϵ 𝐂❨o,n,e❩.
+#o #e #p #n #H0
 elim (pcc_inv_L_dx … H0) -H0 //
 qed-.
 
 (* Constructions with land **************************************************)
 
-lemma pcc_land_dx (o1) (o2) (p) (n):
-      p ϵ 𝐂❨o1,n❩ → p ϵ 𝐂❨o1∧o2,n❩.
+lemma pcc_land_dx (o1) (o2) (e) (p) (n):
+      p ϵ 𝐂❨o1,n,e❩ → p ϵ 𝐂❨o1∧o2,n,e❩.
 #o1 * /2 width=2 by pcc_des_gen/
 qed.
 
-lemma pcc_land_sn (o1) (o2) (p) (n):
-      p ϵ 𝐂❨o2,n❩ → p ϵ 𝐂❨o1∧o2,n❩.
+lemma pcc_land_sn (o1) (o2) (e) (p) (n):
+      p ϵ 𝐂❨o2,n,e❩ → p ϵ 𝐂❨o1∧o2,n,e❩.
 * /2 width=2 by pcc_des_gen/
 qed.
 
 (* Main constructions with path_append **************************************)
 
-theorem pcc_append_bi (o1) (o2) (p) (q) (m) (n):
-        p ϵ 𝐂❨o1,m❩ → q ϵ 𝐂❨o2,n❩ → p●q ϵ 𝐂❨o1∧o2,m+n❩.
-#o1 #o2 #p #q #m #n #Hm #Hn elim Hn -q -n
-/2 width=1 by pcc_m_dx, pcc_A_dx, pcc_S_dx, pcc_land_dx/
+theorem pcc_append_bi (o1) (o2) (e1) (e2) (p) (q) (m) (n):
+        p ϵ 𝐂❨o1,m,e1❩ → q ϵ 𝐂❨o2,n,e2❩ → p●q ϵ 𝐂❨o1∧o2,m+n,e1+e2❩.
+#o1 #o2 #e1 #e2 #p #q #m #n #Hm #Hn elim Hn -q -n
+/3 width=1 by pcc_land_dx, pcc_m_dx, pcc_A_dx, pcc_S_dx, pcc_plus_bi_dx/
 #q #n [ #k #Ho2 ] #_ #IH
 [ @pcc_d_dx // #H0
   elim (andb_inv_true_sn … H0) -H0 #_ #H0 >Ho2 //
@@ -182,9 +192,9 @@ qed.
 
 (* Inversions with path_append **********************************************)
 
-lemma pcc_false_inv_append_bi (x) (m) (n):
-      x ϵ 𝐂❨Ⓕ,m+n❩ →
-      ∃∃p,q. p ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & p●q = x.
+lemma pcc_false_zero_dx_inv_append_bi (x) (m) (n):
+      x ϵ 𝐂❨Ⓕ,m+n,𝟎❩ →
+      ∃∃p,q. p ϵ 𝐂❨Ⓕ,m,𝟎❩ & q ϵ 𝐂❨Ⓕ,n,𝟎❩ & p●q = x.
 #x #m #n #Hx
 @(insert_eq_1 … (m+n) … Hx) -Hx #y #Hy
 generalize in match n; -n
@@ -212,39 +222,39 @@ qed-.
 
 (* Constructions with path_lcons ********************************************)
 
-lemma pcc_m_sn (o) (q) (n):
-      q ϵ 𝐂❨o,n❩ → (𝗺◗q) ϵ 𝐂❨o,n❩.
-#o #q #n #Hq
-lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗺) … Hq) -Hq
+lemma pcc_m_sn (o) (e) (q) (n):
+      q ϵ 𝐂❨o,n,e❩ → (𝗺◗q) ϵ 𝐂❨o,n,e❩.
+#o #e #q #n #Hq
+lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗺) … Hq) -Hq
 /2 width=3 by pcc_m_dx/
 qed.
 
-lemma pcc_L_sn (o) (q) (n):
-      q ϵ 𝐂❨o,n❩ → (𝗟◗q) ϵ 𝐂❨o,↑n❩.
-#o #q #n #Hq
-lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗟) … Hq) -Hq
+lemma pcc_L_sn (o) (e) (q) (n):
+      q ϵ 𝐂❨o,n,e❩ → (𝗟◗q) ϵ 𝐂❨o,↑n,e❩.
+#o #e #q #n #Hq
+lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗟) … Hq) -Hq
 /2 width=3 by pcc_L_dx/
 qed.
 
-lemma pcc_A_sn (o) (q) (n):
-      q ϵ 𝐂❨o,n❩ → (𝗔◗q) ϵ 𝐂❨o,n❩.
-#o #q #n #Hq
-lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗔) … Hq) -Hq
+lemma pcc_A_sn (o) (e) (q) (n):
+      q ϵ 𝐂❨o,n,e❩ → (𝗔◗q) ϵ 𝐂❨o,n,e❩.
+#o #e #q #n #Hq
+lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗔) … Hq) -Hq
 /2 width=3 by pcc_A_dx/
 qed.
 
-lemma pcc_S_sn (o) (q) (n):
-      q ϵ 𝐂❨o,n❩ → (𝗦◗q) ϵ 𝐂❨o,n❩.
-#o #q #n #Hq
-lapply (pcc_append_bi (Ⓣ) … (𝐞◖𝗦) … Hq) -Hq
+lemma pcc_S_sn (o) (e) (q) (n):
+      q ϵ 𝐂❨o,n,e❩ → (𝗦◗q) ϵ 𝐂❨o,n,e❩.
+#o #e #q #n #Hq
+lapply (pcc_append_bi (Ⓣ) … (𝟎) e … (𝐞◖𝗦) … Hq) -Hq
 /2 width=3 by pcc_S_dx/
 qed.
 
 (* Main inversions **********************************************************)
 
-theorem pcc_mono (o1) (o2) (q) (n1):
-        q ϵ 𝐂❨o1,n1❩ → ∀n2. q ϵ 𝐂❨o2,n2❩ → n1 = n2.
-#o1 #o2 #q1 #n1 #Hn1 elim Hn1 -q1 -n1
+theorem pcc_mono (o1) (o2) (e) (q) (n1):
+        q ϵ 𝐂❨o1,n1,e❩ → ∀n2. q ϵ 𝐂❨o2,n2,e❩ → n1 = n2.
+#o1 #o2 #e #q1 #n1 #Hn1 elim Hn1 -q1 -n1
 [|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] #n2 #Hn2
 [ <(pcc_inv_empty … Hn2) -n2 //
 | lapply (pcc_des_d_dx … Hn2) -Hn2 #Hn2
@@ -261,15 +271,15 @@ theorem pcc_mono (o1) (o2) (q) (n1):
 ]
 qed-.
 
-theorem pcc_inj_L_sn (o1) (o2) (p1) (p2) (q1) (n):
-        q1 ϵ 𝐂❨o1,n❩ → ∀q2. q2 ϵ 𝐂❨o2,n❩ →
+theorem pcc_zero_dx_inj_L_sn (o1) (o2) (p1) (p2) (q1) (n):
+        q1 ϵ 𝐂❨o1,n,𝟎❩ → ∀q2. q2 ϵ 𝐂❨o2,n,𝟎❩ →
         p1●𝗟◗q1 = p2●𝗟◗q2 → q1 = q2.
 #o1 #o2 #p1 #p2 #q1 #n #Hq1 elim Hq1 -q1 -n
 [|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] * //
 [1,3,5,7,9,11: #l2 #q2 ] #Hq2
 <list_append_lcons_sn <list_append_lcons_sn #H0
 elim (eq_inv_list_lcons_bi ????? H0) -H0 #H0 #H1 destruct
-[ elim (pcc_inv_L_dx_zero … Hq2)
+[ elim (pcc_inv_L_dx_zero_sn … Hq2)
 | lapply (pcc_des_d_dx … Hq2) -Hq2 #Hq2
   <(IH … Hq2) //
 | lapply (pcc_inv_m_dx … Hq2) -Hq2 #Hq2
@@ -280,14 +290,14 @@ elim (eq_inv_list_lcons_bi ????? H0) -H0 #H0 #H1 destruct
   <(IH … Hq2) //
 | lapply (pcc_inv_S_dx … Hq2) -Hq2 #Hq2
   <(IH … Hq2) //
-| elim (pcc_inv_empty_succ … Hq2)
+| elim (pcc_inv_empty_succ_zero … Hq2)
 ]
 qed-.
 
-theorem pcc_inv_L_sn (o) (q) (n) (m):
-        (𝗟◗q) ϵ 𝐂❨o,n❩ → q ϵ 𝐂❨o,m❩ →
+theorem pcc_inv_L_sn (o) (e) (q) (n) (m):
+        (𝗟◗q) ϵ 𝐂❨o,n,e❩ → q ϵ 𝐂❨o,m,e❩ →
         ∧∧ ↓n = m & n = ↑↓n.
-#o #q #n #m #H1q #H2q
+#o #e #q #n #m #H1q #H2q
 lapply (pcc_L_sn … H2q) -H2q #H2q
 <(pcc_mono … H2q … H1q) -q -n
 /2 width=1 by conj/
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_height.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_height.ma
new file mode 100644
index 000000000..3b9e3fbec
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_height.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/syntax/path_closed.ma".
+include "delayed_updating/syntax/path_height.ma".
+include "delayed_updating/syntax/path_depth.ma".
+
+(* CLOSED CONDITION FOR PATH ************************************************)
+
+(* Destructions with height and depth ***************************************)
+
+lemma path_closed_des_depth (o) (e) (q) (n):
+      q ϵ 𝐂❨o,n,e❩ → ♯q + n = ♭q + e.
+#o #e #q #n #Hq elim Hq -q -n //
+#q #n #_ #IH
+<nplus_succ_dx <nplus_succ_sn //
+qed-.
+
+lemma path_closed_des_succ_zero_depth (o) (q) (n):
+      q ϵ 𝐂❨o,↑n,𝟎❩ → ♭q = ↑↓♭q.
+#o #q #n #Hq
+>(nplus_zero_dx (♭q))
+<(path_closed_des_depth … Hq) -Hq
+<nplus_succ_dx <npred_succ //
+qed-.
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 44554b79e..ab812e9b2 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
@@ -21,7 +21,7 @@ include "delayed_updating/syntax/path_depth.ma".
 (* Constructions with structure *********************************************)
 
 lemma path_closed_structure_depth (o) (p):
-      ⊗p ϵ 𝐂❨o,♭p❩.
+      ⊗p ϵ 𝐂❨o,♭p,𝟎❩.
 #o #p elim p -p // *
 /2 width=1 by pcc_L_dx, pcc_A_dx, pcc_S_dx/
 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
new file mode 100644
index 000000000..934df56d0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma
@@ -0,0 +1,97 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/arith/nat_plus.ma".
+include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/sharp_1.ma".
+
+(* HEIGHT FOR PATH **********************************************************)
+
+rec definition height (p) on p: nat ≝
+match p with
+[ list_empty     ⇒ 𝟎
+| list_lcons l q ⇒
+  match l with
+  [ label_d k ⇒ height q + k
+  | label_m   ⇒ height q
+  | label_L   ⇒ height q
+  | label_A   ⇒ height q
+  | label_S   ⇒ height q
+  ]
+].
+
+interpretation
+  "height (path)"
+  'Sharp p = (height p).
+
+(* Basic constructions ******************************************************)
+
+lemma height_empty: 𝟎 = ♯𝐞.
+// qed.
+
+lemma height_d_dx (p) (k:pnat):
+      (♯p)+k = ♯(p◖𝗱k).
+// qed.
+
+lemma height_m_dx (p):
+      (♯p) = ♯(p◖𝗺).
+// qed.
+
+lemma height_L_dx (p):
+      (♯p) = ♯(p◖𝗟).
+// qed.
+
+lemma height_A_dx (p):
+      (♯p) = ♯(p◖𝗔).
+// qed.
+
+lemma height_S_dx (p):
+      (♯p) = ♯(p◖𝗦).
+// qed.
+
+(* Main constructions *******************************************************)
+
+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 path_lcons ********************************************)
+
+lemma height_d_sn (p) (k:pnat):
+      k+♯p = ♯(𝗱k◗p).
+// qed.
+
+lemma height_m_sn (p):
+      ♯p = ♯(𝗺◗p).
+// qed.
+
+lemma height_L_sn (p):
+      ♯p = ♯(𝗟◗p).
+// qed.
+
+lemma height_A_sn (p):
+      ♯p = ♯(𝗔◗p).
+// qed.
+
+lemma height_S_sn (p):
+      ♯p = ♯(𝗦◗p).
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
index 55a1c3a28..f38a72ac9 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
@@ -26,10 +26,10 @@ include "ground/lib/stream_eq_eq.ma".
 
 (* Destructions with cpp ****************************************************)
 
-lemma nap_plus_unwind2_rmap_closed (o) (f) (q) (m) (n):
-      q ϵ 𝐂❨o,n❩ →
-      f＠§❨m❩+♭q = ▶[f]q＠§❨m+n❩.
-#o #f #q #m #n #Hq elim Hq -q -n //
+lemma nap_plus_unwind2_rmap_closed (o) (e) (f) (q) (m) (n):
+      q ϵ 𝐂❨o,n,e❩ →
+      f＠§❨m+e❩+♭q = ▶[f]q＠§❨m+n❩.
+#o #e #f #q #m #n #Hq elim Hq -q -n //
 #q #n [ #k #_ ] #_ #IH
 [ <depth_d_dx <unwind2_rmap_d_dx
   <tr_compose_nap <tr_uni_nap //
@@ -39,21 +39,21 @@ lemma nap_plus_unwind2_rmap_closed (o) (f) (q) (m) (n):
 qed-.
 
 lemma nap_unwind2_rmap_closed (o) (f) (q) (n):
-      q ϵ 𝐂❨o,n❩ →
+      q ϵ 𝐂❨o,n,𝟎❩ →
       f＠§❨𝟎❩+♭q = ▶[f]q＠§❨n❩.
 #o #f #q #n #Hn
 /2 width=2 by nap_plus_unwind2_rmap_closed/
 qed-.
 
 lemma nap_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n):
-      q ϵ 𝐂❨o,n❩ →
+      q ϵ 𝐂❨o,n,𝟎❩ →
       (⫯▶[f]p)＠§❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
 #o #f #p #q #m #n #Hn
 /2 width=2 by nap_plus_unwind2_rmap_closed/
 qed-.
 
 lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
-      q ϵ 𝐂❨o,n❩ →
+      q ϵ 𝐂❨o,n,𝟎❩ →
       ♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
 #o #f #p #q #n #Hn
 >(nplus_zero_sn n)
@@ -62,7 +62,7 @@ lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
 qed-.
 
 lemma tls_succ_plus_unwind2_rmap_push_closed (o) (f) (q) (n):
-      q ϵ 𝐂❨o,n❩ →
+      q ϵ 𝐂❨o,n,𝟎❩ →
       ∀m. ⇂*[m]f ≗ ⇂*[↑(m+n)]▶[⫯f]q.
 #o #f #q #n #Hn elim Hn -q -n //
 #q #n #k #_ #_ #IH #m
@@ -71,21 +71,21 @@ lemma tls_succ_plus_unwind2_rmap_push_closed (o) (f) (q) (n):
 qed-.
 
 lemma tls_succ_unwind2_rmap_push_closed (o) (f) (q) (n):
-      q ϵ 𝐂❨o,n❩ →
+      q ϵ 𝐂❨o,n,𝟎❩ →
       f ≗ ⇂*[↑n]▶[⫯f]q.
 #o #f #q #n #Hn
 /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
 qed-.
 
 lemma tls_succ_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
-      q ϵ 𝐂❨o,n❩ →
+      q ϵ 𝐂❨o,n,𝟎❩ →
       ∀m. ⇂*[m]▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●𝗟◗q).
 #o #f #p #q #n #Hn #m
 /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
 qed-.
 
 lemma tls_succ_unwind2_rmap_closed (f) (q) (n):
-      q ϵ 𝐂❨Ⓕ,n❩ →
+      q ϵ 𝐂❨Ⓕ,n,𝟎❩ →
       ⇂f ≗ ⇂*[↑n]▶[f]q.
 #f #q #n #Hn
 @(stream_eq_canc_dx … (stream_tls_eq_repl …))
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
index 32bc5f594..a5127cc45 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
@@ -20,7 +20,7 @@ include "delayed_updating/unwind/unwind2_rmap_closed.ma".
 
 (* Note: crux of the commutation between unwind and balanced focused reduction *)
 lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n):
-      b ϵ 𝐂❨Ⓕ,m❩ → q ϵ 𝐂❨Ⓕ,n❩ →
+      b ϵ 𝐂❨Ⓕ,m,𝟎❩ → q ϵ 𝐂❨Ⓕ,n,𝟎❩ →
       (𝐮❨↑(♭b+♭q)❩ ∘ ▶[f]p ≗ ▶[f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩).
 #f #p #b #q #m #n #Hm #Hn
 <list_append_rcons_sn <list_append_rcons_sn >list_append_assoc
@@ -34,7 +34,7 @@ lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n):
 [ <tr_compose_nap <tr_compose_nap <tr_uni_nap <tr_uni_nap
   >nsucc_unfold >nplus_succ_dx >nplus_succ_dx <nplus_assoc <nplus_assoc
   >tr_nap_plus_dx <unwind2_rmap_append <nap_plus_unwind2_rmap_closed
-  /2 width=2 by pcc_A_sn/
+  /2 width=4 by pcc_A_sn/
 | @(stream_eq_canc_sn … (tr_tl_compose_uni_sn …))
   @(stream_eq_trans ????? (tr_tl_compose_uni_sn …))
   >stream_tls_succ <unwind2_rmap_append