|
%------------------------------------------------------------------------
%
% min_array_def: foundation for min_array
% ---------------------------------------
%
% Author: Ricky W. Butler
%
% This theory provides a constructive definition of min (named Imin) to
% provide a means to discharge the TCC produced in min_array. This
% theory is not intended to be directly used.
%
%------------------------------------------------------------------------
min_array_def[N: nat, T: TYPE, <= : (total_order?[T]) ]: THEORY
EXPORTING ALL BUT >=, ge_total, % i.e. DO NOT export max_array stuff
IMP_max_array_def_TCC1 % because max is alias for min
BEGIN
IMPORTING below_arrays[N,T]
A,A1,A2: VAR ARRAY[below(N) -> T]
x, t1, t2: VAR T
ii,jj,j: VAR below(N)
n: VAR {p: posnat | p <= N}
>=(t1,t2): bool = t2 <= t1
ge_total: LEMMA total_order?[T](>=)
IMPORTING max_array_def[N,T,>=]
abv(ii): TYPE = {i: nat | ii <= i AND i < N}
Imin(A,ii,(jj: abv(ii))): {i: subrange(ii,jj) |
(FORALL j: ii <= j AND j <= jj
IMPLIES A(i) <= A(j))}
Imin_1: LEMMA Imin(A,ii,ii) = ii
END min_array_def
¤ Dauer der Verarbeitung: 0.13 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.
|
