|
|
|---|
|
|
|
|---|
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.