%-----------------------------------------------------------------------------
% Composition of mapping functions 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_map_composition[T1, T2, T3: TYPE]: THEORY
BEGIN
IMPORTING csequence_codt_map[T1, T2]
IMPORTING csequence_codt_map[T1, T3]
IMPORTING csequence_codt_map[T2, T3]
map_composition: THEOREM
FORALL (f12: [T1 -> T2]), (f23: [T2 -> T3]), (cseq: csequence[T1]):
map[T2, T3](f23)(map[T1, T2](f12)(cseq)) =
map[T1, T3](f23 o f12)(cseq)
END csequence_map_composition
¤ Dauer der Verarbeitung: 0.10 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.
|
