%----------------------------------------------------------------------------- % The first index in a sequence of countable length where a predicate p holds. % % 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_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))}
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
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.13Bemerkung:
(vorverarbeitet)
¤
