X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_height.ma;h=73c7e21e90de90fa15b338d4e71ecc046983af89;hb=eba13527cf74de399b7e5b958901962666d4cd25;hp=52e6f01e53ebea35423430fa46ca2871ced7c047;hpb=aeec9312d6f72526a460518a1e889eac71657cdd;p=helm.git

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 52e6f01e5..73c7e21e9 100644
--- 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 **********************************************************)
 
@@ -33,32 +33,32 @@ match p with
 
 interpretation
   "height (path)"
-  'Hash p = (height p).
+  'Sharp p = (height p).
 
 (* Basic constructions ******************************************************)
 
-lemma height_empty: ð = â§£ð.
+lemma height_empty: ð = â¯ð.
 // qed.
 
-lemma height_d_sn (q) (n): ninj n+â§£q = â§£(ð±nâq).
+lemma height_d_sn (q) (n): ninj n+â¯q = â¯(ð±nâq).
 // qed.
 
-lemma height_m_sn (q): â§£q = â§£(ðºâq).
+lemma height_m_sn (q): â¯q = â¯(ðºâq).
 // qed.
 
-lemma height_L_sn (q): â§£q = â§£(ðâq).
+lemma height_L_sn (q): â¯q = â¯(ðâq).
 // qed.
 
-lemma height_A_sn (q): â§£q = â§£(ðâq).
+lemma height_A_sn (q): â¯q = â¯(ðâq).
 // qed.
 
-lemma height_S_sn (q): â§£q = â§£(ð¦âq).
+lemma height_S_sn (q): â¯q = â¯(ð¦âq).
 // qed.
 
 (* Main constructions *******************************************************)
 
 theorem height_append (p1) (p2):
-        (â§£p2+â§£p1) = â§£(p1âp2).
+        (â¯p2+â¯p1) = â¯(p1âp2).
 #p1 elim p1 -p1 //
 * [ #n ] #p1 #IH #p2 <list_append_lcons_sn
 [ <height_d_sn <height_d_sn //
@@ -72,21 +72,21 @@ qed.
 (* Constructions with list_rcons ********************************************)
 
 lemma height_d_dx (p) (n):
-      (â§£p)+(ninj n) = â§£(pâð±n).
+      (â¯p)+(ninj n) = â¯(pâð±n).
 // qed.
 
 lemma height_m_dx (p):
-      (â§£p) = â§£(pâðº).
+      (â¯p) = â¯(pâðº).
 // qed.
 
 lemma height_L_dx (p):
-      (â§£p) = â§£(pâð).
+      (â¯p) = â¯(pâð).
 // qed.
 
 lemma height_A_dx (p):
-      (â§£p) = â§£(pâð).
+      (â¯p) = â¯(pâð).
 // qed.
 
 lemma height_S_dx (p):
-      (â§£p) = â§£(pâð¦).
+      (â¯p) = â¯(pâð¦).
 // qed.