%-----------------------------------------------------------------------------
% The combination of the zip and unzip 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_zip_unzip[T1, T2: TYPE]: THEORY
BEGIN
IMPORTING csequence_unzip[T1, T2], csequence_zip[T1, T2]
cseq: VAR csequence[[T1, T2]]
cseq1: VAR csequence[T1]
cseq2: VAR csequence[T2]
zip_unzip_eta: THEOREM FORALL cseq: zip(unzip(cseq)) = cseq
unzip_zip_eta: THEOREM
FORALL cseq1, cseq2:
length_eq(cseq1, cseq2) IMPLIES
unzip(zip(cseq1, cseq2)) = (cseq1, cseq2)
END csequence_zip_unzip
¤ Dauer der Verarbeitung: 0.3 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.
|
