update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind / unwind2_rmap.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma
index 879af25186de361c55a6abc83d74a877003e8b73..5177fd7eea72a4281515f1259b9ee8afb8836d52 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma
@@ -12,92 +12,81 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "delayed_updating/unwind/preunwind2_rmap.ma".
 include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/functions/black_righttriangle_2.ma".
-include "delayed_updating/notation/functions/black_righttriangle_1.ma".
-include "ground/relocation/tr_uni.ma".
-include "ground/relocation/tr_compose.ma".
 
-(* UNWIND MAP FOR PATH ******************************************************)
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
 
 rec definition unwind2_rmap (f) (p) on p: tr_map ≝
 match p with
 [ list_empty     ⇒ f
-| list_lcons l q ⇒
-  match l with
-  [ label_d n ⇒ (unwind2_rmap f q)∘𝐮❨n❩
-  | label_m   ⇒ unwind2_rmap f q
-  | label_L   ⇒ ⫯(unwind2_rmap f q)
-  | label_A   ⇒ unwind2_rmap f q
-  | label_S   ⇒ unwind2_rmap f q
-  ]
+| list_lcons l q ⇒ ▶[unwind2_rmap f q]l
 ].
 
 interpretation
-  "tailed unwind map (reversed path)"
+  "tailed unwind (relocation map)"
   'BlackRightTriangle f p = (unwind2_rmap f p).
 
-interpretation
-  "unwind map (reversed path)"
-  'BlackRightTriangle p = (unwind2_rmap tr_id p).
-
 (* Basic constructions ******************************************************)
 
 lemma unwind2_rmap_empty (f):
       f = ▶[f]𝐞.
 // qed.
 
-lemma unwind2_rmap_d_sn (f) (p) (n:pnat):
-      (▶[f]p∘𝐮❨n❩) = ▶[f](𝗱n◗p).
+lemma unwind2_rmap_rcons (f) (p) (l):
+      ▶[▶[f]p]l = ▶[f](p◖l).
 // qed.
 
-lemma unwind2_rmap_m_sn (f) (p):
-      ▶[f]p = ▶[f](𝗺◗p).
+lemma unwind2_rmap_d_dx (f) (p) (k:pnat):
+      ▶[f]p∘𝐮❨k❩ = ▶[f](p◖𝗱k).
 // qed.
 
-lemma unwind2_rmap_L_sn (f) (p):
-      (⫯▶[f]p) = ▶[f](𝗟◗p).
+lemma unwind2_rmap_m_dx (f) (p):
+      ▶[f]p = ▶[f](p◖𝗺).
 // qed.
 
-lemma unwind2_rmap_A_sn (f) (p):
-      ▶[f]p = ▶[f](𝗔◗p).
+lemma unwind2_rmap_L_dx (f) (p):
+      (⫯▶[f]p) = ▶[f](p◖𝗟).
 // qed.
 
-lemma unwind2_rmap_S_sn (f) (p):
-      ▶[f]p = ▶[f](𝗦◗p).
+lemma unwind2_rmap_A_dx (f) (p):
+      ▶[f]p = ▶[f](p◖𝗔).
+// qed.
+
+lemma unwind2_rmap_S_dx (f) (p):
+      ▶[f]p = ▶[f](p◖𝗦).
 // qed.
 
-(* Constructions with list_append *******************************************)
-
-lemma unwind2_rmap_append (f) (p1) (p2):
-      ▶[▶[f]p2]p1 = ▶[f](p1●p2).
-#f #p1 elim p1 -p1 //
-* [ #n ] #p1 #IH #p2 //
-[ <unwind2_rmap_m_sn <unwind2_rmap_m_sn //
-| <unwind2_rmap_L_sn <unwind2_rmap_L_sn //
-| <unwind2_rmap_A_sn <unwind2_rmap_A_sn //
-| <unwind2_rmap_S_sn <unwind2_rmap_S_sn //
-]
+(* Constructions with path_append *******************************************)
+
+lemma unwind2_rmap_append (f) (p) (q):
+      ▶[▶[f]p]q = ▶[f](p●q).
+#f #p #q elim q -q // #l #q #IH
+<unwind2_rmap_rcons <unwind2_rmap_rcons //
 qed.
 
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
 
-lemma unwind2_rmap_d_dx (f) (p) (n:pnat):
-      ▶[f∘𝐮❨n❩]p = ▶[f](p◖𝗱n).
+lemma unwind2_rmap_lcons (f) (p) (l):
+      ▶[▶[f]l]p = ▶[f](l◗p).
 // qed.
 
-lemma unwind2_rmap_m_dx (f) (p):
-      ▶[f]p = ▶[f](p◖𝗺).
+lemma unwind2_rmap_d_sn (f) (p) (k:pnat):
+      ▶[f∘𝐮❨k❩]p = ▶[f](𝗱k◗p).
 // qed.
 
-lemma unwind2_rmap_L_dx (f) (p):
-      ▶[⫯f]p = ▶[f](p◖𝗟).
+lemma unwind2_rmap_m_sn (f) (p):
+      ▶[f]p = ▶[f](𝗺◗p).
 // qed.
 
-lemma unwind2_rmap_A_dx (f) (p):
-      ▶[f]p = ▶[f](p◖𝗔).
+lemma unwind2_rmap_L_sn (f) (p):
+      ▶[⫯f]p = ▶[f](𝗟◗p).
 // qed.
 
-lemma unwind2_rmap_S_dx (f) (p):
-      ▶[f]p = ▶[f](p◖𝗦).
+lemma unwind2_rmap_A_sn (f) (p):
+      ▶[f]p = ▶[f](𝗔◗p).
+// qed.
+
+lemma unwind2_rmap_S_sn (f) (p):
+      ▶[f]p = ▶[f](𝗦◗p).
 // qed.