X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_depth.ma;h=cdf24943af922c8a47c74990fb79e92acf803231;hb=e0c91d8a4422da0b39aca790e5826dc8a617b303;hp=a85d74ef16e4f6b1e84a62db74e0119c0fdbd6ac;hpb=ad49f5895fadff5a1d9845debb1c852a1455c6c9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
index a85d74ef1..cdf24943a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -55,10 +55,10 @@ lemma depth_A_sn (q): ❘q❘ = ❘𝗔◗q❘.
 lemma depth_S_sn (q): ❘q❘ = ❘𝗦◗q❘.
 // qed.
 
-(* Advanced constructions with nplus ****************************************)
+(* Main constructions *******************************************************)
 
-lemma depth_plus (p1) (p2):
-      ❘p2❘+❘p1❘ = ❘p1●p2❘.
+theorem depth_append (p1) (p2):
+        ❘p2❘+❘p1❘ = ❘p1●p2❘.
 #p1 elim p1 -p1 //
 * [ #n ] #p1 #IH #p2 <list_append_lcons_sn
 [ <depth_d_sn <depth_d_sn //
@@ -68,3 +68,25 @@ lemma depth_plus (p1) (p2):
 | <depth_S_sn <depth_S_sn //
 ]
 qed.
+
+(* Constructions with list_rcons ********************************************)
+
+lemma depth_d_dx (p) (n):
+      ❘p❘ = ❘p◖𝗱n❘.
+// qed.
+
+lemma depth_m_dx (p):
+      ❘p❘ = ❘p◖𝗺❘.
+// qed.
+
+lemma depth_L_dx (p):
+      ↑❘p❘ = ❘p◖𝗟❘.
+// qed.
+
+lemma depth_A_dx (p):
+      ❘p❘ = ❘p◖𝗔❘.
+// qed.
+
+lemma depth_S_dx (p):
+      ❘p❘ = ❘p◖𝗦❘.
+// qed.