Quelle  top.pvs   Sprache: PVS

%-----------------------------------------------------------------------------
% Sequences of countable length defined as coalgebraic datatypes.
%
% Author: Jerry James <loganjerry@gmail.com>
%
% This file and its accompanying proof file are distributed under the CC0 1.0
% Universal license: http://creativecommons.org/publicdomain/zero/1.0/.
%
% Version history:
%   2007 Feb 14: PVS 4.0 version
%   2011 May  6: PVS 5.0 version
%   2013 Jan 11: PVS 6.0 version
%-----------------------------------------------------------------------------
top: THEORY
 BEGIN

  IMPORTING
   ascending_chains,              % Monotonically nondecreasing prefixes
   csequence,                     % Basic definitions
   csequence_add,                 % Properties of the add operator
   csequence_append,              % Append an element to a csequence
   csequence_concatenate,         % The o operator for csequences
   csequence_concatenate_extract, % Eta rule for o and ^
   csequence_constant,            % A single repeated element
   csequence_extract,             % The ^ operator for csequences
   csequence_filter,              % Filter with a predicate
   csequence_filter_map,          % Conjunction of filter and map
   csequence_filter_of,           % Whether one seq is the filter of another
   csequence_finseq,              % Conversions to/from finseq
   csequence_first_p,             % The first element satisfying predicate p
   csequence_flatten,             % Sequence of sequences -> sequence
   csequence_generate,            % Sequences made from generator functions
   csequence_generate_limit,      % Ditto with a limit predicate
   csequence_induction,           % More induction rules for csequences
   csequence_insert,              % Insert an element into a csequence
   csequence_insert_remove,       % Eta rule for insert and remove
   csequence_length,              % Compute the length of a csequence
   csequence_length_comp,         % Length comparisons for all csequences
   csequence_limit,               % The limit of an ascending chain
   csequence_list,                % Conversions to/from list
   csequence_map_composition,     % Composed maps on csequences
   csequence_map_props,           % Properties of the map operator
   csequence_merge,               % Element-by-element merge of 2 csequences
   csequence_merge_split,         % Eta rules for merge and split
   csequence_nth,                 % Find the nth element of a csequence
   csequence_prefix,              % Prefixes of csequences
   csequence_prefix_append,       % Eta rule for prefix and append
   csequence_prefix_suffix,       % Eta rule for prefix and suffix
   csequence_props,               % Basic properties of csequences
   csequence_remove,              % Remove an element from a csequence
   csequence_rest,                % Properties of the rest operator
   csequence_reverse,             % Reverse a finite csequence
   csequence_sequence,            % Conversions to/from sequence
   csequence_singleton,           % Csequences with exactly one element
   csequence_split,               % Split a csequence into two csequences
   csequence_strict_prefix,       % Well-ordered prefixes of a given csequence
   csequence_subsequence,         % Subsequence definition and properties
   csequence_suffix,              % Suffixes of csequences
   csequence_unzip,               % Csequence of pairs to pair of csequences
   csequence_zip,                 % Pair of csequences to csequence of pairs
   csequence_zip_unzip            % Eta rules for zip and unzip

 END top