|
%------------------------------------------------------------------------
%
% max_array_def: foundation for max_array
% ---------------------------------------
%
% Author: Ricky W. Butler
%
% This theory provides a constructive definition of max (named Imax) to
% provide a means to discharge the TCC produced in max_array. This
% theory is not intended to be directly used.
%
%------------------------------------------------------------------------
max_array_def[N: nat, T: TYPE, <= : (total_order?[T]) ]: THEORY
BEGIN
A,A1,A2: VAR ARRAY[below(N) -> T]
t, t1, t2: VAR T
ii,jj,j: VAR below(N)
amax(A,ii,jj): below(N) = IF A(ii) <= A(jj) THEN jj ELSE ii ENDIF
imax_rec(A,ii,jj): RECURSIVE below(N) =
IF jj <= ii THEN ii
ELSE amax(A,jj,imax_rec(A,ii,jj-1))
ENDIF MEASURE (LAMBDA A,ii,jj: jj)
imax_rec_lem: LEMMA ii <= j AND j <= jj IMPLIES
A(j) <= A(imax_rec(A,ii,jj))
imax_rec_rng: LEMMA ii <= jj IMPLIES ii <= imax_rec(A,ii,jj) AND
imax_rec(A,ii,jj) <= jj
abv(ii): TYPE = {i: nat | ii <= i AND i < N}
Imax_rec(A,ii,(jj: abv(ii))): subrange(ii,jj) =
imax_rec(A,ii,jj)
Imax(A,ii,(jj: abv(ii))): {i: subrange(ii,jj) |
(FORALL j: ii <= j AND j <= jj
IMPLIES A(j) <= A(i))}
Imax_1: LEMMA Imax(A,ii,ii) = ii
END max_array_def
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
