This proof is done in NASA PVS and more or less follows the proofs listed below. This proof was done for the class programming verification at University of Applied Sciences Leipzig.
- Ackermann Function – George Tourlakis
- Ackermann function is not primitive recursive
- Termination Lecture 3 - Bigger& Bigger – Jonathan Kalechstain
- A Machine Checked Proof that Ackermann's Function is not Primitive Recursive – Nora Szasz
You can run the whole proof with the proveit_gh script. Make sure to change the PVSPATH to point to your installation of PVS. To run the proofs run the following command:
./proveit_gh -c pr-ack