%-----------------------------------------------------------------------------
% Prefixes and suffixes of sequences of countable length.
%
% 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 14: PVS 6.0 version
%-----------------------------------------------------------------------------
csequence_prefix_suffix[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_prefix[T], csequence_suffix[T]
n: VAR nat
cseq, cseq1, cseq2: VAR csequence
prefix_suffix_eta: THEOREM
FORALL cseq, n: prefix(cseq, n) o suffix(cseq, n) = cseq
prefix_suffix_extensionality: THEOREM
FORALL cseq1, cseq2, n:
prefix(cseq1, n) = prefix(cseq2, n) AND
suffix(cseq1, n) = suffix(cseq2, n)
IMPLIES cseq1 = cseq2
END csequence_prefix_suffix
¤ Dauer der Verarbeitung: 0.0 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.
|
