## Top File of PVS sets_aux Library

```
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     SRI International
%      Jerry James           University of Kansas
%      David Lester    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
```
The tag identifies links that are outside the NASA domain