FDL > PVS > Prelude : Collection

 The PVS prelude.
 The prelude consists of theories that are built in to the PVS system.
 It is typechecked the same as any other PVS theory, but there are hooks
 in the typechecker that require most of these theories to be available,
 hence the order of the theories is important.  For example, no formulas
 may be declared before the booleans are available, as the formula is
 expected to have type bool.  Since definitions implicitly involve both
 formulas and equality, the booleans theory may not include any
 definitions.  Formulas are given below as AXIOMs, POSTULATEs, and LEMMAs.
 POSTULATEs are formulas that can be proved using the decision procedures,
 but would have to be given as axioms in a pure development of the theory.
 AXIOMs are formulas that cannot be proved, and LEMMAS are formulas that
 have been proved.

booleans	measure induction	real defs	lex2
equalities	epsilons	real props	list adt
if def	sets	rational props	list adt map
boolean props	sets lemmas	integer props	list adt reduce
xor def	function inverse	floor ceil	list props
quantifier props	function image	exponentiation	map props
defined types	function props	euclidean division	filters
exists1	function props alt	divides	list2finseq
equality props	function props2	modulo arithmetic	list2set
if props	relation defs	subrange inductions	disjointness
functions	relation props	bounded int inductions	character adt
functions alt	relation props2	bounded nat inductions	strings
restrict	operator defs	subrange type	lift adt
extend	numbers	int types	lift adt map
extend bool	reals	nat types	lift adt reduce
K conversion	real axioms	finite sets def	union adt
K props	bounded real defs	function iterate	union adt map
identity	bounded real defs alt	sequences	union adt reduce
identity props	real types	seq functions	mucalculus
relations	rationals	finite sequences	ctlops
orders	integers	ordstruct adt	fairctlops
orders alt	naturalnumbers	ordstruct adt reduce	Fairctlops
wf induction	min nat	ordinals