update in ground

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_height.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma
index 52e6f01e53ebea35423430fa46ca2871ced7c047..934df56d0dcce4c06942c958a004bc6090224d15 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height.ma
@@ -14,7 +14,7 @@
 
 include "ground/arith/nat_plus.ma".
 include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/functions/hash_1.ma".
+include "delayed_updating/notation/functions/sharp_1.ma".
 
 (* HEIGHT FOR PATH **********************************************************)
 
@@ -23,7 +23,7 @@ match p with
 [ list_empty     ⇒ 𝟎
 | list_lcons l q ⇒
   match l with
-  [ label_d n ⇒ n + height q
+  [ label_d k ⇒ height q + k
   | label_m   ⇒ height q
   | label_L   ⇒ height q
   | label_A   ⇒ height q
@@ -33,60 +33,65 @@ match p with
 
 interpretation
   "height (path)"
-  'Hash p = (height p).
+  'Sharp p = (height p).
 
 (* Basic constructions ******************************************************)
 
-lemma height_empty: ð\9d\9f\8e = ⧣𝐞.
+lemma height_empty: ð\9d\9f\8e = â\99¯𝐞.
 // qed.
 
-lemma height_d_sn (q) (n): ninj n+⧣q = ⧣(𝗱n◗q).
+lemma height_d_dx (p) (k:pnat):
+      (♯p)+k = ♯(p◖𝗱k).
 // qed.
 
-lemma height_m_sn (q): ⧣q = ⧣(𝗺◗q).
+lemma height_m_dx (p):
+      (♯p) = ♯(p◖𝗺).
 // qed.
 
-lemma height_L_sn (q): ⧣q = ⧣(𝗟◗q).
+lemma height_L_dx (p):
+      (♯p) = ♯(p◖𝗟).
 // qed.
 
-lemma height_A_sn (q): ⧣q = ⧣(𝗔◗q).
+lemma height_A_dx (p):
+      (♯p) = ♯(p◖𝗔).
 // qed.
 
-lemma height_S_sn (q): ⧣q = ⧣(𝗦◗q).
+lemma height_S_dx (p):
+      (♯p) = ♯(p◖𝗦).
 // qed.
 
 (* Main constructions *******************************************************)
 
-theorem height_append (p1) (p2):
-        (⧣p2+⧣p1) = ⧣(p1â\97\8fp2).
-#p1 elim p1 -p1 //
-* [ #n ] #p1 #IH #p2 <list_append_lcons_sn
-[ <height_d_sn <height_d_sn //
-| <height_m_sn <height_m_sn //
-| <height_L_sn <height_L_sn //
-| <height_A_sn <height_A_sn //
-| <height_S_sn <height_S_sn //
+theorem height_append (p) (q):
+        (â\99¯p+â\99¯q) = â\99¯(pâ\97\8fq).
+#p #q elim q -q //
+* [ #k ] #q #IH <list_append_lcons_sn
+[ <height_d_dx <height_d_dx //
+| <height_m_dx <height_m_dx //
+| <height_L_dx <height_L_dx //
+| <height_A_dx <height_A_dx //
+| <height_S_dx <height_S_dx //
 ]
 qed.
 
-(* Constructions with list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
 
-lemma height_d_dx (p) (n):
-      (⧣p)+(ninj n) = ⧣(p◖𝗱n).
+lemma height_d_sn (p) (k:pnat):
+      k+♯p = ♯(𝗱k◗p).
 // qed.
 
-lemma height_m_dx (p):
-      (⧣p) = ⧣(p◖𝗺).
+lemma height_m_sn (p):
+      ♯p = ♯(𝗺◗p).
 // qed.
 
-lemma height_L_dx (p):
-      (⧣p) = ⧣(p◖𝗟).
+lemma height_L_sn (p):
+      ♯p = ♯(𝗟◗p).
 // qed.
 
-lemma height_A_dx (p):
-      (⧣p) = ⧣(p◖𝗔).
+lemma height_A_sn (p):
+      ♯p = ♯(𝗔◗p).
 // qed.
 
-lemma height_S_dx (p):
-      (⧣p) = ⧣(p◖𝗦).
+lemma height_S_sn (p):
+      ♯p = ♯(𝗦◗p).
 // qed.