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 "static_2/syntax/sh.ma".
17 (* SORT HIERARCHY ***********************************************************)
19 (* acyclicity condition *)
20 record sh_acyclic (h): Prop ≝
22 nexts_inj: ∀s,n1,n2. (next h)^n1 s = (next h)^n2 s → n1 = n2
25 (* decidability condition *)
26 record sh_decidable (h): Prop ≝
28 nexts_dec: ∀s1,s2. Decidable (∃n. (next h)^n s1 = s2)