/* * Characterization of sequences. */ MACHINE FunSeq ASSERTIONS !(nn, ss, ff) . (nn : NATURAL & ss <: INTEGER & ff : 1..nn --> ss => ff : seq(ss)) ; !(nn, ss, ff) . (nn : NATURAL & ss <: INTEGER & ff : 1..nn >-> ss => ff : iseq(ss)) ; !(nn, ss, ff) . (nn : NATURAL & ss <: INTEGER & ff : 1..nn >->> ss => ff : perm(ss)) END