From 829e3a8af3229c4e625245f7265dd67939da98c4 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 4 Sep 2022 21:30:07 +0200
Subject: [PATCH] update in delayd_updating

+ introduction of path_closed complete
---
 .../head/unwind2_rmap_head.etc}               |  0
 .../head/unwind2_rmap_labels.etc}             |  0
 .../delayed_updating/reduction/dfr.ma         |  9 +-
 .../delayed_updating/reduction/dfr_ifr.ma     | 28 +++---
 .../delayed_updating/reduction/dfr_lift.ma    | 20 ++--
 .../delayed_updating/reduction/ifr.ma         |  9 +-
 .../delayed_updating/reduction/ifr_lift.ma    | 22 ++---
 .../delayed_updating/reduction/ifr_unwind.ma  | 26 +++---
 .../substitution/lift_constructors.ma         | 17 +++-
 .../substitution/lift_path_closed.ma          | 11 +++
 .../substitution/lift_rmap_closed.ma          |  7 ++
 .../delayed_updating/syntax/path_closed.ma    | 45 ++++++++-
 .../unwind/unwind2_rmap_closed.ma             | 92 +++++++++++++++++++
 .../unwind/unwind2_rmap_eq.ma                 |  6 +-
 14 files changed, 217 insertions(+), 75 deletions(-)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind/unwind2_rmap_head.ma => etc/head/unwind2_rmap_head.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind/unwind2_rmap_labels.ma => etc/head/unwind2_rmap_labels.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_head.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_head.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_labels.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_labels.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index d0dcf4eee..27468022a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -15,18 +15,17 @@
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/syntax/prototerm_constructors.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
-include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/notation/relations/black_rightarrow_df_3.ma".
 include "ground/xoa/ex_4_3.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 
-(**) (* explicit ninj because we cannot declare the expectd type of k *)
 definition dfr (r): relation2 prototerm prototerm ≝
            λt1,t2.
