Proof – Ackermann is not primitive recursive

This proof performed in NASA PVS was done for the class programming verification.