| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle infinite_sets.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % Cardinality properties of infinite sets. % % For PVS version 3.2. February 10, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % prelude: finite_sets[T], infinite_sets_def[T] % sets_aux: card_comp_set[nat,T], card_comp_set[T,nat], card_comp_set[T,T], % card_comp_set_props[T,nat], card_comp_set_props[T,T], % card_sets_lemmas[T], card_single[T], countable_props[T], % countability[T], infinite_sets[T] % %------------------------------------------------------------------------- infinite_sets[T: TYPE]: THEORY BEGIN IMPORTING countable_props[T], card_sets_lemmas[T] t: VAR T S, R: VAR set[T] Fin: VAR finite_set[T] Inf: VAR infinite_set[T] infinite_add_card: THEOREM FORALL Inf, t: card_eq(Inf, add(t, Inf)) infinite_remove_card: THEOREM FORALL Inf, t: card_eq(Inf, remove(t, Inf)) finite_infinite_lt: THEOREM FORALL S: (FORALL Fin: card_lt(Fin, S)) IFF is_infinite(S) END infinite_sets ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28