]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_depth.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "delayed_updating/syntax/path.ma".
16 include "ground/notation/functions/verticalbars_1.ma".
17
18 (* DEPTH FOR PATH ***********************************************************)
19
20 rec definition depth (p) on p: pnat ā‰
21 match p with
22 [ list_empty     ā‡’ šŸ
23 | list_lcons l q ā‡’
24   match l with
25   [ label_d _ ā‡’ depth q
26   | label_m   ā‡’ depth q
27   | label_L   ā‡’ ā†‘(depth q)
28   | label_A   ā‡’ depth q
29   | label_S   ā‡’ depth q
30   ]
31 ].
32
33 interpretation
34   "depth (path)"
35   'VerticalBars p = (depth p).
36
37 (* Basic constructions ******************************************************)
38
39 lemma depth_empty: šŸ = ā˜šžā˜.
40 // qed.
41
42 lemma depth_d (q) (n): ā˜qā˜ = ā˜š—±nā——qā˜.
43 // qed.
44
45 lemma depth_m (q): ā˜qā˜ = ā˜š—ŗā——qā˜.
46 // qed.
47
48 lemma depth_L (q): ā†‘ā˜qā˜ = ā˜š—Ÿā——qā˜.
49 // qed.
50
51 lemma depth_A (q): ā˜qā˜ = ā˜š—”ā——qā˜.
52 // qed.
53
54 lemma depth_S (q): ā˜qā˜ = ā˜š—¦ā——qā˜.
55 // qed.