%-----------------------------------------------------------------------------
% The interaction between the insert and remove operations on a sequence 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_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
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
