%
%
% Purpose: results to get rid of is_finite TCCs
%
% Author: Alfons Geser ([email protected]), 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
¤ Dauer der Verarbeitung: 0.24 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.
|
