------------------------------------------------------------------------
Number theory library
---------------------
div nt -- division theory defined for efficiency in PVS
div nt alt -- div defined recursively
mod nt -- mod function
divisibility -- defines divides, lcm
gcd -- defines greatest common divisor
primes -- prime factorization
unique factorization -- prime factorization is unique
infinite primes -- set of primes has infinite cardinality
Note:
Theories div_nt and div_nat should not be imported at the same
time. This is also true for mod_nt and mod_nat.
Author:
Ricky W. Butler email: *.*.******@****.****.***
Mail Stop 130 fax : (804) 864-xxxx
NASA Langley Research Center phone: (804) 864-xxxx
Hampton, Virginia 23681-0001
12/11/01 Changed name "sort" to "psort" in "product_perm_lems"
to get around bug
------------------------------------------------------------------------