Quelle  top_seq.pvs   Sprache: PVS

top_seq: THEORY
BEGIN
   IMPORTING
     seqs, 
     max_seq,          % defines max function over an sequence 
     min_seq,          % defines min function over a sequence
     permutations_seq, % permutations defined using arrays
     majority_seq,     % defines majority function over finite sequences
     bubblesort,       % bubble sort correctness theorem
     sort_seq,         % defines a sort function over sequences
     sort_seq_lems,    % relationship between sort and min and max
     set2seq,           % convert set to sequence
     seq2set,           % convert sequence to a set
     seq_extras,        % extra-definitions that complements the prelude's finite sequences
     seq_pigeon         % Pigeon hole principle for the prelude's finite sequences

END top_seq