| Quellcodebibliothek Statistik Leitseite 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.pvsSprache: 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 % ------- % 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.10 Sekunden (vorverarbeitet am 2026-06-15) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09