Quelle finite_sets_below_extra.pvs Sprache: PVS

%
%
% Purpose: results to get rid of is_finite TCCs
%
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
%

finite_sets_below_extra[N: nat]: THEORY

BEGIN

  IMPORTING finite_sets@finite_sets_below[N]

  below_is_finite_type: LEMMA is_finite_type[below(N)]

  set_below_is_finite: JUDGEMENT set[below(N)] SUBTYPE_OF finite_set[below(N)]

END finite_sets_below_extra

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.