%-----------------------------------------------------------------------------
% The first index in a sequence of countable length where a predicate p holds.
%
% 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_first_p[T: TYPE]: THEORY
BEGIN
IMPORTING csequence_nth[T]
p: VAR pred[T]
cseq: VAR csequence
% The indexes of a sequence where the elements satisfy p
p_indexes(cseq, p): set[indexes(cseq)] =
{i: indexes(cseq) | p(nth(cseq, i))}
p_indexes_nonempty: LEMMA
FORALL cseq, p: some(p)(cseq) IFF nonempty?(p_indexes(cseq, p))
% The first element of a sequence satisfying p
first_p(p, (cseq: (csequence_codt[T].some(p)))): indexes(cseq) =
min(p_indexes(cseq, p))
first_p_nth: LEMMA
FORALL cseq, p: some(p)(cseq) IMPLIES p(nth(cseq, first_p(p, cseq)))
first_p_rest: LEMMA
FORALL cseq, p:
some(p)(cseq) IMPLIES
first_p(p, cseq) =
IF p(first(cseq)) THEN 0 ELSE first_p(p, rest(cseq)) + 1 ENDIF
END csequence_first_p
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.15Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
