%-----------------------------------------------------------------------------
% Composition of mapping functions on sequences of countable length.
%
% Author: Jerry James <loganjerry@gmail.com>
%
% 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
