%----------------------------------------------------------------------------
% Lee Pike
% [email protected]
% Formal Methods Group, NASA Langley Research Center
%
% PVS Version 3.1
%
% PURPOSE:
% Define the minimum and maximum for ordered finite bags.
%----------------------------------------------------------------------------
finite_bags_minmax[T: NONEMPTY_TYPE,
leq: (total_order?[T])]: THEORY
BEGIN
IMPORTING
finite_bags[T],
finite_sets@finite_sets_minmax[T, leq],
finite_bags_inductions[T]
D : VAR nonempty_finite_bag
max(D) : T = max(bag_to_set(D))
min(D) : T = min(bag_to_set(D))
max_member : LEMMA member(max(D), D)
min_member : LEMMA member(min(D), D)
END finite_bags_minmax
¤ Dauer der Verarbeitung: 0.209 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.
|
