X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_depth.ma;h=a769327f65b218f655530102b435ca614b60eb22;hb=9e31ac1f3f868349154b0ce2e550e2476aaf6a30;hp=474bbcbda501f43dd5de91697dd321d58ca33c7f;hpb=3c78efa39d4783f83638b1aabe8d776d83aabf35;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 474bbcbda..a769327f6 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -23,7 +23,7 @@ match p with
 [ list_empty     ⇒ 𝟎
 | list_lcons l q ⇒
   match l with
-  [ label_d _ ⇒ depth q
+  [ label_d k ⇒ depth q
   | label_m   ⇒ depth q
   | label_L   ⇒ ↑(depth q)
   | label_A   ⇒ depth q
@@ -40,53 +40,58 @@ interpretation
 lemma depth_empty: 𝟎 = ♭𝐞.
 // qed.
 
-lemma depth_d_sn (q) (n): ♭q = ♭(𝗱n◗q).
+lemma depth_d_dx (p) (k):
+      ♭p = ♭(p◖𝗱k).
 // qed.
 
-lemma depth_m_sn (q): ♭q = ♭(𝗺◗q).
+lemma depth_m_dx (p):
+      ♭p = ♭(p◖𝗺).
 // qed.
 
-lemma depth_L_sn (q): ↑♭q = ♭(𝗟◗q).
+lemma depth_L_dx (p):
+      ↑♭p = ♭(p◖𝗟).
 // qed.
 
-lemma depth_A_sn (q): ♭q = ♭(𝗔◗q).
+lemma depth_A_dx (p):
+      ♭p = ♭(p◖𝗔).
 // qed.
 
-lemma depth_S_sn (q): ♭q = ♭(𝗦◗q).
+lemma depth_S_dx (p):
+      ♭p = ♭(p◖𝗦).
 // qed.
 
 (* Main constructions *******************************************************)
 
-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 //
-| <depth_m_sn <depth_m_sn //
-| <depth_L_sn <depth_L_sn //
-| <depth_A_sn <depth_A_sn //
-| <depth_S_sn <depth_S_sn //
+theorem depth_append (p) (q):
+        (♭p)+(♭q) = ♭(p●q).
+#p #q elim q -q //
+* [ #k ] #q #IH <list_append_lcons_sn
+[ <depth_d_dx <depth_d_dx //
+| <depth_m_dx <depth_m_dx //
+| <depth_L_dx <depth_L_dx //
+| <depth_A_dx <depth_A_dx //
+| <depth_S_dx <depth_S_dx //
 ]
 qed.
 
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
 
-lemma depth_d_dx (p) (n):
-      ♭p = ♭(p◖𝗱n).
+lemma depth_d_sn (p) (k):
+      ♭p = ♭(𝗱k◗p).
 // qed.
 
-lemma depth_m_dx (p):
-      ♭p = ♭(p◖𝗺).
+lemma depth_m_sn (p):
+      ♭p = ♭(𝗺◗p).
 // qed.
 
-lemma depth_L_dx (p):
-      ↑♭p = ♭(p◖𝗟).
+lemma depth_L_sn (p):
+      ↑♭p = ♭(𝗟◗p).
 // qed.
 
-lemma depth_A_dx (p):
-      ♭p = ♭(p◖𝗔).
+lemma depth_A_sn (p):
+      ♭p = ♭(𝗔◗p).
 // qed.
 
-lemma depth_S_dx (p):
-      ♭p = ♭(p◖𝗦).
+lemma depth_S_sn (p):
+      ♭p = ♭(𝗦◗p).
 // qed.