| 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 3 kB |
|
SSL top.pvs Sprache: PVS |
|||||||||
|
top: THEORY
%---------------------------------------------------------------------------- % % Additional Set Theory (sets_aux) % -------------------------------- % % Version 1.0 Powersets merged with finite_sets_aux 2/10/04 % Version 2.0 Jerry James libraries added 5/5/04 % Version 2.1 Updates for PVS 3.2; removed theories 11/3/04 % now in the prelude or finite_sets % Version 3.0 Merged in Alfons Geser's order theories 2/10/05 % Version 3.1 Added some theories from David Lester 4/12/05 % Version 3.2 Added cardinal and sets_lemmas_extra 5/11/05 % Version 3.3 Updated countable sets theories 9/15/09 % % Authors: % Bruno Dutertre <bruno@sdl.sri.com> SRI International % Jerry James <jamesj@acm.org> University of Kansas % David Lester <dlester@cs.man.ac.uk> Manchester University %---------------------------------------------------------------------------- BEGIN %---- Bruno Dutertre theories on powersets IMPORTING fun_below_props, % bijections with Cartesian products power_sets, % cardinality and finiteness set_of_functions % functions from finite set A to B %---- Jerry James theories on infinite cardinalities IMPORTING bits, % sets of bit numbers (used to show countability) card_comp, % compare the cardinality of any two types card_comp_props, % properties of the card_comp predicates card_comp_set, % compare the cardinality of any two sets card_comp_set_props, % properties of the card_comp_set predicates card_comp_set_transitive, % transitivity of the card_comp_set predicates card_comp_transitive, % transitivity of the card_comp predicates card_finite, % card_comp vs. card(S) from finite_sets card_power, % card[T] < card[set[T]] card_power_set, % card(S) < card(powerset(S)) card_sets_lemmas, % relationships of set operations to cardinality card_single, % single type properties of card_comp_set preds card_function, % surjection/injection image properties cardinal, % cardinality(S) for any set S countability, % definition of (un)countable sets countable_image, % countable image countable_props, % properties of (un)countable sets countable_set, % some countable sets of numbers (e.g., integers) countable_setofsets, % operations on countable families of sets countable_types, % countability of some prelude types infinite_card, % card_comp implications for finiteness infinite_image, % infinite images of a set under some function infinite_sets, % cardinality of infinite set add and remove sets_lemmas_extra % disjoint? is commutative %--- David Lester theories on infinite/countable sets IMPORTING countable_image, % image of a countable set is countable card_function, % finite/infinite properties of functions infinite_nat_def, % infinite IFF injective map from the naturals indexed_sets_aux, % Additional prelude indexed set lemmas countable_indexed_sets,% countable setsofsets vs indexed sets nat_indexed_sets, % increasing/decresing indexed sets inverse_image_Union, % inverse_image(f,Union(X)) countability_aux, %% RWB cantor_bernstein_schroeder %% Proved by Anthony Narkawicz IMPORTING % Dragan Stosic's relational and functional choice facts based on Axiom of Choice top_choice_facts, % Dragan Stosic's refinement relations top_refinement_relations END top ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28