update in delayed_updating

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

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 cdf24943af922c8a47c74990fb79e92acf803231..474bbcbda501f43dd5de91697dd321d58ca33c7f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/flat_1.ma".
 include "ground/arith/nat_plus.ma".
-include "ground/notation/functions/verticalbars_1.ma".
 
 (* DEPTH FOR PATH ***********************************************************)
 
@@ -33,32 +33,32 @@ match p with
 
 interpretation
   "depth (path)"
-  'VerticalBars p = (depth p).
+  'Flat p = (depth p).
 
 (* Basic constructions ******************************************************)
 
-lemma depth_empty: ð\9d\9f\8e = â\9d\98ð\9d\90\9eâ\9d\98.
+lemma depth_empty: ð\9d\9f\8e = â\99­ð\9d\90\9e.
 // qed.
 
-lemma depth_d_sn (q) (n): â\9d\98qâ\9d\98 = â\9d\98ð\9d\97±nâ\97\97qâ\9d\98.
+lemma depth_d_sn (q) (n): â\99­q = â\99­(ð\9d\97±nâ\97\97q).
 // qed.
 
-lemma depth_m_sn (q): â\9d\98qâ\9d\98 = â\9d\98ð\9d\97ºâ\97\97qâ\9d\98.
+lemma depth_m_sn (q): â\99­q = â\99­(ð\9d\97ºâ\97\97q).
 // qed.
 
-lemma depth_L_sn (q): â\86\91â\9d\98qâ\9d\98 = â\9d\98ð\9d\97\9fâ\97\97qâ\9d\98.
+lemma depth_L_sn (q): â\86\91â\99­q = â\99­(ð\9d\97\9fâ\97\97q).
 // qed.
 
-lemma depth_A_sn (q): â\9d\98qâ\9d\98 = â\9d\98ð\9d\97\94â\97\97qâ\9d\98.
+lemma depth_A_sn (q): â\99­q = â\99­(ð\9d\97\94â\97\97q).
 // qed.
 
-lemma depth_S_sn (q): â\9d\98qâ\9d\98 = â\9d\98ð\9d\97¦â\97\97qâ\9d\98.
+lemma depth_S_sn (q): â\99­q = â\99­(ð\9d\97¦â\97\97q).
 // qed.
 
 (* Main constructions *******************************************************)
 
 theorem depth_append (p1) (p2):
-        ❘p2❘+❘p1❘ = ❘p1●p2❘.
+        (♭p2)+(♭p1) = ♭(p1●p2).
 #p1 elim p1 -p1 //
 * [ #n ] #p1 #IH #p2 <list_append_lcons_sn
 [ <depth_d_sn <depth_d_sn //
@@ -72,21 +72,21 @@ qed.
 (* Constructions with list_rcons ********************************************)
 
 lemma depth_d_dx (p) (n):
-      â\9d\98pâ\9d\98 = â\9d\98pâ\97\96ð\9d\97±nâ\9d\98.
+      â\99­p = â\99­(pâ\97\96ð\9d\97±n).
 // qed.
 
 lemma depth_m_dx (p):
-      â\9d\98pâ\9d\98 = â\9d\98pâ\97\96ð\9d\97ºâ\9d\98.
+      â\99­p = â\99­(pâ\97\96ð\9d\97º).
 // qed.
 
 lemma depth_L_dx (p):
-      â\86\91â\9d\98pâ\9d\98 = â\9d\98pâ\97\96ð\9d\97\9fâ\9d\98.
+      â\86\91â\99­p = â\99­(pâ\97\96ð\9d\97\9f).
 // qed.
 
 lemma depth_A_dx (p):
-      â\9d\98pâ\9d\98 = â\9d\98pâ\97\96ð\9d\97\94â\9d\98.
+      â\99­p = â\99­(pâ\97\96ð\9d\97\94).
 // qed.
 
 lemma depth_S_dx (p):
-      â\9d\98pâ\9d\98 = â\9d\98pâ\97\96ð\9d\97¦â\9d\98.
+      â\99­p = â\99­(pâ\97\96ð\9d\97¦).
 // qed.