Functions used to prove admissibility.

This theory contains the DEFUN-THEORY (see :DOC DEFUN-THEORY) of all functions (except those in (THEORY BUILT-INS)) that are necessary to prove the admissibility of recursive functions in most cases. Note that this theory is probably useless without the theory BUILT-INS and some simple theory of arithmetic (such as the theory ALGEBRA from the book "math-lemmas".

For functions that recur on the length of a string you may have to ENABLE LENGTH and LEN, as we steadfastly refuse to allow ANY globally enabled recursive functions.