| products/sources/formale sprachen/PVS/co_structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: top.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
%-----------------------------------------------------------------------------
% Sequences of countable length defined as coalgebraic datatypes. % % Author: Jerry James <[email protected]> % % 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 ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
