|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
comDefinition.ml
Sprache: PVS
Original von: PVS©
|
|
% every nonempty set of nats has a least element.
% This also holds for any subtype T of the integers.
%
% Author: Jerry James ([email protected]), 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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
