Quelle  csequence_prefix_append.pvs   Sprache: PVS

%-----------------------------------------------------------------------------
% Prefix of an appended sequence 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_prefix_append[T: TYPE]: THEORY
 BEGIN

  IMPORTING csequence_prefix[T], csequence_append[T]

  prefix_append_eta: THEOREM
    FORALL (fseq: finite_csequence), (t: T):
      prefix(append(t, fseq), length(fseq)) = fseq

 END csequence_prefix_append