X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_structure.ma;h=0330665ad2e55ca16d2417900eef45f61b122aa7;hb=13584a37bbcde10e03c8a488f5b93e1e042da0a6;hp=8c60eea7595c8a88c43250865500b11010701dee;hpb=2cc4eb5d0210be58286e028278852122dcb68052;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
index 8c60eea75..0330665ad 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -22,10 +22,11 @@ match p with
 [ list_empty     ⇒ 𝐞
 | list_lcons l q ⇒
    match l with
-   [ label_node_d n ⇒ structure q
-   | label_edge_L   ⇒ 𝗟◗structure q
-   | label_edge_A   ⇒ 𝗔◗structure q
-   | label_edge_S   ⇒ 𝗦◗structure q
+   [ label_d n ⇒ structure q
+   | label_m   ⇒ structure q
+   | label_L   ⇒ 𝗟◗structure q
+   | label_A   ⇒ 𝗔◗structure q
+   | label_S   ⇒ 𝗦◗structure q
    ]
 ].
 
@@ -43,16 +44,20 @@ lemma structure_d_sn (p) (n):
       ⊗p = ⊗(𝗱n◗p).
 // qed.
 
+lemma structure_m_sn (p):
+      ⊗p = ⊗(𝗺◗p).
+// qed.
+
 lemma structure_L_sn (p):
-      𝗟◗⊗p = ⊗(𝗟◗p).
+      (𝗟◗⊗p) = ⊗(𝗟◗p).
 // qed.
 
 lemma structure_A_sn (p):
-      𝗔◗⊗p = ⊗(𝗔◗p).
+      (𝗔◗⊗p) = ⊗(𝗔◗p).
 // qed.
 
 lemma structure_S_sn (p):
-      𝗦◗⊗p = ⊗(𝗦◗p).
+      (𝗦◗⊗p) = ⊗(𝗦◗p).
 // qed.
 
 (* Main constructions *******************************************************)
@@ -75,6 +80,11 @@ lemma structure_d_dx (p) (n):
 #p #n <structure_append //
 qed.
 
+lemma structure_m_dx (p):
+      ⊗p = ⊗(p◖𝗺).
+#p <structure_append //
+qed.
+
 lemma structure_L_dx (p):
       (⊗p)◖𝗟 = ⊗(p◖𝗟).
 #p <structure_append //