Nach dem Mausklick ist die Projektion eines vierdimensionalen Würfels zu sehen csequence_generate_limit.pvs
Sprache: PVS
%----------------------------------------------------------------------------- % Functions that generate sequences until a limit condition is met. % % 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_generate_limit[T: TYPE]: THEORY BEGIN
t, u: VAR T
p: VAR pred[T]
f: VAR [T -> T]
n: VAR nat
stop?: VAR pred[T]
state: VAR [[T -> T], T, pred[T]]
% The sequence generated from a generator function, a starting element, and % a predicate that determines when the next T should not appear in the % sequence.
generate_limit_struct(state): csequence_struct = IF state`3(state`2) THEN inj_empty_cseq ELSE inj_add(state`2, (state`1, state`1(state`2), state`3)) ENDIF
% This lemma is helpful in proving the next theorem
generate_has_length: LEMMA FORALL f, t, stop?, n:
has_length(generate(f, t, stop?), n) IFF
(stop?(iterate(f, n)(t)) AND
(FORALL (m: below[n]): NOT stop?(iterate(f, m)(t))))
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
