From b0c6bbd5db69489a5ebd1b36de6685fa6de441b3 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 8 Sep 2022 00:13:21 +0200
Subject: [PATCH] update in ground and delayed_updating

+ example of unprotected balanced segment
+ balanced reduction parked for now
+ additions and renaming
---
 .../dbfr.ma => etc/balanced/dbfr.etc}         | 10 ++---
 .../balanced/dbfr_ibfr.etc}                   | 37 ++++++++--------
 .../balanced/dbfr_lift.etc}                   |  0
 .../ibfr.ma => etc/balanced/ibfr.etc}         | 10 ++---
 .../delayed_updating/reduction/dfr_ifr.ma     |  6 +--
 .../delayed_updating/reduction/ifr_unwind.ma  |  6 +--
 .../unwind/unwind2_rmap_closed.ma             | 18 ++++++--
 .../unwind/unwind2_rmap_unprotected.ma        | 43 +++++++++++++++++++
 .../ground/relocation/tr_uni_compose.ma       |  7 +++
 .../lambdadelta/ground/relocation/xap.ma      |  5 +++
 10 files changed, 102 insertions(+), 40 deletions(-)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/dbfr.ma => etc/balanced/dbfr.etc} (83%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/dbfr_ibfr.ma => etc/balanced/dbfr_ibfr.etc} (76%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/dbfr_lift.ma => etc/balanced/dbfr_lift.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/ibfr.ma => etc/balanced/ibfr.etc} (83%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr.etc
similarity index 83%
rename from matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr.etc
index 349195cb0..f82db8a73 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr.etc
@@ -15,7 +15,7 @@
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/syntax/prototerm_constructors.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
-include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/syntax/path_balanced.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/notation/relations/black_rightarrow_dbf_3.ma".
@@ -24,13 +24,11 @@ include "ground/xoa/ex_6_5.ma".
 
 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
 
-(**) (* explicit ninj because we cannot declare the expectd type of k *)
 definition dbfr (r): relation2 prototerm prototerm ≝
            λt1,t2.
-           ∃∃p,b,q,h,k. p●𝗔◗b●𝗟◗q = r &
-           ⊗b ϵ 𝐁 & b = ↳[h]b &
-           (𝗟◗q) = ↳[ninj k](𝗟◗q) & r◖𝗱k ϵ t1 &
-           t1[⋔r←𝛕(k+h).(t1⋔(p◖𝗦))] ⇔ t2
+           ∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
+           ⊗b ϵ 𝐁 & b ϵ 𝐂❨m❩ & q ϵ 𝐂❨n❩ & r◖𝗱↑n ϵ t1 &
+           t1[⋔r←𝛕↑(m+n).(t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_ibfr.etc
similarity index 76%
rename from matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_ibfr.etc
index 043f61085..d7c16ca2b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_ibfr.etc
@@ -19,13 +19,13 @@ include "delayed_updating/unwind/unwind2_constructors.ma".
 include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
 include "delayed_updating/unwind/unwind2_preterm_eq.ma".
 include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
-include "delayed_updating/unwind/unwind2_rmap_head.ma".
+include "delayed_updating/unwind/unwind2_rmap_closed.ma".
 
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 
 include "delayed_updating/syntax/prototerm_proper_constructors.ma".
-include "delayed_updating/syntax/path_head_structure.ma".
+include "delayed_updating/syntax/path_closed_structure.ma".
 include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
@@ -35,22 +35,21 @@ include "delayed_updating/syntax/path_structure_depth.ma".
 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 #h #k #Hr #Hb #Hh #H1k #Ht1 #Ht2 destruct
-@(ex6_5_intro … (⊗p) (⊗b) (⊗q) (♭b) (↑♭q))
-[ -H0t1 -Hb -Hh -H1k -Ht1 -Ht2 //
-| -H0t1 -Hh -H1k -Ht1 -Ht2 //
-| -H0t1 -Hb -Ht1 -H1k -Ht2
-  >Hh in ⊢ (??%?); >path_head_structure_depth <Hh -Hh //
-| -H0t1 -Hb -Hh -Ht1 -Ht2
-  >structure_L_sn
-  >H1k in ⊢ (??%?); >path_head_structure_depth <H1k -H1k //
-| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1 -Hb -Hh
-  <unwind2_path_d_dx >list_append_rcons_dx >list_append_assoc
-  lapply (unwind2_rmap_append_pap_closed f … (p●𝗔◗b) … H1k) -H1k
-  <depth_L_sn #H2k
-  lapply (eq_inv_ninj_bi … H2k) -H2k #H2k <H2k -H2k #Ht1 //
+* #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 -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
+  <unwind2_path_d_dx <tr_pap_succ_nap >list_append_rcons_dx >list_append_assoc
+  <unwind2_rmap_append_closed_nap //
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
+(*
   lapply (path_head_refl_append_bi … Hh H1k) -Hh -H1k <nrplus_inj_sn #H1k
+*)
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_ppc …))
   [ @fsubst_eq_repl [ // | // ]
@@ -61,14 +60,16 @@ theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
     <list_append_rcons_sn
-    @(stream_eq_trans … (tr_compose_uni_dx …))
+    @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
     @tr_compose_eq_repl
-    [ <unwind2_rmap_append_pap_closed //
+(* TODO  
+    [ <unwind2_rmap_append_closed_nap //   
       <depth_append <depth_L_sn
       <nplus_comm <nrplus_npsucc_sn <nplus_succ_sn //
     | >unwind2_rmap_A_dx
       /2 width=1 by tls_unwind2_rmap_closed/
     ]
+*)
 (* Note: crux of the proof ends *)
   | //
   | /2 width=2 by ex_intro/
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_lift.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_lift.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/ibfr.etc
similarity index 83%
rename from matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/ibfr.etc
index b235cb481..dfa14ef98 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/ibfr.etc
@@ -15,7 +15,7 @@
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/substitution/lift_prototerm.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
-include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/syntax/path_balanced.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/notation/relations/black_rightarrow_ibf_3.ma".
@@ -25,13 +25,11 @@ include "ground/xoa/ex_6_5.ma".
 
 (* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
 
-(**) (* explicit ninj because we cannot declare the expectd type of k *)
 definition ibfr (r): relation2 prototerm prototerm ≝
            λt1,t2.
-           ∃∃p,b,q,h,k. p●𝗔◗b●𝗟◗q = r &
-           ⊗b ϵ 𝐁 & b = ↳[h]b &
-           (𝗟◗q) = ↳[ninj k](𝗟◗q) & r◖𝗱k ϵ t1 &
-           t1[⋔r←↑[𝐮❨k+h❩](t1⋔(p◖𝗦))] ⇔ t2
+           ∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
+           ⊗b ϵ 𝐁 & b ϵ 𝐂❨m❩ & q ϵ 𝐂❨n❩ & r◖𝗱↑n ϵ t1 &
+           t1[⋔r←↑[𝐮❨↑(m+n)❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
index 5f37abd5f..d64067123 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -42,7 +42,7 @@ theorem dfr_des_ifr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
   /2 width=2 by path_closed_structure_depth/
 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1
   <unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn
-  <unwind2_rmap_append_closed_nap //
+  <unwind2_rmap_append_closed_Lq_dx_nap_depth //
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_ppc …))
@@ -56,8 +56,8 @@ theorem dfr_des_ifr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
     <list_append_rcons_sn
     @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
     @tr_compose_eq_repl
-    [ <unwind2_rmap_append_closed_nap //
-    | /2 width=1 by tls_succ_unwind2_rmap_append_L_closed_dx/
+    [ <unwind2_rmap_append_closed_Lq_dx_nap_depth //
+    | /2 width=1 by tls_succ_unwind2_rmap_append_closed_Lq_dx/
     ]
 (* Note: crux of the proof ends *)
   | //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
index 077ff798e..d3b567b72 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
@@ -40,7 +40,7 @@ lemma ifr_unwind_bi (f) (t1) (t2) (r):
   /2 width=2 by path_closed_structure_depth/
 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2r
   <unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn
-  <unwind2_rmap_append_closed_nap //
+  <unwind2_rmap_append_closed_Lq_dx_nap_depth //
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_pic …))
@@ -54,8 +54,8 @@ lemma ifr_unwind_bi (f) (t1) (t2) (r):
     <list_append_rcons_sn
     @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
     @tr_compose_eq_repl
-    [ <unwind2_rmap_append_closed_nap //
-    | /2 width=1 by tls_succ_unwind2_rmap_append_L_closed_dx/
+    [ <unwind2_rmap_append_closed_Lq_dx_nap_depth //
+    | /2 width=1 by tls_succ_unwind2_rmap_append_closed_Lq_dx/
     ]
 (* Note: crux of the proof ends *)
   | //
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 7c551ed85..9879b54fb 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
@@ -48,7 +48,7 @@ lemma unwind2_rmap_append_closed_dx_xap_le (f) (p) (q) (n):
 ]
 qed-.
 
-lemma unwind2_rmap_append_L_closed_dx_nap (f) (p) (q) (n):
+lemma unwind2_rmap_append_closed_Lq_dx_nap (f) (p) (q) (n):
       q ϵ 𝐂❨n❩ →
       ▶[f](𝗟◗q)＠§❨n❩ = ▶[f](p●𝗟◗q)＠§❨n❩.
 #f #p #q #n #Hq
@@ -66,11 +66,11 @@ lemma unwind2_rmap_push_closed_nap (f) (q) (n):
 <unwind2_rmap_d_dx <tr_compose_nap //
 qed-.
 
-lemma unwind2_rmap_append_closed_nap (f) (p) (q) (n):
+lemma unwind2_rmap_append_closed_Lq_dx_nap_depth (f) (p) (q) (n):
       q ϵ 𝐂❨n❩ →
       ♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
 #f #p #q #n #Hq
-<unwind2_rmap_append_L_closed_dx_nap //
+<unwind2_rmap_append_closed_Lq_dx_nap //
 /2 width=1 by unwind2_rmap_push_closed_nap/
 qed-.
 
@@ -85,8 +85,18 @@ lemma tls_succ_plus_unwind2_rmap_push_closed (f) (q) (n):
 ]
 qed-.
 
-lemma tls_succ_unwind2_rmap_append_L_closed_dx (f) (p) (q) (n):
+lemma tls_succ_unwind2_rmap_append_closed_Lq_dx (f) (p) (q) (n):
       q ϵ 𝐂❨n❩ →
       ▶[f]p ≗ ⇂*[↑n]▶[f](p●𝗟◗q).
 /2 width=1 by tls_succ_plus_unwind2_rmap_push_closed/
 qed-.
+
+lemma unwind2_rmap_append_closed_Lq_dx_nap_plus (f) (p) (q) (m) (n):
+      q ϵ 𝐂❨n❩ →
+      ▶[f]p＠❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
+#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=1 by unwind2_rmap_append_closed_Lq_dx_nap_depth/
+]
+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
new file mode 100644
index 000000000..1f2a9d530
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 b: path ≝ 𝐞◖𝗔◖𝗟◖𝗱𝟏.
+
+lemma b_unfold: 𝐞◖𝗔◖𝗟◖𝗱𝟏 = b.
+// qed.
+
+lemma b_balanced: ⊗b ϵ 𝐁.
+<b_unfold <structure_d_dx
+/2 width=1 by pbc_empty, pbc_redex/
+qed.
+
+lemma b_closed: b ϵ 𝐂❨𝟎❩.
+/4 width=1 by pcc_A_sn, pcc_empty, pcc_d_dx, pcc_L_dx/
+qed.
+
+lemma b_unwind2_rmap_unfold (f):
+      (⫯f)∘𝐮❨𝟏❩ = ▶[f]b.
+// qed.
+
+lemma b_unwind2_rmap_pap_unit (f):
+      ↑(f＠⧣❨𝟏❩) = ▶[f]b＠⧣❨𝟏❩.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
index 2343c74ac..abae78a7e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
@@ -19,6 +19,13 @@ include "ground/lib/stream_hdtl_eq.ma".
 
 (* UNIFORM ELEMENTS FOR TOTAL RELOCATION MAPS *******************************)
 
+(* Constructions with tr_compose and tr_next ********************************)
+
+lemma tr_compose_uni_unit_sn (f):
+      ↑f ≗ 𝐮❨𝟏❩∘f.
+#f >nsucc_zero <tr_uni_succ //
+qed.
+
 (* Constructions with tr_compose and tr_tl **********************************)
 
 lemma tr_tl_compose_uni_sn (n) (f):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
index aef0c26e1..0f367b218 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
@@ -77,3 +77,8 @@ theorem tr_xap_eq_repl (i):
 <tr_xap_unfold <tr_xap_unfold
 /3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/
 qed.
+
+lemma tr_nap_plus (f) (m) (n):
+      ⇂*[↑n]f＠❨m❩+f＠§❨n❩ = f＠§❨m+n❩.
+/2 width=1 by eq_inv_nsucc_bi/
+qed.
-- 
2.39.2