fseqs_aux_vertical[vsmin,vsmax:real] : THEORY
BEGIN

  IMPORTING structures@sort_fseq[real,<=],
     structures@fseqs_ops[real],
            trig_fnd@to2pi

  vs,fs   : VAR fseq


  %%%%% Vertical Speed %%%%%

  vs_fseq?(vs): bool =
    FORALL (i:below(vs`length)): vsmin<=vs`seq(i) AND vs`seq(i)<=vsmax

  vsb,vsb1,vsb2 : VAR (vs_fseq?)

  empty_vs_fseq : JUDGEMENT
    emptyseq HAS_TYPE (vs_fseq?)

  comp_vs_fseq : JUDGEMENT
    o(vsb1,vsb2) HAS_TYPE (vs_fseq?)

  sort_vs_fseq : JUDGEMENT
    sort(vsb) HAS_TYPE (vs_fseq?)

END fseqs_aux_vertical