X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_rmap_unprotected.ma;h=df93a6709fa1e6f4a058d58306a4248bce6e94b4;hp=b8cb1d2cf7cb176180bf3e5d16b24a6801097b86;hb=513c4a61f11ce03888a8a0f9d8e513de6e3a7c8b;hpb=48cd63fc7f4415925582eae224a36a9c1bb3cc06

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
index b8cb1d2cf..df93a6709 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
@@ -20,24 +20,24 @@ include "delayed_updating/syntax/path_structure.ma".
 
 (* Example of unprotected balanced path *************************************)
 
-definition b: path ≝ 𝐞◖𝗔◖𝗟◖𝗱𝟏.
+definition l3_b: path ≝ 𝐞◖𝗔◖𝗟◖𝗱𝟏.
 
-lemma b_unfold: 𝐞◖𝗔◖𝗟◖𝗱𝟏 = b.
+lemma l3_b_unfold: 𝐞◖𝗔◖𝗟◖𝗱𝟏 = l3_b.
 // qed.
 
-lemma b_balanced: ⊗b ϵ 𝐁.
-<b_unfold <structure_d_dx
+lemma l3_b_balanced: ⊗l3_b ϵ 𝐁.
+<l3_b_unfold <structure_d_dx
 /2 width=1 by pbc_empty, pbc_redex/
 qed.
 
-lemma b_closed: b ϵ 𝐂❨Ⓕ,𝟎❩.
+lemma l3_b_closed: l3_b ϵ 𝐂❨Ⓕ,𝟎❩.
 /4 width=1 by pcc_A_sn, pcc_empty, pcc_false_d_dx, pcc_L_dx/
 qed.
 
-lemma b_unwind2_rmap_unfold (f):
-      (⫯f)∘𝐮❨𝟏❩ = ▶[f]b.
+lemma l3_b_unwind2_rmap_unfold (f):
+      (⫯f)∘𝐮❨𝟏❩ = ▶[f]l3_b.
 // qed.
 
-lemma b_unwind2_rmap_pap_unit (f):
-      ↑(f＠⧣❨𝟏❩) = ▶[f]b＠⧣❨𝟏❩.
+lemma l3_b_unwind2_rmap_pap_unit (f):
+      ↑(f＠⧣❨𝟏❩) = ▶[f]l3_b＠⧣❨𝟏❩.
 // qed.