%------------------------------------------------------------------------- % % 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 % ------- % prelude: functions[set[T],T], functions[T,set[T]] % sets_aux: card_comp[set[T],T], card_comp[T,set[T]], % card_comp_props[T,set[T]], card_power[T] % %-------------------------------------------------------------------------
card_power[T: TYPE]: THEORY BEGIN
IMPORTING card_comp_props[T, set[T]]
card_power: THEOREM card_lt[T, set[T]]
END card_power
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
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.
