%-----------------------------------------------------------------------------
% Eta rule for use with the concatenate and extract operators on 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_concatenate_extract[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_concatenate[T], csequence_extract[T]
i, j, k: VAR nat
fseq: VAR finite_csequence
o_extract: THEOREM
FORALL fseq, i, j, k:
i <= j AND j <= k IMPLIES
(fseq ^ (i, j)) o (fseq ^ (j + 1, k)) = fseq ^ (i, k)
o_extract_eta: THEOREM
FORALL fseq, i, j:
i < j AND j >= length(fseq) - 1 IMPLIES
(fseq ^ (0, i)) o (fseq ^ (i + 1, j)) = fseq
END csequence_concatenate_extract
¤ Dauer der Verarbeitung: 0.19 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.
|
