Details About PVS Structures Library

  IMPORTING           	% -------------- arrays -----------------
     top_array,
     min_array,       	% defines min function over an array
     max_array,       	% defines max function over an array 
     permutations,    	% permutations defined using arrays
     sort_array,      	% defines a sort function over arrays
     sort_array_lems, 	% relationship between sort and min and max
     array_ops,       	% array operations
     majority_array,  	% defines majority function over an array 

                      	% -------------- sequences -----------------
     top_seq,
     max_seq,         	% defines max function over an sequence 
     min_seq,         	% defines min function over a sequence
     permutations_seq,	% permutations defined using arrays
     majority_seq,    	% defines majority function over finite sequences
     bubblesort,      	% bubble sort correctness theorem
     sort_seq,        	% defines a sort function over sequences
     sort_seq_lems,   	% relationship between sort and min and max
     seq2set,          	% convert sequence to a set

                      	% -------------- bags -----------------
     top_bags,        
     bags,            	% fundamental definitions and properties
     bags_aux,        	% definition of filter, rest, and choose 
     bags_to_sets,    	% converts bags to sets
     finite_bags_lems,	% basic definitions and lemmas 
     finite_bags_aux, 	% lemmas need induction 
     finite_bags_inductions % induction schemes