--- /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.