Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/PVS/sets_aux/ (PVS Prover Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 734 B

Quelle card_power_set.pvs

Sprache: PVS

%-------------------------------------------------------------------------
%
%  The cardinality of a set is always less than the cardinality of its
%  power set.
%
%  For PVS version 3.2.  November 4, 2004
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  sets_aux: card_comp_set[set[T],T], card_comp_set[T,set[T]],
%    card_comp_set_props[T,set[T]], card_power_set[T]
%
%-------------------------------------------------------------------------
card_power_set[T: TYPE]: THEORY
BEGIN

  IMPORTING card_comp_set_props[T, set[T]]

  card_power: THEOREM FORALL (S: set[T]): card_lt(S, powerset(S))

END card_power_set