%-----------------------------------------------------------------------------
% Properties of the rest function as applied to 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_rest[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_nth[T]
n: VAR nat
t: VAR T
p: VAR pred[T]
iseq: VAR infinite_csequence
nseq: VAR nonempty_csequence
nfseq: VAR nonempty_finite_csequence
rest_finite: JUDGEMENT rest(nfseq) HAS_TYPE finite_csequence
rest_infinite: JUDGEMENT rest(iseq) HAS_TYPE infinite_csequence
rest_empty_add: THEOREM
FORALL nseq:
empty?(rest(nseq)) IFF (EXISTS t: nseq = add(t, empty_cseq))
rest_empty: THEOREM
FORALL nseq: empty?(rest(nseq)) IFF is_finite(nseq) AND length(nseq) = 1
rest_nonempty: THEOREM
FORALL nseq:
nonempty?(rest(nseq)) IFF is_infinite(nseq) OR length(nseq) > 1
rest_first: THEOREM
FORALL nseq:
nonempty?(rest(nseq)) IMPLIES first(rest(nseq)) = nth(nseq, 1)
rest_length: THEOREM FORALL nfseq: length(rest(nfseq)) = length(nfseq) - 1
rest_index: THEOREM
FORALL nseq, n: index?(rest(nseq))(n) IFF index?(nseq)(n + 1)
rest_nth: THEOREM
FORALL nseq, (n: indexes(rest(nseq))):
nth(rest(nseq), n) = nth(nseq, n + 1)
rest_some: THEOREM
FORALL nseq, p: some(p)(nseq) IFF p(first(nseq)) OR some(p)(rest(nseq))
rest_every: THEOREM
FORALL nseq, p:
every(p)(nseq) IFF p(first(nseq)) AND every(p)(rest(nseq))
END csequence_rest
¤ 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.
|
