From 345b9054da93e11139d3dfe07f83e444e3022fc1 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 14 Dec 2022 22:15:07 +0100
Subject: [PATCH] update in delayed_updating

+ guard condition removed from reduction
---
 .../class_g_0.ma => etc/guard/class_g_0.etc}  |  0
 .../guard/lift_path_guard.etc}                |  0
 .../guard/path_closed_guard.etc}              |  0
 .../guard/path_guard.etc}                     |  0
 .../guard/path_guard_structure.etc}           |  0
 .../guard/unwind2_rmap_guard.etc}             |  0
 .../lambdadelta/delayed_updating/notes.txt    |  2 -
 .../delayed_updating/reduction/dbfr.ma        |  9 ++--
 .../dbfr_constructors.ma}                     |  2 +-
 .../delayed_updating/reduction/dbfr_ibfr.ma   | 39 +++++++--------
 .../delayed_updating/reduction/dbfr_lift.ma   | 20 ++++----
 .../delayed_updating/reduction/ibfr.ma        |  9 ++--
 .../ibfr_constructors.ma}                     |  0
 .../delayed_updating/reduction/ibfr_eq.ma     |  4 +-
 .../delayed_updating/reduction/ibfr_lift.ma   | 20 ++++----
 .../delayed_updating/reduction/ibfr_unwind.ma | 47 ++++++-------------
 .../substitution/lift_rmap_structure.ma       | 32 +++++++++++++
 .../unwind/unwind2_rmap_closed.ma             | 28 ++++++++++-
 .../unwind/unwind2_rmap_crux.ma               | 19 ++++----
 19 files changed, 130 insertions(+), 101 deletions(-)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/class_g_0.ma => etc/guard/class_g_0.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{substitution/lift_path_guard.ma => etc/guard/lift_path_guard.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{syntax/path_closed_guard.ma => etc/guard/path_closed_guard.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{syntax/path_guard.ma => etc/guard/path_guard.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{syntax/path_guard_structure.ma => etc/guard/path_guard_structure.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind/unwind2_rmap_guard.ma => etc/guard/unwind2_rmap_guard.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{etc/reduction/dbfr_constructors.etc => reduction/dbfr_constructors.ma} (98%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{etc/reduction/ibfr_constructors.etc => reduction/ibfr_constructors.ma} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_structure.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_g_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/class_g_0.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_g_0.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/class_g_0.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/lift_path_guard.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_guard.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/lift_path_guard.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_closed_guard.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_guard.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_closed_guard.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_guard.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_guard.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_guard_structure.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard_structure.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_guard_structure.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/unwind2_rmap_guard.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_guard.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/unwind2_rmap_guard.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
index 79d8698f9..079d44d8d 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
@@ -8,5 +8,3 @@ 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 66d2a248f..776696b24 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
@@ -17,17 +17,16 @@ 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/xoa/ex_7_5.ma".
+include "ground/xoa/ex_6_5.ma".
 
 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
 
 definition dbfr (r): relation2 prototerm prototerm ≝
            λt1,t2.
            ∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
-           p ϵ 𝐆 & ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
+           ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
            t1[⋔r←𝛕↑(m+n).(t1⋔(p◖𝗦))] ⇔ t2
 .
 
@@ -40,6 +39,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 #Hp #Hb #Hm #Hn #Ht1 #Ht #Ht2
-/3 width=14 by subset_eq_trans, ex7_5_intro/
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=13 by subset_eq_trans, ex6_5_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
similarity index 98%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_constructors.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
index 4dd861087..f0ffe995b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_constructors.etc
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
@@ -82,7 +82,7 @@ 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] ＠v.＠v1.𝛌.𝛌.(t[⋔q←𝛕↑↑n.v]).
 #v #v1 #t #q #n #Hn #Ht
 @(ex6_5_intro … (𝐞) (𝗔◗𝗟◗𝐞) q (𝟏) … Hn) -Hn
 [ //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
index 572b25097..387dc8f15 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
@@ -13,32 +13,40 @@
 (**************************************************************************)
 
 include "delayed_updating/reduction/dbfr.ma".
-include "delayed_updating/reduction/ibfr_unwind.ma".
+include "delayed_updating/reduction/ibfr.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_crux.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_push (f) (t1) (t2) (r): t1 ϵ 𝐓 →
-        t1 ➡𝐝𝐛𝐟[r] t2 → ▼[⫯f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[⫯f]t2.
+theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
+        t1 ➡𝐝𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
 #f #t1 #t2 #r #H0t1
-* #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
+* #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
   /2 width=2 by path_closed_structure_depth/
-| -H0t1 -Hp -Hb -Hm -Ht1 -Ht2
+| -H0t1 -Hb -Hm -Ht1 -Ht2
   /2 width=2 by path_closed_structure_depth/
-| lapply (in_comp_unwind2_path_term (⫯f) … Ht1) -H0t1 -Hp -Hb -Hm -Ht2 -Ht1
+| lapply (in_comp_unwind2_path_term f … Ht1) -H0t1 -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 //
-| lapply (unwind2_term_eq_repl_dx (⫯f) … Ht2) -Ht2 #Ht2
+| 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,10 +64,3 @@ theorem dbfr_des_ibfr_push (f) (t1) (t2) (r): t1 ϵ 𝐓 →
   ]
 ]
 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 e1446df2d..1f5c35a85 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
@@ -19,7 +19,6 @@ 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 ***************************************)
@@ -29,19 +28,17 @@ 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 #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
+* #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
   /2 width=1 by lift_path_closed/
-| -Hp -Hb -Hm -Ht1 -Ht2
+| -Hb -Hm -Ht1 -Ht2
   /2 width=1 by lift_path_rmap_closed_L/
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn -Hp
+| 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 -Hp
+| 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 [ // | // ]
@@ -51,6 +48,7 @@ theorem dbfr_lift_bi (f) (t1) (t2) (r):
   @iref_eq_repl
   @(subset_eq_canc_sn … (lift_term_grafted_S …))
   @lift_term_eq_repl_sn
+(* 🠢[f]p ≗ ⇂*[↑(m+n)]🠢[f](((p◖𝗔)●b)●𝗟◗q) *)
 (* Note: crux of the proof begins *)
   >lift_rmap_A_dx
   /2 width=2 by tls_succ_plus_lift_rmap_append_closed_bLq_dx/
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
index 974ceba5c..700440011 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
@@ -17,18 +17,17 @@ 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/xoa/ex_7_5.ma".
+include "ground/xoa/ex_6_5.ma".
 
 (* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
 
 definition ibfr (r): relation2 prototerm prototerm ≝
            λt1,t2.
            ∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
-           p ϵ 𝐆 & ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
+           ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
            t1[⋔r←🠡[𝐮❨↑(m+n)❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
@@ -41,6 +40,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#Hp #Hb #Hm #Hn #Ht1 #Ht #Ht2
-/3 width=14 by subset_eq_trans, ex7_5_intro/
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=13 by subset_eq_trans, ex6_5_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/ibfr_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/ibfr_constructors.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma
index 0d569e6df..973a4570f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma
@@ -23,8 +23,8 @@ include "delayed_updating/substitution/lift_prototerm_eq.ma".
 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
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht #Ht2 destruct
+@(ex6_5_intro … p … Hb Hm Hn) [ // ] -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/
 ]
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 1b6bb9903..e08f3d419 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_lift.ma
@@ -19,7 +19,6 @@ 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".
@@ -32,19 +31,17 @@ 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 #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
+* #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
   /2 width=1 by lift_path_closed/
-| -Hp -Hb -Hm -Ht1 -Ht2
+| -Hb -Hm -Ht1 -Ht2
   /2 width=1 by lift_path_rmap_closed_L/
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hp -Hn
+| 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 -Hp
+| 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 [ // | <lift_path_append // ]
@@ -53,6 +50,7 @@ theorem ibfr_lift_bi (f) (t1) (t2) (r):
   @(subset_eq_trans … (lift_term_after …))
   @(subset_eq_canc_dx … (lift_term_after …))
   @lift_term_eq_repl_sn
+(* 𝐮❨ ↑(🠢[f](p●𝗔◗b)＠❨m❩ + 🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩) ❩ ∘ 🠢[f]p ≗ 🠢[f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩ *)
 (* Note: crux of the proof begins *)
   @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
   @tr_compose_eq_repl
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 952ef252b..34feec243 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
@@ -12,50 +12,39 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/reduction/ibfr_lift.ma".
-include "delayed_updating/reduction/ibfr_eq.ma".
+include "delayed_updating/reduction/ibfr.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_crux.ma".
 
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.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_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):
+lemma ibfr_unwind_bi (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 #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
+* #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
   /2 width=2 by path_closed_structure_depth/
-| -H1t1 -H2r -Hp -Hb -Hm -Ht1 -Ht2
+| -H1t1 -H2r -Hb -Hm -Ht1 -Ht2
   /2 width=2 by path_closed_structure_depth/
-| lapply (in_comp_unwind2_path_term (⫯f) … Ht1) -Ht2 -Ht1 -H1t1 -H2r -Hp -Hb
+| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2r -Hb
   <unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn >list_append_assoc
   <nap_unwind2_rmap_append_closed_Lq_dx //
-| lapply (unwind2_term_eq_repl_dx (⫯f) … Ht2) -Ht2 #Ht2
+| 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 [ // | // ]
@@ -73,11 +62,3 @@ lemma ibfr_unwind_bi_push (f) (t1) (t2) (r):
   ]
 ]
 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_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_structure.ma
new file mode 100644
index 000000000..32b39247a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_structure.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/substitution/lift_rmap.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/relocation/tr_pushs.ma".
+
+(* LIFT FOR RELOCATION MAP **************************************************)
+
+(* Constructions with structure *********************************************)
+
+lemma lift_rmap_structure (f) (q):
+      (⫯*[♭q]f) = 🠢[f]⊗q.
+#f #q elim q -q //
+* [ #k ] #q #IH //
+[ <depth_L_dx <tr_pushs_succ <structure_L_dx <lift_rmap_L_dx //
+| <depth_A_dx <structure_A_dx <lift_rmap_A_dx //
+| <depth_S_dx <structure_S_dx <lift_rmap_S_dx //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
index 7dd546a81..55a1c3a28 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
@@ -12,10 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "delayed_updating/unwind/unwind2_rmap_lift.ma".
 include "delayed_updating/unwind/unwind2_rmap_eq.ma".
+include "delayed_updating/substitution/lift_rmap_structure.ma".
 include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/syntax/path_depth.ma".
 include "ground/relocation/nap.ma".
+include "ground/relocation/tr_pushs_tls.ma".
 include "ground/lib/stream_tls_plus.ma".
 include "ground/lib/stream_eq_eq.ma".
 
@@ -35,6 +38,13 @@ lemma nap_plus_unwind2_rmap_closed (o) (f) (q) (m) (n):
 ]
 qed-.
 
+lemma nap_unwind2_rmap_closed (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ →
+      f＠§❨𝟎❩+♭q = ▶[f]q＠§❨n❩.
+#o #f #q #n #Hn
+/2 width=2 by nap_plus_unwind2_rmap_closed/
+qed-.
+
 lemma nap_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n):
       q ϵ 𝐂❨o,n❩ →
       (⫯▶[f]p)＠§❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
@@ -62,7 +72,7 @@ qed-.
 
 lemma tls_succ_unwind2_rmap_push_closed (o) (f) (q) (n):
       q ϵ 𝐂❨o,n❩ →
-      f ≗ ⇂*[↑n]▶[⫯f](q).
+      f ≗ ⇂*[↑n]▶[⫯f]q.
 #o #f #q #n #Hn
 /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
 qed-.
@@ -73,3 +83,19 @@ lemma tls_succ_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
 #o #f #p #q #n #Hn #m
 /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
 qed-.
+
+lemma tls_succ_unwind2_rmap_closed (f) (q) (n):
+      q ϵ 𝐂❨Ⓕ,n❩ →
+      ⇂f ≗ ⇂*[↑n]▶[f]q.
+#f #q #n #Hn
+@(stream_eq_canc_dx … (stream_tls_eq_repl …))
+[| @(unwind2_rmap_eq_repl … (tr_compose_id_dx …)) | skip ]
+@(stream_eq_trans … (stream_tls_eq_repl …))
+[| @(lift_unwind2_rmap_after … ) | skip ]
+<tr_compose_tls <tr_id_unfold
+@(stream_eq_trans … (tr_compose_eq_repl …))
+[| @(tls_succ_unwind2_rmap_push_closed … Hn) | skip | // | skip ]
+@(stream_eq_trans ????? (tr_compose_id_dx …))
+<tr_pap_succ_nap <(nap_unwind2_rmap_closed … Hn) <nplus_zero_sn
+<lift_rmap_structure <stream_tls_succ <tr_tls_pushs //
+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
index c919221da..32bc5f594 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_rmap_closed.ma".
-include "delayed_updating/unwind/unwind2_rmap_guard.ma".
 
 (* TAILED UNWIND FOR RELOCATION MAP *****************************************)
 
@@ -21,9 +20,9 @@ include "delayed_updating/unwind/unwind2_rmap_guard.ma".
 
 (* 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
+      b ϵ 𝐂❨Ⓕ,m❩ → q ϵ 𝐂❨Ⓕ,n❩ →
+      (𝐮❨↑(♭b+♭q)❩ ∘ ▶[f]p ≗ ▶[f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩).
+#f #p #b #q #m #n #Hm #Hn
 <list_append_rcons_sn <list_append_rcons_sn >list_append_assoc
 >list_append_rcons_sn >(list_append_rcons_sn … b)
 @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
@@ -33,14 +32,12 @@ lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n):
 ] -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 //
+  >nsucc_unfold >nplus_succ_dx >nplus_succ_dx <nplus_assoc <nplus_assoc
+  >tr_nap_plus_dx <unwind2_rmap_append <nap_plus_unwind2_rmap_closed
+  /2 width=2 by pcc_A_sn/
 | @(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/
+  >stream_tls_succ <unwind2_rmap_append
+  /3 width=2 by tls_succ_unwind2_rmap_closed, pcc_A_sn/
 ]
 qed-.
-- 
2.39.2