1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/arith/nat_succ_iter.ma".
16 include "static_2/notation/functions/uparrowstar_2_0.ma".
17 include "static_2/syntax/sh.ma".
19 (* SORT HIERARCHY ***********************************************************)
21 definition sh_nexts (h) (n): nat → nat ≝ ⇡[h]^n.
24 "iterated next sort (sort hierarchy)"
25 'UpArrowStar_2_0 h n = (sh_nexts h n).
27 (* Basic constructions *)
29 lemma sh_nexts_zero (h): ∀s. s = ⇡*[h,𝟎]s.
32 lemma sh_nexts_unit (h): ⇡[h] ≐ ⇡*[h,𝟏].
35 lemma sh_nexts_succ (h) (n): ⇡[h] ∘ (⇡*[h,n]) ≐ ⇡*[h,↑n].
36 /2 width=1 by niter_succ/ qed.
38 (* Advanced constructions ****************************)
40 lemma sh_nexts_swap (h) (n): ⇡[h] ∘ (⇡*[h,n]) ≐ ⇡*[h,n] ∘ ⇡[h].
41 /2 width=1 by niter_appl/ qed.
43 (* Helper constructions *****************************************************)
45 lemma sh_nexts_succ_next (h) (n): ⇡*[h,n] ∘ (⇡[h]) ≐ ⇡*[h,↑n].