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):
33 lemma sh_nexts_unit (h):
37 lemma sh_nexts_succ (h) (n):
38 ∀s. ⇡[h](⇡*[h,n]s) = ⇡*[h,↑n]s.
39 #h #n #s @(niter_succ … (⇡[h]))
42 (* Advanced constructions ****************************)
44 lemma sh_nexts_swap (h) (n):
45 ∀s. ⇡[h](⇡*[h,n]s) = ⇡*[h,n](⇡[h]s).
46 #h #n #s @(niter_appl … (⇡[h]))
49 (* Helper constructions *****************************************************)
51 lemma sh_nexts_succ_next (h) (n):
52 ∀s. ⇡*[h,n](⇡[h]s) = ⇡*[h,↑n]s.