-           ∃∃p,q,k. p●𝗔◗𝗟◗q = r &
-           (𝗟◗q) = ↳[ninj k](𝗟◗q) & r◖𝗱k ϵ t1 &
-           t1[⋔r←𝛕k.(t1⋔(p◖𝗦))] ⇔ t2
+           ∃∃p,q,n. p●𝗔◗𝗟◗q = r &
+           q ϵ 𝐂❨n❩ & r◖𝗱↑n ϵ t1 &
+           t1[⋔r←𝛕↑n.(t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
index 68cea487c..5f37abd5f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -19,13 +19,13 @@ include "delayed_updating/unwind/unwind2_constructors.ma".
 include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
 include "delayed_updating/unwind/unwind2_preterm_eq.ma".
 include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
-include "delayed_updating/unwind/unwind2_rmap_head.ma".
+include "delayed_updating/unwind/unwind2_rmap_closed.ma".
 
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 
 include "delayed_updating/syntax/prototerm_proper_constructors.ma".
-include "delayed_updating/syntax/path_head_structure.ma".
+include "delayed_updating/syntax/path_closed_structure.ma".
 include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
@@ -35,33 +35,29 @@ include "delayed_updating/syntax/path_structure_depth.ma".
 theorem dfr_des_ifr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
         t1 ➡𝐝𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐟[⊗r] ▼[f]t2.
 #f #t1 #t2 #r #H0t1
-* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
-@(ex4_3_intro … (⊗p) (⊗q) (↑♭q))
-[ -H0t1 -H1k -Ht1 -Ht2 //
+* #p #q #n #Hr #Hn #Ht1 #Ht2 destruct
+@(ex4_3_intro … (⊗p) (⊗q) (♭q))
+[ -H0t1 -Hn -Ht1 -Ht2 //
 | -H0t1 -Ht1 -Ht2
-  >structure_L_sn
-  >H1k in ⊢ (??%?); >path_head_structure_depth <H1k -H1k //
+  /2 width=2 by path_closed_structure_depth/
 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1
-  <unwind2_path_d_dx <list_append_rcons_sn
-  lapply (unwind2_rmap_append_pap_closed f … (p◖𝗔) … H1k) -H1k
-  <depth_L_sn #H2k
-  lapply (eq_inv_ninj_bi … H2k) -H2k #H2k <H2k -H2k #Ht1 //
+  <unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn
+  <unwind2_rmap_append_closed_nap //
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_ppc …))
   [ @fsubst_eq_repl [ // | // ]
-    @(subset_eq_trans … (unwind2_term_iref …))
+    @(subset_eq_trans … (unwind2_term_iref…))
     @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
     [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
     @(subset_eq_trans … (lift_unwind2_term_after …))
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
     <list_append_rcons_sn
-    @(stream_eq_trans … (tr_compose_uni_dx …))
+    @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
     @tr_compose_eq_repl
-    [ <unwind2_rmap_append_pap_closed //
-    | >unwind2_rmap_A_dx
-      /2 width=1 by tls_unwind2_rmap_closed/
+    [ <unwind2_rmap_append_closed_nap //
+    | /2 width=1 by tls_succ_unwind2_rmap_append_L_closed_dx/
     ]
 (* Note: crux of the proof ends *)
   | //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
index b60bd708c..830dbd640 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
@@ -17,8 +17,8 @@ include "delayed_updating/reduction/dfr.ma".
 include "delayed_updating/substitution/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_constructors.ma".
-include "delayed_updating/substitution/lift_path_head.ma".
-include "delayed_updating/substitution/lift_rmap_head.ma".
+include "delayed_updating/substitution/lift_path_closed.ma".
+include "delayed_updating/substitution/lift_rmap_closed.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 
@@ -27,25 +27,23 @@ include "delayed_updating/substitution/lift_rmap_head.ma".
 theorem dfr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐝𝐟[r] t2 → ↑[f]t1 ➡𝐝𝐟[↑[f]r] ↑[f]t2.
 #f #t1 #t2 #r
-* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
-@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠⧣❨k❩))
-[ -H1k -Ht1 -Ht2 //
+* #p #q #n #Hr #Hn #Ht1 #Ht2 destruct
+@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠§❨n❩))
+[ -Hn -Ht1 -Ht2 //
 | -Ht1 -Ht2
-  <lift_rmap_L_dx >lift_path_L_sn
-  <(lift_path_head_closed … H1k) in ⊢ (??%?); -H1k //
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1k
+  /2 width=1 by lift_path_rmap_closed_L/
+| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn
   <lift_path_d_dx #Ht1 //
 | lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (lift_term_fsubst …))
   @fsubst_eq_repl [ // | // ]
-  @(subset_eq_trans … (lift_term_iref …))
+  @(subset_eq_trans … (lift_term_iref_nap …))
   @iref_eq_repl
   @(subset_eq_canc_sn … (lift_term_grafted_S …))
   @lift_term_eq_repl_sn
 (* Note: crux of the proof begins *)
-  >list_append_rcons_sn in H1k; #H1k >lift_rmap_A_dx
-  /2 width=1 by tls_lift_rmap_closed/
+  /2 width=1 by tls_succ_lift_rmap_append_L_closed_dx/
 (* Note: crux of the proof ends *)
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index b36038141..92512b342 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -15,19 +15,18 @@
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/substitution/lift_prototerm.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
-include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/notation/relations/black_rightarrow_if_3.ma".
 include "ground/relocation/tr_uni.ma".
 include "ground/xoa/ex_4_3.ma".
 
 (* IMMEDIATE FOCUSED REDUCTION ************************************************)
 
-(**) (* explicit ninj because we cannot declare the expectd type of k *)
 definition ifr (r): relation2 prototerm prototerm ≝
            λt1,t2.
-           ∃∃p,q,k. p●𝗔◗𝗟◗q = r &
-           (𝗟◗q) = ↳[ninj k](𝗟◗q) & r◖𝗱k ϵ t1 &
-           t1[⋔r←↑[𝐮❨ninj k❩](t1⋔(p◖𝗦))] ⇔ t2
+           ∃∃p,q,n. p●𝗔◗𝗟◗q = r &
+           q ϵ 𝐂❨n❩ & r◖𝗱↑n ϵ t1 &
+           t1[⋔r←↑[𝐮❨↑n❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
index 7c4d11d73..1d8f5855a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
@@ -17,8 +17,8 @@ include "delayed_updating/reduction/ifr.ma".
 include "delayed_updating/substitution/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_after.ma".
-include "delayed_updating/substitution/lift_path_head.ma".
-include "delayed_updating/substitution/lift_rmap_head.ma".
+include "delayed_updating/substitution/lift_path_closed.ma".
+include "delayed_updating/substitution/lift_rmap_closed.ma".
 
 include "ground/relocation/tr_uni_compose.ma".
 include "ground/relocation/tr_compose_eq.ma".
@@ -30,13 +30,12 @@ include "ground/relocation/tr_compose_eq.ma".
 theorem ifr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐢𝐟[r] t2 → ↑[f]t1 ➡𝐢𝐟[↑[f]r] ↑[f]t2.
 #f #t1 #t2 #r
-* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
-@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠⧣❨k❩))
-[ -H1k -Ht1 -Ht2 //
+* #p #q #n #Hr #Hn #Ht1 #Ht2 destruct
+@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠§❨n❩))
+[ -Hn -Ht1 -Ht2 //
 | -Ht1 -Ht2
-  <lift_rmap_L_dx >lift_path_L_sn
-  <(lift_path_head_closed … H1k) in ⊢ (??%?); -H1k //
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1k
+  /2 width=1 by lift_path_rmap_closed_L/
+| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn
   <lift_path_d_dx #Ht1 //
 | lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
   @(subset_eq_trans … Ht2) -t2
@@ -48,10 +47,9 @@ theorem ifr_lift_bi (f) (t1) (t2) (r):
   @(subset_eq_canc_dx … (lift_term_after …))
   @lift_term_eq_repl_sn
 (* Note: crux of the proof begins *)
-  @(stream_eq_trans … (tr_compose_uni_dx …))
-  @tr_compose_eq_repl //
-  >list_append_rcons_sn in H1k; #H1k >lift_rmap_A_dx
-  /2 width=1 by tls_lift_rmap_closed/
+  @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
+  @tr_compose_eq_repl // >nsucc_unfold
+  /2 width=1 by tls_succ_lift_rmap_append_L_closed_dx/
 (* Note: crux of the proof ends *)
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
index e8cc51826..077ff798e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
@@ -17,12 +17,12 @@ include "delayed_updating/reduction/ifr.ma".
 include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
 include "delayed_updating/unwind/unwind2_preterm_eq.ma".
 include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
-include "delayed_updating/unwind/unwind2_rmap_head.ma".
+include "delayed_updating/unwind/unwind2_rmap_closed.ma".
 
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 
-include "delayed_updating/syntax/path_head_structure.ma".
+include "delayed_updating/syntax/path_closed_structure.ma".
 include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* IMMEDIATE FOCUSED REDUCTION **********************************************)
@@ -33,17 +33,14 @@ lemma ifr_unwind_bi (f) (t1) (t2) (r):
       t1 ϵ 𝐓 → r ϵ 𝐈 →
       t1 ➡𝐢𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐟[⊗r] ▼[f]t2.
 #f #t1 #t2 #r #H1t1 #H2r
-* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
-@(ex4_3_intro … (⊗p) (⊗q) (↑♭q))
-[ -H1t1 -H2r -H1k -Ht1 -Ht2 //
+* #p #q #n #Hr #Hn #Ht1 #Ht2 destruct
+@(ex4_3_intro … (⊗p) (⊗q) (♭q))
+[ -H1t1 -H2r -Hn -Ht1 -Ht2 //
 | -H1t1 -H2r -Ht1 -Ht2
-  >structure_L_sn
-  >H1k in ⊢ (??%?); >path_head_structure_depth <H1k -H1k //
+  /2 width=2 by path_closed_structure_depth/
 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2r
-  <unwind2_path_d_dx <list_append_rcons_sn
-  lapply (unwind2_rmap_append_pap_closed f … (p◖𝗔) … H1k) -H1k
-  <depth_L_sn #H2k
-  lapply (eq_inv_ninj_bi … H2k) -H2k #H2k <H2k -H2k #Ht1 //
+  <unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn
+  <unwind2_rmap_append_closed_nap //
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_pic …))
@@ -55,11 +52,10 @@ lemma ifr_unwind_bi (f) (t1) (t2) (r):
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
     <list_append_rcons_sn
-    @(stream_eq_trans … (tr_compose_uni_dx …))
+    @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
     @tr_compose_eq_repl
-    [ <unwind2_rmap_append_pap_closed //
-    | >unwind2_rmap_A_dx
-      /2 width=1 by tls_unwind2_rmap_closed/
+    [ <unwind2_rmap_append_closed_nap //
+    | /2 width=1 by tls_succ_unwind2_rmap_append_L_closed_dx/
     ]
 (* Note: crux of the proof ends *)
   | //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
index e87ccb21f..f263e2d14 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
@@ -15,17 +15,18 @@
 include "delayed_updating/substitution/lift_prototerm_id.ma".
 include "delayed_updating/substitution/lift_path_uni.ma".
 include "delayed_updating/syntax/prototerm_constructors_eq.ma".
+include "ground/relocation/nap.ma".
 
 (* LIFT FOR PROTOTERM *******************************************************)
 
-lemma lift_term_iref_sn (f) (t:prototerm) (k:pnat):
+lemma lift_term_iref_pap_sn (f) (t:prototerm) (k:pnat):
       (𝛕f＠⧣❨k❩.↑[⇂*[k]f]t) ⊆ ↑[f](𝛕k.t).
 #f #t #k #p * #q * #r #Hr #H1 #H2 destruct
 @(ex2_intro … (𝗱k◗𝗺◗r))
 /2 width=1 by in_comp_iref/
 qed-.
 
-lemma lift_term_iref_dx (f) (t) (k:pnat):
+lemma lift_term_iref_pap_dx (f) (t) (k:pnat):
       ↑[f](𝛕k.t) ⊆ 𝛕f＠⧣❨k❩.↑[⇂*[k]f]t.
 #f #t #k #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
@@ -33,15 +34,21 @@ elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
 /3 width=1 by in_comp_iref, in_comp_lift_path_term/
 qed-.
 
-lemma lift_term_iref (f) (t) (k:pnat):
+lemma lift_term_iref_pap (f) (t) (k:pnat):
       (𝛕f＠⧣❨k❩.↑[⇂*[k]f]t) ⇔ ↑[f](𝛕k.t).
-/3 width=1 by conj, lift_term_iref_sn, lift_term_iref_dx/
+/3 width=1 by conj, lift_term_iref_pap_sn, lift_term_iref_pap_dx/
+qed.
+
+lemma lift_term_iref_nap (f) (t) (n):
+      (𝛕↑(f＠§❨n❩).↑[⇂*[↑n]f]t) ⇔ ↑[f](𝛕↑n.t).
+#f #t #n
+>tr_pap_succ_nap //
 qed.
 
 lemma lift_term_iref_uni (t) (n) (k):
       (𝛕(k+n).t) ⇔ ↑[𝐮❨n❩](𝛕k.t).
 #t #n #k
-@(subset_eq_trans … (lift_term_iref …))
+@(subset_eq_trans … (lift_term_iref_pap …))
 <tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
 /3 width=1 by iref_eq_repl, lift_term_id/
 qed.
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 b332b841f..79443ca3b 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
@@ -31,3 +31,14 @@ lemma lift_path_rmap_closed (f) (p) (q) (n):
       q ϵ 𝐂❨n❩ → ↑[↑[p]f]q ϵ 𝐂❨↑[p●q]f＠❨n❩❩.
 /2 width=1 by lift_path_closed/
 qed.
+
+lemma lift_path_rmap_closed_L (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ → ↑[↑[p◖𝗟]f]q ϵ 𝐂❨↑[p●𝗟◗q]f＠§❨n❩❩.
+#f #p #q #n #Hq
+lapply (lift_path_closed (↑[p◖𝗟]f) … Hq) #Hq0
+lapply (pcc_L_sn … Hq) -Hq #Hq1
+lapply (lift_path_rmap_closed f p … Hq1) -Hq1
+<lift_path_L_sn >lift_rmap_L_dx #Hq1
+elim (pcc_inv_L_sn … Hq1 Hq0) -Hq1 #H0 #_
+<H0 in Hq0; -H0 //
+qed.
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 58bef8153..cc3e61bf7 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
@@ -34,3 +34,10 @@ lemma tls_lift_rmap_closed (f) (q) (n):
 #f #q #n #H0
 /2 width=1 by tls_plus_lift_rmap_closed/
 qed-.
+
+lemma tls_succ_lift_rmap_append_L_closed_dx (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ↑[p]f ≗ ⇂*[↑n]↑[p●𝗟◗q]f.
+#f #p #q #n #Hq
+/3 width=1 by tls_lift_rmap_closed, pcc_L_sn/
+qed-.
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 fd7a9954f..620db955c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma
@@ -65,7 +65,7 @@ qed-.
 
 lemma pcc_inv_L_dx (p) (n):
       p◖𝗟 ϵ 𝐂❨n❩ →
-      ∧∧ p ϵ 𝐂❨↓n❩ & ↑↓n = n.
+      ∧∧ p ϵ 𝐂❨↓n❩ & n = ↑↓n.
 #p #n @(insert_eq_1 … (p◖𝗟))
 #x * -x -n
 [|*: #x #n [ #k ] #Hx ] #H0 destruct
@@ -99,7 +99,7 @@ lemma pcc_inv_L_dx_zero (p):
       p◖𝗟 ϵ 𝐂❨𝟎❩ → ⊥.
 #p #H0
 elim (pcc_inv_L_dx … H0) -H0 #_ #H0
-/2 width=7 by eq_inv_nsucc_zero/
+/2 width=7 by eq_inv_zero_nsucc/
 qed-.
 
 lemma pcc_inv_L_dx_succ (p) (n):
@@ -117,9 +117,39 @@ theorem pcc_append_bi (p) (q) (m) (n):
 /2 width=1 by pcc_d_dx, pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/
 qed.
 
+(* Constructions with path_lcons ********************************************)
+
+lemma pcc_m_sn (q) (n):
+      q ϵ 𝐂❨n❩ → (𝗺◗q) ϵ 𝐂❨n❩.
+#q #n #Hq
+lapply (pcc_append_bi (𝐞◖𝗺) … Hq) -Hq
+/2 width=3 by pcc_m_dx/
+qed.
+
+lemma pcc_L_sn (q) (n):
+      q ϵ 𝐂❨n❩ → (𝗟◗q) ϵ 𝐂❨↑n❩.
+#q #n #Hq
+lapply (pcc_append_bi (𝐞◖𝗟) … Hq) -Hq
+/2 width=3 by pcc_L_dx/
+qed.
+
+lemma pcc_A_sn (q) (n):
+      q ϵ 𝐂❨n❩ → (𝗔◗q) ϵ 𝐂❨n❩.
+#q #n #Hq
+lapply (pcc_append_bi (𝐞◖𝗔) … Hq) -Hq
+/2 width=3 by pcc_A_dx/
+qed.
+
+lemma pcc_S_sn (q) (n):
+      q ϵ 𝐂❨n❩ → (𝗦◗q) ϵ 𝐂❨n❩.
+#q #n #Hq
+lapply (pcc_append_bi (𝐞◖𝗦) … Hq) -Hq
+/2 width=3 by pcc_S_dx/
+qed.
+
 (* Main inversions **********************************************************)
 
-theorem ppc_mono (q) (n1):
+theorem pcc_mono (q) (n1):
         q ϵ 𝐂❨n1❩ → ∀n2. q ϵ 𝐂❨n2❩ → n1 = n2.
 #q1 #n1 #Hn1 elim Hn1 -q1 -n1
 [|*: #q1 #n1 [ #k1 ] #_ #IH ] #n2 #Hn2
@@ -160,3 +190,12 @@ elim (eq_inv_list_lcons_bi ????? H0) -H0 #H0 #H1 destruct
 | elim (pcc_inv_empty_succ … Hq2)
 ]
 qed-.
+
+theorem pcc_inv_L_sn (q) (n) (m):
+        (𝗟◗q) ϵ 𝐂❨n❩ → q ϵ 𝐂❨m❩ →
+        ∧∧ ↓n = m & n = ↑↓n.
+#q #n #m #H1q #H2q
+lapply (pcc_L_sn … H2q) -H2q #H2q
+<(pcc_mono … H2q … H1q) -q -n
+/2 width=1 by conj/
+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
new file mode 100644
index 000000000..7c551ed85
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
@@ -0,0 +1,92 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind/unwind2_rmap_eq.ma".
+include "delayed_updating/syntax/path_closed.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/relocation/xap.ma".
+include "ground/lib/stream_eq_eq.ma".
+include "ground/arith/nat_le_plus.ma".
+include "ground/arith/nat_le_pred.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Destructions with cpp ****************************************************)
+
+lemma unwind2_rmap_append_closed_dx_xap_le (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ → ∀m. m ≤ n →
+      ▶[f]q＠❨m❩ = ▶[f](p●q)＠❨m❩.
+#f #p #q #n #Hq elim Hq -q -n
+[|*: #q #n [ #k ] #_ #IH ] #m #Hm
+[ <(nle_inv_zero_dx … Hm) -m //
+| <unwind2_rmap_d_dx <unwind2_rmap_d_dx
+  <tr_compose_xap <tr_compose_xap
+  @IH -IH (**) (* auto too slow *)
+  @nle_trans [| @tr_uni_xap ]
+  /2 width=1 by nle_plus_bi_dx/
+| <unwind2_rmap_m_dx <unwind2_rmap_m_dx
+  /2 width=2 by/
+| <unwind2_rmap_L_dx <unwind2_rmap_L_dx
+  elim (nle_inv_succ_dx … Hm) -Hm // * #Hm #H0
+  >H0 -H0 <tr_xap_push <tr_xap_push
+  /3 width=2 by eq_f/
+| <unwind2_rmap_A_dx <unwind2_rmap_A_dx
+  /2 width=2 by/
+| <unwind2_rmap_S_dx <unwind2_rmap_S_dx
+  /2 width=2 by/
+]
+qed-.
+
+lemma unwind2_rmap_append_L_closed_dx_nap (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ▶[f](𝗟◗q)＠§❨n❩ = ▶[f](p●𝗟◗q)＠§❨n❩.
+#f #p #q #n #Hq
+lapply (pcc_L_sn … Hq) -Hq #Hq
+lapply (unwind2_rmap_append_closed_dx_xap_le f p … Hq (↑n) ?) -Hq //
+<tr_xap_succ_nap <tr_xap_succ_nap #Hq
+/2 width=1 by eq_inv_nsucc_bi/
+qed-.
+
+lemma unwind2_rmap_push_closed_nap (f) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ♭q = ▶[⫯f]q＠§❨n❩.
+#f #q #n #Hq elim Hq -q -n
+[|*: #q #n [ #k ] #_ #IH ] //
+<unwind2_rmap_d_dx <tr_compose_nap //
+qed-.
+
+lemma unwind2_rmap_append_closed_nap (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
+#f #p #q #n #Hq
+<unwind2_rmap_append_L_closed_dx_nap //
+/2 width=1 by unwind2_rmap_push_closed_nap/
+qed-.
+
+lemma tls_succ_plus_unwind2_rmap_push_closed (f) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ∀m. ⇂*[m]f ≗ ⇂*[↑(m+n)]▶[⫯f]q.
+#f #q #n #Hq elim Hq -q -n //
+#q #n [ #k ] #_ #IH #m
+[ @(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
+  >nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold //
+| <unwind2_rmap_L_dx <nplus_succ_dx //
+]
+qed-.
+
+lemma tls_succ_unwind2_rmap_append_L_closed_dx (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ▶[f]p ≗ ⇂*[↑n]▶[f](p●𝗟◗q).
+/2 width=1 by tls_succ_plus_unwind2_rmap_push_closed/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
index c075e2f25..b93aabf0f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
@@ -28,9 +28,9 @@ lemma unwind2_rmap_eq_repl (p):
 /3 width=1 by preunwind2_rmap_eq_repl/
 qed-.
 
-lemma tls_unwind2_rmap_d_dx (f) (p) (n) (k):
-      ⇂*[n+k]▶[f]p ≗ ⇂*[n]▶[f](p◖𝗱k).
-#f #p #n #k
+lemma tls_unwind2_rmap_d_dx (f) (p) (h) (k):
+      ⇂*[h+k]▶[f]p ≗ ⇂*[h]▶[f](p◖𝗱k).
+#f #p #h #k
 <unwind2_rmap_d_dx >nrplus_inj_dx
 /2 width=1 by tr_tls_compose_uni_dx/
 qed.
-- 
2.39.2