--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/fsubst.ma".
+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_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".
+
+(* 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 &
+ t1[⋔r←𝛕↑(m+n).(t1⋔(p◖𝗦))] ⇔ t2
+.
+
+interpretation
+ "balanced focused reduction with delayed updating (prototerm)"
+ 'BlackRightArrowDBF t1 r t2 = (dbfr r t1 t2).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/reduction/ibfr.ma".
+
+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_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.
+#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
+ /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 [ // | // ]
+ @(subset_eq_trans … (unwind2_term_iref …))
+ @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
+ [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
+ @(subset_eq_trans … (lift_unwind2_term_after …))
+ @unwind2_term_eq_repl_sn
+(* Note: crux of the proof begins *)
+ <list_append_rcons_sn
+ @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
+ @tr_compose_eq_repl
+(* 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/
+ | //
+ ]
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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_lift.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_constructors.ma".
+include "delayed_updating/substitution/lift_path_head.ma".
+include "delayed_updating/substitution/lift_rmap_head.ma".
+
+(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
+
+(* Constructions with lift **************************************************)
+
+theorem dfr_lift_bi (f) (t1) (t2) (r):
+ t1 ➡𝐝𝐛𝐟[r] t2 → ↑[f]t1 ➡𝐝𝐛𝐟[↑[f]r] ↑[f]t2.
+#f #t1 #t2 #r
+* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
+@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)@⧣❨k❩))
+[ -H1k -Ht1 -Ht2 //
+| -Ht1 -Ht2
+ <lift_rmap_L_dx >lift_path_L_sn
+ <(lift_path_head_closed … H1k) in ⊢ (??%?); -H1k //
+| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1k
+ <lift_path_d_dx #Ht1 //
+| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
+ @(subset_eq_trans … Ht2) -t2
+ @(subset_eq_trans … (lift_term_fsubst …))
+ @fsubst_eq_repl [ // | // ]
+ @(subset_eq_trans … (lift_term_iref …))
+ @iref_eq_repl
+ @(subset_eq_canc_sn … (lift_term_grafted_S …))
+ @lift_term_eq_repl_sn
+(* Note: crux of the proof begins *)
+ >list_append_rcons_sn in H1k; #H1k >lift_rmap_A_dx
+ /2 width=1 by tls_lift_rmap_closed/
+(* Note: crux of the proof ends *)
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/fsubst.ma".
+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_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".
+
+(* 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 &
+ t1[⋔r←↑[𝐮❨↑(m+n)❩](t1⋔(p◖𝗦))] ⇔ t2
+.
+
+interpretation
+ "balanced focused reduction with immediate updating (prototerm)"
+ 'BlackRightArrowIBF t1 r t2 = (ibfr r t1 t2).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/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_balanced.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".
-
-(* 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
-.
-
-interpretation
- "balanced focused reduction with delayed updating (prototerm)"
- 'BlackRightArrowDBF t1 r t2 = (dbfr r t1 t2).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/reduction/ibfr.ma".
-
-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/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_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.
-#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 //
-| 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 [ // | // ]
- @(subset_eq_trans … (unwind2_term_iref …))
- @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
- [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
- @(subset_eq_trans … (lift_unwind2_term_after …))
- @unwind2_term_eq_repl_sn
-(* Note: crux of the proof begins *)
- <list_append_rcons_sn
- @(stream_eq_trans … (tr_compose_uni_dx …))
- @tr_compose_eq_repl
- [ <unwind2_rmap_append_pap_closed //
- <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/
- | //
- ]
-]
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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_lift.ma".
-include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_constructors.ma".
-include "delayed_updating/substitution/lift_path_head.ma".
-include "delayed_updating/substitution/lift_rmap_head.ma".
-
-(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
-
-(* Constructions with lift **************************************************)
-
-theorem dfr_lift_bi (f) (t1) (t2) (r):
- t1 ➡𝐝𝐛𝐟[r] t2 → ↑[f]t1 ➡𝐝𝐛𝐟[↑[f]r] ↑[f]t2.
-#f #t1 #t2 #r
-* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
-@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)@⧣❨k❩))
-[ -H1k -Ht1 -Ht2 //
-| -Ht1 -Ht2
- <lift_rmap_L_dx >lift_path_L_sn
- <(lift_path_head_closed … H1k) in ⊢ (??%?); -H1k //
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1k
- <lift_path_d_dx #Ht1 //
-| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
- @(subset_eq_trans … Ht2) -t2
- @(subset_eq_trans … (lift_term_fsubst …))
- @fsubst_eq_repl [ // | // ]
- @(subset_eq_trans … (lift_term_iref …))
- @iref_eq_repl
- @(subset_eq_canc_sn … (lift_term_grafted_S …))
- @lift_term_eq_repl_sn
-(* Note: crux of the proof begins *)
- >list_append_rcons_sn in H1k; #H1k >lift_rmap_A_dx
- /2 width=1 by tls_lift_rmap_closed/
-(* Note: crux of the proof ends *)
-]
-qed.
/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 …))
<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 *)
| //
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/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_balanced.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".
-
-(* 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
-.
-
-interpretation
- "balanced focused reduction with immediate updating (prototerm)"
- 'BlackRightArrowIBF t1 r t2 = (ibfr r t1 t2).
/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 …))
<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 *)
| //
]
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
<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-.
]
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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
(* 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):
<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.