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=1b82038aa813e24e84959526e83dd35d849b51f2;hp=d7608ba18cc41268dff09f4f27c6e065829a8cbb;hpb=9605ffc88831066a901ea4eb8e419f277662f372;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 d7608ba18..0330665ad 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -17,18 +17,85 @@ include "delayed_updating/notation/functions/circled_times_1.ma".
 
 (* STRUCTURE FOR PATH *******************************************************)
 
-rec definition path_structure (p) on p ≝
+rec definition structure (p) on p ≝
 match p with
 [ list_empty     ⇒ 𝐞
 | list_lcons l q ⇒
    match l with
-   [ label_node_d n ⇒ path_structure q
-   | label_edge_L   ⇒ 𝗟;path_structure q
-   | label_edge_A   ⇒ 𝗔;path_structure q
-   | label_edge_S   ⇒ 𝗦;path_structure q
+   [ label_d n ⇒ structure q
+   | label_m   ⇒ structure q
+   | label_L   ⇒ 𝗟◗structure q
+   | label_A   ⇒ 𝗔◗structure q
+   | label_S   ⇒ 𝗦◗structure q
    ]
 ].
 
 interpretation
   "structure (path)"
-  'CircledTimes p = (path_structure p).
+  'CircledTimes p = (structure p).
+
+(* Basic constructions ******************************************************)
+
+lemma structure_empty:
+      𝐞 = ⊗𝐞.
+// qed.
+
+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).
+// qed.
+
+lemma structure_A_sn (p):
+      (𝗔◗⊗p) = ⊗(𝗔◗p).
+// qed.
+
+lemma structure_S_sn (p):
+      (𝗦◗⊗p) = ⊗(𝗦◗p).
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem structure_idem (p):
+        ⊗p = ⊗⊗p.
+#p elim p -p [| * [ #n ] #p #IH ] //
+qed.
+
+theorem structure_append (p1) (p2):
+        ⊗p1●⊗p2 = ⊗(p1●p2).
+#p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
+[||*: <list_append_lcons_sn ] //
+qed.
+
+(* Constructions with list_rcons ********************************************)
+
+lemma structure_d_dx (p) (n):
+      ⊗p = ⊗(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 //
+qed.
+
+lemma structure_A_dx (p):
+      (⊗p)◖𝗔 = ⊗(p◖𝗔).
+#p <structure_append //
+qed.
+
+lemma structure_S_dx (p):
+      (⊗p)◖𝗦 = ⊗(p◖𝗦).
+#p <structure_append //
+qed.