definition sh_N: sh ≝ mk_sh S ….
// defined.

axiom nexts_dec: ∀h,s1,s2. Decidable (∃n. (next h)^n s1 = s2).

axiom nexts_inj: ∀h,s,n1,n2. (next h)^n1 s = (next h)^n2 s → n1 = n2.