Impressum bounded_nats.pvs  Sprache: unbekannt

% every nonempty set of nats has a least element.
% This also holds for any subtype T of the integers.
%
% Author: Jerry James (jamesj@acm.org), University of Kansas
% Date: 13 Jan 2005

bounded_nats[T: TYPE FROM nat]: THEORY

BEGIN

  IMPORTING bounded_integers[T]

  every_nonempty_set_has_least: JUDGEMENT
    (nonempty?[T]) SUBTYPE_OF (has_least?(<=))

END bounded_nats