From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 11 Dec 2022 18:29:08 +0000 (+0100)
Subject: update in delayed_updating
X-Git-Tag: make_still_working~22
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d108bcea8ebae11b03e8d8a155dfd3f2eb445127

update in delayed_updating

+ bug fixed in the "crux of the proof" allows to certify more reductions
+ restricted form of closed path not used anymore
---

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
index 88b0e413f..72b6dead7 100644
--- 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
@@ -18,10 +18,17 @@ include "delayed_updating/syntax/path_depth.ma".
 
 (* CLOSED CONDITION FOR PATH ************************************************)
 
-(* Constructions with height and depth **************************************)
+(* Destructions with height and depth ***************************************)
 
-lemma path_closed_depth (p) (n):
-      p ϵ 𝐂❨n❩ → ♯p + n = ♭p.
-#p #n #Hn elim Hn -Hn //
-#p #n #_ #IH <nplus_succ_dx //
-qed.
+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/unwind2_rmap_closed_height.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/unwind2_rmap_closed_height.etc
new file mode 100644
index 000000000..6703b3c1d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/unwind2_rmap_closed_height.etc
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_closed.ma".
+include "delayed_updating/syntax/path_closed_height.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Destructions with cpp and height *****************************************)
+
+lemma nap_depth_unwind2_rmap_closed (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ →
+      f＠§❨♯q❩+♭q = ▶[f]q＠§❨♭q❩.
+#o #f #q #n #Hq
+<(path_closed_des_depth … Hq) in ⊢ (???%);
+/2 width=2 by nap_plus_unwind2_rmap_closed_depth/
+qed-.
+
+lemma tls_depth_unwind2_rmap_closed (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ →
+      ⇂*[♯q]f ≗ ⇂*[♭q]▶[f]q.
+#o #f #q #n #Hq elim Hq -q -n //
+#q #n #k #_
+>(npsucc_pred k) in ⊢ (%→?); <nplus_succ_dx #Hq #IH
+<height_d_dx <depth_d_dx
+>(path_closed_des_succ_depth … Hq)
+@(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
+>nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold
+<(path_closed_des_succ_depth … Hq) -Hq
+<nplus_comm <stream_tls_plus
+<nplus_comm <stream_tls_plus
+/2 width=1 by stream_tls_eq_repl/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_constructors.etc
new file mode 100644
index 000000000..4dd861087
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_constructors.etc
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reduction/dbfr.ma".
+include "delayed_updating/substitution/fsubst_constructors.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/syntax/prototerm_constructors_eq.ma".
+
+(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma dbfr_abst_hd (t1) (t2) (r):
+      t1 ➡𝐝𝐛𝐟[r] t2 → 𝛌.t1 ➡𝐝𝐛𝐟[𝗟◗r] 𝛌.t2.
+#t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (𝗟◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_abst_hd/
+| @(subset_eq_trans … (abst_eq_repl … Ht2)) -Ht1 -Ht2
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @fsubst_eq_repl // @iref_eq_repl
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) //
+]
+qed.
+
+lemma dbfr_appl_hd (v) (t1) (t2) (r):
+      t1 ➡𝐝𝐛𝐟[r] t2 → ＠v.t1 ➡𝐝𝐛𝐟[𝗔◗r] ＠v.t2.
+#v #t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (𝗔◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_appl_hd/
+| @(subset_eq_trans … (appl_eq_repl … Ht2)) -Ht1 -Ht2 [|*: // ]
+  @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+  @fsubst_eq_repl // @iref_eq_repl
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) //
+]
+qed.
+
+lemma dbfr_appl_sd (v1) (v2) (t) (r):
+      v1 ➡𝐝𝐛𝐟[r] v2 → ＠v1.t ➡𝐝𝐛𝐟[𝗦◗r] ＠v2.t.
+#v1 #v2 #t #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
+@(ex6_5_intro … (𝗦◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Hv2 //
+| -Hv2 /2 width=1 by in_comp_appl_sd/
+| @(subset_eq_trans ????? (appl_eq_repl …)) [3: @Hv2 |2,4: // |5: skip ]
+  @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
+  @fsubst_eq_repl // @iref_eq_repl
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) //
+]
+qed.
+
+lemma dbfr_beta_0 (v) (t) (q) (n):
+      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
+[ //
+| //
+| //
+| /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @fsubst_eq_repl // <nplus_zero_sn @iref_eq_repl
+  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
+  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
+]
+qed.
+(*
+lemma dbfr_beta_1 (v) (v1) (t) (q) (n):
+      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
+[ //
+| /2 width=1 by pbc_empty, pbc_redex/
+| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
+| /5 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @fsubst_eq_repl // <nplus_unit_sn @lift_term_eq_repl_dx
+  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
+  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
+]
+qed.
+*)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_unprotected.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_unprotected.etc
new file mode 100644
index 000000000..753d38c68
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_unprotected.etc
@@ -0,0 +1,85 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reduction/dbfr_constructors.ma".
+include "delayed_updating/reduction/ibfr_constructors.ma".
+include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
+include "delayed_updating/substitution/lift_prototerm_constructors.ma".
+include "ground/arith/pnat_two.ma".
+
+(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
+
+(* Example of unprotected balanced β-reduction ******************************)
+
+definition l3_t: prototerm ≝
+           (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.⧣𝟏).
+
+definition l3_i1: prototerm ≝
+           (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣𝟏).
+
+definition l3_i2: prototerm ≝
+           (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣↑𝟐).
+
+definition l3_d1: prototerm ≝
+           (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.⧣𝟏).
+
+definition l3_d2: prototerm ≝
+           (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.𝛕𝟏.⧣𝟏).
+
+lemma l3_ti1:
+      l3_t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_i1.
+@ibfr_appl_hd
+@ibfr_eq_trans [| @ibfr_beta_0 // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@(subset_eq_canc_sn … (fsubst_empty_rc …))
+@(subset_eq_canc_sn … (lift_term_abst …))
+@abst_eq_repl
+@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
+qed.
+
+lemma l3_i12:
+      l3_i1 ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗𝐞] l3_i2.
+@ibfr_eq_trans [| @ibfr_beta_1 // ]
+@appl_eq_repl [ // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@abst_eq_repl
+@(subset_eq_canc_sn … (fsubst_empty_rc …))
+@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
+qed.
+
+lemma l3_td1:
+      l3_t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_d1.
+@dbfr_appl_hd
+@dbfr_eq_trans [| @dbfr_beta_0 // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@(subset_eq_canc_sn … (fsubst_empty_rc …)) //
+qed.
+
+lemma ld_di2:
+      l3_i2 ⇔ ▼[𝐢]l3_d2.
+@(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
+[ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) // ]
+@(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
+[ @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
+  @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
+]
+@(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
+@(subset_eq_canc_sn … (unwind2_term_iref …))
+@(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
+@(subset_eq_canc_sn … (unwind2_term_iref …))
+@(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/ibfr_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/ibfr_constructors.etc
new file mode 100644
index 000000000..112a98c39
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/ibfr_constructors.etc
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reduction/ibfr.ma".
+include "delayed_updating/substitution/fsubst_constructors.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
+include "delayed_updating/syntax/prototerm_constructors_eq.ma".
+
+(* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma ibfr_abst_hd (t1) (t2) (r):
+      t1 ➡𝐢𝐛𝐟[r] t2 → 𝛌.t1 ➡𝐢𝐛𝐟[𝗟◗r] 𝛌.t2.
+#t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (𝗟◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_abst_hd/
+| @(subset_eq_trans … (abst_eq_repl … Ht2)) -Ht1 -Ht2
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @fsubst_eq_repl // @lift_term_eq_repl_dx
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) //
+]
+qed.
+
+lemma ibfr_appl_hd (v) (t1) (t2) (r):
+      t1 ➡𝐢𝐛𝐟[r] t2 → ＠v.t1 ➡𝐢𝐛𝐟[𝗔◗r] ＠v.t2.
+#v #t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (𝗔◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_appl_hd/
+| @(subset_eq_trans … (appl_eq_repl … Ht2)) -Ht1 -Ht2 [|*: // ]
+  @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+  @fsubst_eq_repl // @lift_term_eq_repl_dx
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) //
+]
+qed.
+
+lemma ibfr_appl_sd (v1) (v2) (t) (r):
+      v1 ➡𝐢𝐛𝐟[r] v2 → ＠v1.t ➡𝐢𝐛𝐟[𝗦◗r] ＠v2.t.
+#v1 #v2 #t #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
+@(ex6_5_intro … (𝗦◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Hv2 //
+| -Hv2 /2 width=1 by in_comp_appl_sd/
+| @(subset_eq_trans ????? (appl_eq_repl …)) [3: @Hv2 |2,4: // |5: skip ]
+  @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
+  @fsubst_eq_repl // @lift_term_eq_repl_dx
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) //
+]
+qed.
+
+lemma ibfr_beta_0 (v) (t) (q) (n):
+      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
+[ //
+| //
+| //
+| /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @fsubst_eq_repl // <nplus_zero_sn @lift_term_eq_repl_dx
+  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
+  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
+]
+qed.
+
+lemma ibfr_beta_1 (v) (v1) (t) (q) (n):
+      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
+[ //
+| /2 width=1 by pbc_empty, pbc_redex/
+| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
+| /5 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @fsubst_eq_repl // <nplus_unit_sn @lift_term_eq_repl_dx
+  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
+  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_1.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_1.etc
new file mode 100644
index 000000000..df946bf8f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_1.etc
@@ -0,0 +1,110 @@
+include "ground/arith/nat_le_plus.ma".
+include "ground/arith/nat_le_pred.ma".
+
+lemma tls_succ_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
+      q ϵ 𝐂❨o,n❩ →
+      ▶[f]p ≗ ⇂*[↑n]▶[f](p●𝗟◗q).
+/2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
+qed-.
+
+lemma xap_le_unwind2_rmap_append_closed_dx (o) (f) (p) (q) (n):
+      q ϵ 𝐂❨o,n❩ → ∀m. m ≤ n →
+      ▶[f]q＠❨m❩ = ▶[f](p●q)＠❨m❩.
+#o #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 nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
+      q ϵ 𝐂❨o,n❩ →
+      ▶[f](𝗟◗q)＠§❨n❩ = ▶[f](p●𝗟◗q)＠§❨n❩.
+#o #f #p #q #n #Hq
+lapply (pcc_L_sn … Hq) -Hq #Hq
+lapply (xap_le_unwind2_rmap_append_closed_dx o f p … Hq (↑n) ?) -Hq //
+<tr_xap_succ_nap <tr_xap_succ_nap #Hq
+/2 width=1 by eq_inv_nsucc_bi/
+qed-.
+
+lemma nap_unwind2_rmap_push_closed_depth (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ →
+      ♭q = ▶[⫯f]q＠§❨n❩.
+#o #f #q #n #Hq elim Hq -q -n
+[|*: #q #n [ #k #_ ] #_ #IH ] //
+<unwind2_rmap_d_dx <tr_compose_nap //
+qed-.
+
+lemma nap_unwind2_rmap_append_closed_Lq_dx_depth (o) (f) (p) (q) (n):
+      q ϵ 𝐂❨o,n❩ →
+      ♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
+#o #f #p #q #n #Hq
+<nap_unwind2_rmap_append_closed_Lq_dx //
+/2 width=2 by nap_unwind2_rmap_push_closed_depth/
+qed-.
+
+lemma xap_unwind2_rmap_append_closed_true_dx_depth (f) (p) (q) (n):
+      q ϵ 𝐂❨Ⓣ,n❩ → ♭q = ▶[f](p●q)＠❨n❩.
+#f #p #q #n #Hq elim Hq -q -n //
+#q #n #k #Ho #_ #IH
+<unwind2_rmap_d_dx <tr_compose_xap
+>Ho // <tr_uni_xap_succ <Ho //
+qed-.
+
+lemma tls_plus_unwind2_rmap_closed_true (f) (q) (n):
+      q ϵ 𝐂❨Ⓣ,n❩ →
+      ∀m. ⇂*[m]f ≗ ⇂*[m+n]▶[f]q.
+#f #q #n #Hq elim Hq -q -n //
+#q #n #k #Ho #_ #IH #m
+>Ho // <nplus_succ_dx
+@(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
+>nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold
+>nplus_succ_dx <Ho //
+qed-.
+
+lemma tls_unwind2_rmap_append_closed_true_dx (f) (p) (q) (n):
+      q ϵ 𝐂❨Ⓣ,n❩ →
+      ▶[f]p ≗ ⇂*[n]▶[f](p●q).
+/2 width=1 by tls_plus_unwind2_rmap_closed_true/
+qed-.
+
+lemma nap_plus_unwind2_rmap_append_closed_Lq_dx_depth (o) (f) (p) (q) (m) (n):
+      q ϵ 𝐂❨o,n❩ →
+      ▶[f]p＠❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
+#o #f #p #q #m #n #Hq
+<tr_nap_plus @eq_f2
+[ <(tr_xap_eq_repl … (tls_succ_unwind2_rmap_append_closed_Lq_dx …)) //
+| /2 width=2 by nap_unwind2_rmap_append_closed_Lq_dx_depth/
+]
+qed-.
+
+lemma nap_plus_unwind2_rmap_append_closed_bLq_dx_depth (o) (f) (p) (b) (q) (m) (n):
+      b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
+      ♭b+♭q = ▶[f](p●b●𝗟◗q)＠§❨m+n❩.
+#o #f #p #b #q #m #n #Hb #Hq
+>(xap_unwind2_rmap_append_closed_true_dx_depth f p … Hb) -Hb
+>(nap_plus_unwind2_rmap_append_closed_Lq_dx_depth … Hq) -Hq //
+qed-.
+
+lemma tls_succ_plus_unwind2_rmap_append_closed_bLq_dx (o) (f) (p) (b) (q) (m) (n):
+      b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
+      ▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●b●𝗟◗q).
+#o #f #p #b #q #m #n #Hb #Hq
+>nplus_succ_dx <stream_tls_plus >list_append_assoc
+@(stream_eq_trans … (tls_unwind2_rmap_append_closed_true_dx … Hb)) -Hb
+/3 width=2 by stream_tls_eq_repl, tls_succ_unwind2_rmap_append_closed_Lq_dx/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc
new file mode 100644
index 000000000..58b1aab8d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc
@@ -0,0 +1,57 @@
+include "delayed_updating/unwind/unwind2_rmap_closed.ma".
+
+lemma pippo (o) (q) (n):
+      (q◖𝗟) ϵ 𝐂❨o,n❩ →
+      (𝗟◗q) ϵ 𝐂❨o,n❩.
+#o #q elim q -q //
+* [ #k ] #q #IH #n #H0
+elim (pcc_inv_L_dx … H0) -H0 #H0 #Hn
+[ elim (pcc_inv_d_dx … H0) -H0 #_ #H0
+  >Hn -Hn /4 width=1 by pcc_d_dx, pcc_L_dx/
+| lapply (pcc_inv_m_dx … H0) -H0 #H0
+  >Hn -Hn /4 width=1 by pcc_m_dx, pcc_L_dx/
+| elim (pcc_inv_L_dx … H0) -H0 #H0 #Hnn
+  >Hn -Hn /4 width=1 by pcc_L_dx/
+| lapply (pcc_inv_A_dx … H0) -H0 #H0
+  >Hn -Hn /4 width=1 by pcc_A_dx, pcc_L_dx/
+| lapply (pcc_inv_S_dx … H0) -H0 #H0
+  >Hn -Hn /4 width=1 by pcc_S_dx, pcc_L_dx/
+]
+qed-.
+
+
+lemma pippo (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ → ♭q < ▶[f]q＠⧣❨↑n❩.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <depth_d_dx <unwind2_rmap_d_dx
+  <tr_compose_pap <tr_uni_pap //
+| <depth_L_dx <unwind2_rmap_L_dx
+  <tr_pap_push
+  /2 width=1 by nlt_succ_bi/
+]
+qed-.
+
+lemma pippo2 (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ → ▶[f]q＠❨n❩ ≤ ♭q.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <unwind2_rmap_d_dx <depth_d_dx
+  @(nle_trans … IH) -IH
+  <tr_compose_xap
+| <unwind2_rmap_L_dx <depth_L_dx
+  <tr_xap_push
+  /2 width=1 by nle_succ_bi/
+]
+qed-.
+
+lemma pippo (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ → n < ▶[f]q＠⧣❨↑♭q❩.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <unwind2_rmap_d_dx <depth_d_dx
+  <tr_compose_pap <tr_uni_pap
+  @(nlt_trans … (n+k)) [ // ]
+  @(nlt_trans … IH) -IH
+| <unwind2_rmap_L_dx <depth_L_dx <tr_pap_push
+  /2 width=1 by nlt_succ_bi/ 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/names.txt b/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
index 715cb268e..a31ae3caa 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
@@ -1,7 +1,9 @@
 METAVARIABLES
 
+  a         : auxiliary path
   b         : balanced path
   d         : depth
+  e         : excess
   f, g      : update function
   h, k      : reference index by depth
   l         : label
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
index 47d6b3600..79d8698f9 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
@@ -1,8 +1,3 @@
-1) (⫯f)@(1) = 1
-2) f@❨d-n❩ = k → n <= d → (f∘𝐮❨n❩)@❨d❩ = k
-3) f@❨d-1❩ = k-1 → 1 < d → 1 < k → (⫯f)@❨d❩ = k
-
-
 lemma pr_pat_after_uni_tls (i2) (i1):
       ∀f2. @❨i1, f2❩ ≘ i2 →
       ∀f. 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
@@ -13,3 +8,5 @@ lemma pr_pat_after_uni_tls (i2) (i1):
 266D;MUSIC FLAT SIGN;So;0;ON;;;;;N;FLAT;;;;
 266E;MUSIC NATURAL SIGN;So;0;ON;;;;;N;NATURAL;;;;
 266F;MUSIC SHARP SIGN;Sm;0;ON;;;;;N;SHARP;;;;
+
+include "ground/xoa/ex_6_5.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
index 7e4e6dbe3..66d2a248f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
@@ -17,17 +17,17 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/syntax/path_balanced.ma".
+include "delayed_updating/syntax/path_guard.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/notation/relations/black_rightarrow_dbf_3.ma".
-include "ground/arith/nat_rplus.ma".
-include "ground/xoa/ex_6_5.ma".
+include "ground/xoa/ex_7_5.ma".
 
 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
 
 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 &
+           p ϵ 𝐆 & ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
            t1[⋔r←𝛕↑(m+n).(t1⋔(p◖𝗦))] ⇔ t2
 .
 
@@ -40,6 +40,6 @@ interpretation
 lemma dbfr_eq_trans (t) (t1) (t2) (r):
       t1 ➡𝐝𝐛𝐟[r] t → t ⇔ t2 → t1 ➡𝐝𝐛𝐟[r] t2.
 #t #t1 #t2 #r
-* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht #Ht2
-/3 width=13 by subset_eq_trans, ex6_5_intro/
+* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=14 by subset_eq_trans, ex7_5_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
deleted file mode 100644
index 4dd861087..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
+++ /dev/null
@@ -1,101 +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/reduction/dbfr.ma".
-include "delayed_updating/substitution/fsubst_constructors.ma".
-include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/syntax/prototerm_constructors_eq.ma".
-
-(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
-
-(* Constructions with constructors for prototerm ****************************)
-
-lemma dbfr_abst_hd (t1) (t2) (r):
-      t1 ➡𝐝𝐛𝐟[r] t2 → 𝛌.t1 ➡𝐝𝐛𝐟[𝗟◗r] 𝛌.t2.
-#t1 #t2 #r *
-#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex6_5_intro … (𝗟◗p) … Hb Hm Hn) -Hb -Hm -Hn
-[ -Ht2 //
-| -Ht2 /2 width=1 by in_comp_abst_hd/
-| @(subset_eq_trans … (abst_eq_repl … Ht2)) -Ht1 -Ht2
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @fsubst_eq_repl // @iref_eq_repl
-  >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) //
-]
-qed.
-
-lemma dbfr_appl_hd (v) (t1) (t2) (r):
-      t1 ➡𝐝𝐛𝐟[r] t2 → ＠v.t1 ➡𝐝𝐛𝐟[𝗔◗r] ＠v.t2.
-#v #t1 #t2 #r *
-#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex6_5_intro … (𝗔◗p) … Hb Hm Hn) -Hb -Hm -Hn
-[ -Ht2 //
-| -Ht2 /2 width=1 by in_comp_appl_hd/
-| @(subset_eq_trans … (appl_eq_repl … Ht2)) -Ht1 -Ht2 [|*: // ]
-  @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
-  @fsubst_eq_repl // @iref_eq_repl
-  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) //
-]
-qed.
-
-lemma dbfr_appl_sd (v1) (v2) (t) (r):
-      v1 ➡𝐝𝐛𝐟[r] v2 → ＠v1.t ➡𝐝𝐛𝐟[𝗦◗r] ＠v2.t.
-#v1 #v2 #t #r *
-#p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
-@(ex6_5_intro … (𝗦◗p) … Hb Hm Hn) -Hb -Hm -Hn
-[ -Hv2 //
-| -Hv2 /2 width=1 by in_comp_appl_sd/
-| @(subset_eq_trans ????? (appl_eq_repl …)) [3: @Hv2 |2,4: // |5: skip ]
-  @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
-  @fsubst_eq_repl // @iref_eq_repl
-  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) //
-]
-qed.
-
-lemma dbfr_beta_0 (v) (t) (q) (n):
-      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
-[ //
-| //
-| //
-| /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
-| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @fsubst_eq_repl // <nplus_zero_sn @iref_eq_repl
-  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
-  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
-]
-qed.
-(*
-lemma dbfr_beta_1 (v) (v1) (t) (q) (n):
-      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
-[ //
-| /2 width=1 by pbc_empty, pbc_redex/
-| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
-| /5 width=1 by in_comp_appl_hd, in_comp_abst_hd/
-| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
-  @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @fsubst_eq_repl // <nplus_unit_sn @lift_term_eq_repl_dx
-  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
-  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
-]
-qed.
-*)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
index 35966d9f7..572b25097 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
@@ -13,40 +13,32 @@
 (**************************************************************************)
 
 include "delayed_updating/reduction/dbfr.ma".
-include "delayed_updating/reduction/ibfr.ma".
+include "delayed_updating/reduction/ibfr_unwind.ma".
 
 include "delayed_updating/unwind/unwind2_prototerm_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_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_closed_structure.ma".
-include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
 
 (* Main destructions with ibfr **********************************************)
 
-theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
-        t1 ➡𝐝𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
+theorem dbfr_des_ibfr_push (f) (t1) (t2) (r): t1 ϵ 𝐓 →
+        t1 ➡𝐝𝐛𝐟[r] t2 → ▼[⫯f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[⫯f]t2.
 #f #t1 #t2 #r #H0t1
-* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex6_5_intro … (⊗p) (⊗b) (⊗q) (♭b) (♭q))
-[ -H0t1 -Hb -Hm -Hn -Ht1 -Ht2 //
-| -H0t1 -Hm -Hn -Ht1 -Ht2 //
-| -H0t1 -Hb -Hn -Ht1 -Ht2
+* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex7_5_intro … (⊗p) (⊗b) (⊗q) (♭b) (♭q))
+[ -H0t1 -Hp -Hb -Hm -Hn -Ht1 -Ht2 //
+| -H0t1 -Hb -Hm -Hn -Ht1 -Ht2 /2 width=1 by path_guard_structure/
+| -H0t1 -Hp -Hm -Hn -Ht1 -Ht2 //
+| -H0t1 -Hp -Hb -Hn -Ht1 -Ht2
   /2 width=2 by path_closed_structure_depth/
-| -H0t1 -Hb -Hm -Ht1 -Ht2
+| -H0t1 -Hp -Hb -Hm -Ht1 -Ht2
   /2 width=2 by path_closed_structure_depth/
-| lapply (in_comp_unwind2_path_term f … Ht1) -H0t1 -Hb -Hm -Ht2 -Ht1
+| lapply (in_comp_unwind2_path_term (⫯f) … Ht1) -H0t1 -Hp -Hb -Hm -Ht2 -Ht1
   <unwind2_path_d_dx <tr_pap_succ_nap >list_append_rcons_dx >list_append_assoc
-  <nap_unwind2_rmap_append_closed_Lq_dx_depth //
-| lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
+  <nap_unwind2_rmap_append_closed_Lq_dx //
+| 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 [ // | // ]
@@ -56,17 +48,18 @@ theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
     @(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_pap …)) <tr_pap_succ_nap
-    @tr_compose_eq_repl
-    [ <nap_plus_unwind2_rmap_append_closed_bLq_dx_depth //
-    | >unwind2_rmap_A_dx
-      /2 width=2 by tls_succ_plus_unwind2_rmap_append_closed_bLq_dx/
-    ]
+    /2 width=1 by unwind2_rmap_uni_crux/
 (* Note: crux of the proof ends *)
   | //
   | /2 width=2 by ex_intro/
   | //
   ]
 ]
+qed-.
+
+theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
+        t1 ➡𝐝𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
+#f #t1 #t2 #r #Ht1 #Ht12
+lapply (dbfr_des_ibfr_push (𝐢) … Ht1 Ht12) -Ht1 -Ht12 #Ht12
+/2 width=1 by ibfr_structure_unwind_bi/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
index 0c6ab932f..e1446df2d 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
@@ -19,6 +19,7 @@ include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_constructors.ma".
 include "delayed_updating/substitution/lift_path_structure.ma".
 include "delayed_updating/substitution/lift_path_closed.ma".
+include "delayed_updating/substitution/lift_path_guard.ma".
 include "delayed_updating/substitution/lift_rmap_closed.ma".
 
 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
@@ -28,17 +29,19 @@ include "delayed_updating/substitution/lift_rmap_closed.ma".
 theorem dbfr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐝𝐛𝐟[r] t2 → 🠡[f]t1 ➡𝐝𝐛𝐟[🠡[f]r] 🠡[f]t2.
 #f #t1 #t2 #r
-* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex6_5_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔)]b) (🠡[🠢[f](p◖𝗔●b◖𝗟)]q) (🠢[f](p●𝗔◗b)＠❨m❩) (🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩))
-[ -Hb -Hm -Hn -Ht1 -Ht2 //
-| -Hm -Hn -Ht1 -Ht2 //
-| -Hb -Hn -Ht1 -Ht2
+* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex7_5_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔)]b) (🠡[🠢[f](p◖𝗔●b◖𝗟)]q) (🠢[f](p●𝗔◗b)＠❨m❩) (🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩))
+[ -Hp -Hb -Hm -Hn -Ht1 -Ht2 //
+| -Hb -Hm -Hn -Ht1 -Ht2
+  /2 width=1 by lift_path_guard/
+| -Hp -Hm -Hn -Ht1 -Ht2 //
+| -Hp -Hb -Hn -Ht1 -Ht2
   /2 width=1 by lift_path_closed/
-| -Hb -Hm -Ht1 -Ht2
+| -Hp -Hb -Hm -Ht1 -Ht2
   /2 width=1 by lift_path_rmap_closed_L/
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn
+| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn -Hp
   <lift_path_d_dx #Ht1 //
-| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
+| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1 -Hp
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (lift_term_fsubst …))
   @fsubst_eq_repl [ // | // ]
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma
deleted file mode 100644
index 753d38c68..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma
+++ /dev/null
@@ -1,85 +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/reduction/dbfr_constructors.ma".
-include "delayed_updating/reduction/ibfr_constructors.ma".
-include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
-include "delayed_updating/substitution/lift_prototerm_constructors.ma".
-include "ground/arith/pnat_two.ma".
-
-(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
-
-(* Example of unprotected balanced β-reduction ******************************)
-
-definition l3_t: prototerm ≝
-           (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.⧣𝟏).
-
-definition l3_i1: prototerm ≝
-           (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣𝟏).
-
-definition l3_i2: prototerm ≝
-           (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣↑𝟐).
-
-definition l3_d1: prototerm ≝
-           (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.⧣𝟏).
-
-definition l3_d2: prototerm ≝
-           (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.𝛕𝟏.⧣𝟏).
-
-lemma l3_ti1:
-      l3_t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_i1.
-@ibfr_appl_hd
-@ibfr_eq_trans [| @ibfr_beta_0 // ]
-@appl_eq_repl [ // ]
-@abst_eq_repl
-@(subset_eq_canc_sn … (fsubst_empty_rc …))
-@(subset_eq_canc_sn … (lift_term_abst …))
-@abst_eq_repl
-@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
-qed.
-
-lemma l3_i12:
-      l3_i1 ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗𝐞] l3_i2.
-@ibfr_eq_trans [| @ibfr_beta_1 // ]
-@appl_eq_repl [ // ]
-@appl_eq_repl [ // ]
-@abst_eq_repl
-@abst_eq_repl
-@(subset_eq_canc_sn … (fsubst_empty_rc …))
-@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
-qed.
-
-lemma l3_td1:
-      l3_t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_d1.
-@dbfr_appl_hd
-@dbfr_eq_trans [| @dbfr_beta_0 // ]
-@appl_eq_repl [ // ]
-@abst_eq_repl
-@(subset_eq_canc_sn … (fsubst_empty_rc …)) //
-qed.
-
-lemma ld_di2:
-      l3_i2 ⇔ ▼[𝐢]l3_d2.
-@(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
-[ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) // ]
-@(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
-[ @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
-  @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
-]
-@(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
-@(subset_eq_canc_sn … (unwind2_term_iref …))
-@(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
-@(subset_eq_canc_sn … (unwind2_term_iref …))
-@(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
index 90b16d3de..974ceba5c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
@@ -17,18 +17,18 @@ include "delayed_updating/substitution/lift_prototerm.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/syntax/path_balanced.ma".
+include "delayed_updating/syntax/path_guard.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/notation/relations/black_rightarrow_ibf_3.ma".
 include "ground/relocation/tr_uni.ma".
-include "ground/arith/nat_rplus.ma".
-include "ground/xoa/ex_6_5.ma".
+include "ground/xoa/ex_7_5.ma".
 
 (* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
 
 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 &
+           p ϵ 𝐆 & ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
            t1[⋔r←🠡[𝐮❨↑(m+n)❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
@@ -41,6 +41,6 @@ interpretation
 lemma ibfr_eq_trans (t) (t1) (t2) (r):
       t1 ➡𝐢𝐛𝐟[r] t → t ⇔ t2 → t1 ➡𝐢𝐛𝐟[r] t2.
 #t #t1 #t2 #r
-* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht #Ht2
-/3 width=13 by subset_eq_trans, ex6_5_intro/
+* #p #b #q #m #n #Hr#Hp #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=14 by subset_eq_trans, ex7_5_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
deleted file mode 100644
index 112a98c39..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
+++ /dev/null
@@ -1,101 +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/reduction/ibfr.ma".
-include "delayed_updating/substitution/fsubst_constructors.ma".
-include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_prototerm_eq.ma".
-include "delayed_updating/syntax/prototerm_constructors_eq.ma".
-
-(* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
-
-(* Constructions with constructors for prototerm ****************************)
-
-lemma ibfr_abst_hd (t1) (t2) (r):
-      t1 ➡𝐢𝐛𝐟[r] t2 → 𝛌.t1 ➡𝐢𝐛𝐟[𝗟◗r] 𝛌.t2.
-#t1 #t2 #r *
-#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex6_5_intro … (𝗟◗p) … Hb Hm Hn) -Hb -Hm -Hn
-[ -Ht2 //
-| -Ht2 /2 width=1 by in_comp_abst_hd/
-| @(subset_eq_trans … (abst_eq_repl … Ht2)) -Ht1 -Ht2
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @fsubst_eq_repl // @lift_term_eq_repl_dx
-  >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) //
-]
-qed.
-
-lemma ibfr_appl_hd (v) (t1) (t2) (r):
-      t1 ➡𝐢𝐛𝐟[r] t2 → ＠v.t1 ➡𝐢𝐛𝐟[𝗔◗r] ＠v.t2.
-#v #t1 #t2 #r *
-#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex6_5_intro … (𝗔◗p) … Hb Hm Hn) -Hb -Hm -Hn
-[ -Ht2 //
-| -Ht2 /2 width=1 by in_comp_appl_hd/
-| @(subset_eq_trans … (appl_eq_repl … Ht2)) -Ht1 -Ht2 [|*: // ]
-  @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
-  @fsubst_eq_repl // @lift_term_eq_repl_dx
-  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) //
-]
-qed.
-
-lemma ibfr_appl_sd (v1) (v2) (t) (r):
-      v1 ➡𝐢𝐛𝐟[r] v2 → ＠v1.t ➡𝐢𝐛𝐟[𝗦◗r] ＠v2.t.
-#v1 #v2 #t #r *
-#p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
-@(ex6_5_intro … (𝗦◗p) … Hb Hm Hn) -Hb -Hm -Hn
-[ -Hv2 //
-| -Hv2 /2 width=1 by in_comp_appl_sd/
-| @(subset_eq_trans ????? (appl_eq_repl …)) [3: @Hv2 |2,4: // |5: skip ]
-  @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
-  @fsubst_eq_repl // @lift_term_eq_repl_dx
-  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) //
-]
-qed.
-
-lemma ibfr_beta_0 (v) (t) (q) (n):
-      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
-[ //
-| //
-| //
-| /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
-| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @fsubst_eq_repl // <nplus_zero_sn @lift_term_eq_repl_dx
-  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
-  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
-]
-qed.
-
-lemma ibfr_beta_1 (v) (v1) (t) (q) (n):
-      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
-[ //
-| /2 width=1 by pbc_empty, pbc_redex/
-| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
-| /5 width=1 by in_comp_appl_hd, in_comp_abst_hd/
-| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
-  @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @fsubst_eq_repl // <nplus_unit_sn @lift_term_eq_repl_dx
-  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
-  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma
new file mode 100644
index 000000000..0d569e6df
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
+
+include "delayed_updating/reduction/ibfr.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma ibfr_eq_canc_sn (t) (t1) (t2) (r):
+      t ⇔ t1 → t ➡𝐢𝐛𝐟[r] t2 → t1 ➡𝐢𝐛𝐟[r] t2.
+#t #t1 #t2 #r #Ht1
+* #p #b #q #m #n #Hr#Hp #Hb #Hm #Hn #Ht #Ht2 destruct
+@(ex7_5_intro … Hp Hb Hm Hn) [ // ] -Hp -Hb -Hm -Hn
+[ /2 width=3 by subset_in_eq_repl_back/
+| /5 width=3 by subset_eq_canc_sn, fsubst_eq_repl, lift_term_eq_repl_dx, grafted_eq_repl/
+]
+qed-.
+
+lemma ibfr_eq_repl (t1) (t2) (u1) (u2) (r):
+      t1 ⇔ u1 → t2 ⇔ u2 → t1 ➡𝐢𝐛𝐟[r] t2 → u1 ➡𝐢𝐛𝐟[r] u2.
+/3 width=3 by ibfr_eq_canc_sn, ibfr_eq_trans/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_lift.ma
index ac690a3bc..1b6bb9903 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_lift.ma
@@ -19,6 +19,7 @@ include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_after.ma".
 include "delayed_updating/substitution/lift_path_structure.ma".
 include "delayed_updating/substitution/lift_path_closed.ma".
+include "delayed_updating/substitution/lift_path_guard.ma".
 include "delayed_updating/substitution/lift_rmap_closed.ma".
 
 include "ground/relocation/tr_uni_compose.ma".
@@ -31,17 +32,19 @@ include "ground/relocation/tr_compose_eq.ma".
 theorem ibfr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐢𝐛𝐟[r] t2 → 🠡[f]t1 ➡𝐢𝐛𝐟[🠡[f]r] 🠡[f]t2.
 #f #t1 #t2 #r
-* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex6_5_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔)]b) (🠡[🠢[f](p◖𝗔●b◖𝗟)]q) (🠢[f](p●𝗔◗b)＠❨m❩) (🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩))
-[ -Hb -Hm -Hn -Ht1 -Ht2 //
-| -Hm -Hn -Ht1 -Ht2 //
-| -Hb -Hn -Ht1 -Ht2
+* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex7_5_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔)]b) (🠡[🠢[f](p◖𝗔●b◖𝗟)]q) (🠢[f](p●𝗔◗b)＠❨m❩) (🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩))
+[ -Hp -Hb -Hm -Hn -Ht1 -Ht2 //
+| -Hb -Hm -Hn -Ht1 -Ht2
+  /2 width=1 by lift_path_guard/
+| -Hp -Hm -Hn -Ht1 -Ht2 //
+| -Hp -Hb -Hn -Ht1 -Ht2
   /2 width=1 by lift_path_closed/
-| -Hb -Hm -Ht1 -Ht2
+| -Hp -Hb -Hm -Ht1 -Ht2
   /2 width=1 by lift_path_rmap_closed_L/
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn
+| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hp -Hn
   <lift_path_d_dx #Ht1 //
-| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
+| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1 -Hp
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (lift_term_fsubst …))
   @fsubst_eq_repl [ // | <lift_path_append // ]
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
index f3d7d16fa..952ef252b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
@@ -12,39 +12,50 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/reduction/ibfr.ma".
+include "delayed_updating/reduction/ibfr_lift.ma".
+include "delayed_updating/reduction/ibfr_eq.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_closed.ma".
-
-include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_prototerm_eq.ma".
+include "delayed_updating/unwind/unwind2_rmap_crux.ma".
 
 include "delayed_updating/syntax/path_closed_structure.ma".
+include "delayed_updating/syntax/path_guard_structure.ma".
 include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
 
 (* Constructions with unwind2 ***********************************************)
 
-lemma ibfr_unwind_bi (f) (t1) (t2) (r):
+lemma ibfr_structure_unwind_bi (f) (t1) (t2) (r):
+      ▼[⫯𝐢]t1 ➡𝐢𝐛𝐟[⊗r] ▼[⫯𝐢]t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
+#f #t1 #t2 #r #Ht12
+lapply (ibfr_lift_bi (f) … Ht12) -Ht12
+<lift_path_structure #Ht12
+@(ibfr_eq_repl … Ht12) -r
+@(subset_eq_canc_dx … (lift_unwind2_term_after …))
+@unwind2_term_eq_repl_sn -t1 -t2 //
+qed-.
+
+lemma ibfr_unwind_bi_push (f) (t1) (t2) (r):
       t1 ϵ 𝐓 → r ϵ 𝐈 →
-      t1 ➡𝐢𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
+      t1 ➡𝐢𝐛𝐟[r] t2 → ▼[⫯f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[⫯f]t2.
 #f #t1 #t2 #r #H1t1 #H2r
-* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex6_5_intro … (⊗p) (⊗b) (⊗q) (♭b) (♭q))
-[ -H1t1 -H2r -Hb -Hm -Hn -Ht1 -Ht2 //
-| -H1t1 -H2r -Hm -Hn -Ht1 -Ht2 //
-| -H1t1 -H2r -Hb -Hn -Ht1 -Ht2
+* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex7_5_intro … (⊗p) (⊗b) (⊗q) (♭b) (♭q))
+[ -H1t1 -H2r -Hp -Hb -Hm -Hn -Ht1 -Ht2 //
+| -H1t1 -H2r -Hb -Hm -Hn -Ht1 -Ht2
+  /2 width=1 by path_guard_structure/
+| -H1t1 -H2r -Hp -Hm -Hn -Ht1 -Ht2 //
+| -H1t1 -H2r -Hp -Hb -Hn -Ht1 -Ht2
   /2 width=2 by path_closed_structure_depth/
-| -H1t1 -H2r -Hb -Hm -Ht1 -Ht2
+| -H1t1 -H2r -Hp -Hb -Hm -Ht1 -Ht2
   /2 width=2 by path_closed_structure_depth/
-| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2r -Hb
+| lapply (in_comp_unwind2_path_term (⫯f) … Ht1) -Ht2 -Ht1 -H1t1 -H2r -Hp -Hb
   <unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn >list_append_assoc
-  <nap_unwind2_rmap_append_closed_Lq_dx_depth //
-| lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
+  <nap_unwind2_rmap_append_closed_Lq_dx //
+| lapply (unwind2_term_eq_repl_dx (⫯f) … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_pic …))
   [ @fsubst_eq_repl [ // | // ]
@@ -54,17 +65,19 @@ lemma ibfr_unwind_bi (f) (t1) (t2) (r):
     @(subset_eq_canc_dx … (unwind2_lift_term_after …))
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
-    <list_append_rcons_sn
-    @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
-    @tr_compose_eq_repl
-    [ <nap_plus_unwind2_rmap_append_closed_bLq_dx_depth //
-    | >unwind2_rmap_A_dx
-      /2 width=2 by tls_succ_plus_unwind2_rmap_append_closed_bLq_dx/
-    ]
+    /2 width=1 by unwind2_rmap_uni_crux/
 (* Note: crux of the proof ends *)
   | //
   | /2 width=2 by ex_intro/
   | //
   ]
 ]
+qed-.
+
+lemma ibfr_unwind_bi (f) (t1) (t2) (r):
+      t1 ϵ 𝐓 → r ϵ 𝐈 →
+      t1 ➡𝐢𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
+#f #t1 #t2 #r #Ht1 #Hr #Ht12
+lapply (ibfr_unwind_bi_push (𝐢) … Ht1 Hr Ht12) -Ht1 -Hr -Ht12 #Ht12
+/2 width=1 by ibfr_structure_unwind_bi/
 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 ec386108e..9e8a3a99e 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
@@ -59,7 +59,8 @@ 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❩.
+      🠢[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/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
index 5604578e5..bf73d3005 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
@@ -24,6 +24,18 @@ lemma grafted_empty_dx (t):
 /2 width=1 by conj/
 qed.
 
+lemma grafted_incl_repl (t1) (t2) (p):
+      t1 ⊆ t2 → t1⋔p ⊆ t2⋔p.
+#t1 #t2 #p #Ht #q #Hq
+/2 width=1 by/
+qed.
+
+lemma grafted_eq_repl (t1) (t2) (p):
+      t1 ⇔ t2 → t1⋔p ⇔ t2⋔p.
+#t1 #t2 #p * #H1t #H2t
+/3 width=1 by conj, grafted_incl_repl/
+qed.
+
 (* Constructions with prototerm_root ****************************************)
 
 lemma prototerm_root_incl_repl:
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 b0d062de6..7dd546a81 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
@@ -15,129 +15,61 @@
 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/relocation/nap.ma".
 include "ground/lib/stream_tls_plus.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 xap_le_unwind2_rmap_append_closed_dx (o) (f) (p) (q) (n):
-      q ϵ 𝐂❨o,n❩ → ∀m. m ≤ n →
-      ▶[f]q＠❨m❩ = ▶[f](p●q)＠❨m❩.
-#o #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 nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
+lemma nap_plus_unwind2_rmap_closed (o) (f) (q) (m) (n):
       q ϵ 𝐂❨o,n❩ →
-      ▶[f](𝗟◗q)＠§❨n❩ = ▶[f](p●𝗟◗q)＠§❨n❩.
-#o #f #p #q #n #Hq
-lapply (pcc_L_sn … Hq) -Hq #Hq
-lapply (xap_le_unwind2_rmap_append_closed_dx o f p … Hq (↑n) ?) -Hq //
-<tr_xap_succ_nap <tr_xap_succ_nap #Hq
-/2 width=1 by eq_inv_nsucc_bi/
+      f＠§❨m❩+♭q = ▶[f]q＠§❨m+n❩.
+#o #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 //
+| <depth_L_dx <unwind2_rmap_L_dx
+  <tr_nap_push <nplus_succ_dx //
+]
 qed-.
 
-lemma nap_unwind2_rmap_push_closed_depth (o) (f) (q) (n):
+lemma nap_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n):
       q ϵ 𝐂❨o,n❩ →
-      ♭q = ▶[⫯f]q＠§❨n❩.
-#o #f #q #n #Hq elim Hq -q -n
-[|*: #q #n [ #k #_ ] #_ #IH ] //
-<unwind2_rmap_d_dx <tr_compose_nap //
+      (⫯▶[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_depth (o) (f) (p) (q) (n):
+lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
       q ϵ 𝐂❨o,n❩ →
       ♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
-#o #f #p #q #n #Hq
-<nap_unwind2_rmap_append_closed_Lq_dx //
-/2 width=2 by nap_unwind2_rmap_push_closed_depth/
-qed-.
-
-lemma xap_unwind2_rmap_append_closed_true_dx_depth (f) (p) (q) (n):
-      q ϵ 𝐂❨Ⓣ,n❩ → ♭q = ▶[f](p●q)＠❨n❩.
-#f #p #q #n #Hq elim Hq -q -n //
-#q #n #k #Ho #_ #IH
-<unwind2_rmap_d_dx <tr_compose_xap
->Ho // <tr_uni_xap_succ <Ho //
+#o #f #p #q #n #Hn
+>(nplus_zero_sn n)
+<(nap_plus_unwind2_rmap_append_closed_Lq_dx … Hn) -Hn
+<nplus_zero_sn //
 qed-.
 
 lemma tls_succ_plus_unwind2_rmap_push_closed (o) (f) (q) (n):
       q ϵ 𝐂❨o,n❩ →
       ∀m. ⇂*[m]f ≗ ⇂*[↑(m+n)]▶[⫯f]q.
-#o #f #q #n #Hq elim Hq -q -n //
+#o #f #q #n #Hn elim Hn -q -n //
 #q #n #k #_ #_ #IH #m
 @(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
 >nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold //
 qed-.
 
-lemma tls_plus_unwind2_rmap_closed_true (f) (q) (n):
-      q ϵ 𝐂❨Ⓣ,n❩ →
-      ∀m. ⇂*[m]f ≗ ⇂*[m+n]▶[f]q.
-#f #q #n #Hq elim Hq -q -n //
-#q #n #k #Ho #_ #IH #m
->Ho // <nplus_succ_dx
-@(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
->nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold
->nplus_succ_dx <Ho //
-qed-.
-
-lemma tls_succ_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
+lemma tls_succ_unwind2_rmap_push_closed (o) (f) (q) (n):
       q ϵ 𝐂❨o,n❩ →
-      ▶[f]p ≗ ⇂*[↑n]▶[f](p●𝗟◗q).
+      f ≗ ⇂*[↑n]▶[⫯f](q).
+#o #f #q #n #Hn
 /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
 qed-.
 
-lemma tls_unwind2_rmap_append_closed_true_dx (f) (p) (q) (n):
-      q ϵ 𝐂❨Ⓣ,n❩ →
-      ▶[f]p ≗ ⇂*[n]▶[f](p●q).
-/2 width=1 by tls_plus_unwind2_rmap_closed_true/
-qed-.
-
-lemma nap_plus_unwind2_rmap_append_closed_Lq_dx_depth (o) (f) (p) (q) (m) (n):
+lemma tls_succ_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
       q ϵ 𝐂❨o,n❩ →
-      ▶[f]p＠❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
-#o #f #p #q #m #n #Hq
-<tr_nap_plus @eq_f2
-[ <(tr_xap_eq_repl … (tls_succ_unwind2_rmap_append_closed_Lq_dx …)) //
-| /2 width=2 by nap_unwind2_rmap_append_closed_Lq_dx_depth/
-]
-qed-.
-
-lemma nap_plus_unwind2_rmap_append_closed_bLq_dx_depth (o) (f) (p) (b) (q) (m) (n):
-      b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
-      ♭b+♭q = ▶[f](p●b●𝗟◗q)＠§❨m+n❩.
-#o #f #p #b #q #m #n #Hb #Hq
->(xap_unwind2_rmap_append_closed_true_dx_depth f p … Hb) -Hb
->(nap_plus_unwind2_rmap_append_closed_Lq_dx_depth … Hq) -Hq //
-qed-.
-
-lemma tls_succ_plus_unwind2_rmap_append_closed_bLq_dx (o) (f) (p) (b) (q) (m) (n):
-      b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
-      ▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●b●𝗟◗q).
-#o #f #p #b #q #m #n #Hb #Hq
->nplus_succ_dx <stream_tls_plus >list_append_assoc
-@(stream_eq_trans … (tls_unwind2_rmap_append_closed_true_dx … Hb)) -Hb
-/3 width=2 by stream_tls_eq_repl, tls_succ_unwind2_rmap_append_closed_Lq_dx/
+      ∀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-.
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
new file mode 100644
index 000000000..c919221da
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_closed.ma".
+include "delayed_updating/unwind/unwind2_rmap_guard.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Crucial constructions with tr_uni ****************************************)
+
+(* Note: crux of the commutation between unwind and balanced focused reduction *)
+lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n):
+      p ϵ 𝐆 → b ϵ 𝐂❨Ⓕ,m❩ → q ϵ 𝐂❨Ⓕ,n❩ →
+      (𝐮❨↑(♭b+♭q)❩ ∘ ▶[⫯f]p ≗ ▶[⫯f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩).
+#f #p #b #q #m #n #Hp #Hm #Hn
+<list_append_rcons_sn <list_append_rcons_sn >list_append_assoc
+>list_append_rcons_sn >(list_append_rcons_sn … b)
+@(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
+@(stream_eq_trans ????? (tr_compose_eq_repl …))
+[| @tls_succ_plus_unwind2_rmap_append_closed_Lq_dx // | skip
+|  <nap_plus_unwind2_rmap_append_closed_Lq_dx // | skip
+] -Hn
+@tr_eq_inv_nap_zero_tl_bi
+[ <tr_compose_nap <tr_compose_nap <tr_uni_nap <tr_uni_nap
+  <nap_zero_unwind2_rmap_push_guard // <nplus_zero_sn
+  >nsucc_unfold >nplus_succ_dx >nplus_succ_dx <nplus_assoc
+  >tr_nap_plus_dx <unwind2_rmap_append
+  <nap_plus_unwind2_rmap_closed [|*: /2 width=2 by pcc_A_sn/ ]
+  <nap_zero_unwind2_rmap_push_guard //
+| @(stream_eq_canc_sn … (tr_tl_compose_uni_sn …))
+  @(stream_eq_trans ????? (tr_tl_compose_uni_sn …))
+  >stream_tls_succ <unwind2_rmap_append <unwind2_rmap_push_guard
+  /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_guard.ma
new file mode 100644
index 000000000..bdf843577
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_guard.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.ma".
+include "delayed_updating/syntax/path_guard.ma".
+include "ground/relocation/nap.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Destructions with pgc ****************************************************)
+
+lemma unwind2_rmap_push_guard (f) (p):
+      p ϵ 𝐆 → ⫯⇂▶[⫯f]p = ▶[⫯f]p.
+#f #p * //
+qed-.
+
+lemma nap_zero_unwind2_rmap_push_guard (f) (p):
+      p ϵ 𝐆 → 𝟎 = ▶[⫯f]p＠§❨𝟎❩.
+#f #p #Hp
+<(unwind2_rmap_push_guard … Hp) -Hp //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
deleted file mode 100644
index df93a6709..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
+++ /dev/null
@@ -1,43 +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/unwind/unwind2_rmap_closed.ma".
-include "delayed_updating/syntax/path_balanced.ma".
-include "delayed_updating/syntax/path_structure.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Example of unprotected balanced path *************************************)
-
-definition l3_b: path ≝ 𝐞◖𝗔◖𝗟◖𝗱𝟏.
-
-lemma l3_b_unfold: 𝐞◖𝗔◖𝗟◖𝗱𝟏 = l3_b.
-// qed.
-
-lemma l3_b_balanced: ⊗l3_b ϵ 𝐁.
-<l3_b_unfold <structure_d_dx
-/2 width=1 by pbc_empty, pbc_redex/
-qed.
-
-lemma l3_b_closed: l3_b ϵ 𝐂❨Ⓕ,𝟎❩.
-/4 width=1 by pcc_A_sn, pcc_empty, pcc_false_d_dx, pcc_L_dx/
-qed.
-
-lemma l3_b_unwind2_rmap_unfold (f):
-      (⫯f)∘𝐮❨𝟏❩ = ▶[f]l3_b.
-// qed.
-
-lemma l3_b_unwind2_rmap_pap_unit (f):
-      ↑(f＠⧣❨𝟏❩) = ▶[f]l3_b＠⧣❨𝟏❩.
-// qed.