SSL csequence_insert_remove.pvs   Sprache: PVS

%-----------------------------------------------------------------------------
% The interaction between the insert and remove operations on a 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_insert_remove[T: TYPE]: THEORY
 BEGIN

  IMPORTING csequence_insert[T], csequence_remove[T]

  insert_remove_eta: THEOREM
    FORALL (cseq: csequence), (n: indexes(cseq)):
      insert(nth(cseq, n), n, remove(cseq, n)) = cseq

 END csequence_insert_remove