| products/sources/formale Sprachen/PVS/co_structures/ (Office von Apache Version 25.8.3.2©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle csequence_first_p.pvs Sprache: PVS |
|||||||||
|
%-----------------------------------------------------------------------------
% 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))} 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 ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28