An Automatic Induction Proof for

The termination problem is in general undecidable, however, termination can be proved for specific classes of programs. This work describes an automatic method that tests for termination of modulo-case functions by conducting a mathematical induction proof. The system takes a modulo-case function and builds an execution trace tree from its inverse. Based on the execution trace tree, a linear polynomial is formed in order to capture the level of the executed trace tree for which the termination problem holds. Using the cases of the original function, an inductive proof is performed and compared to the coefficient of the polynomial. If the completed proof is found to be within the polynomial’s coefficient then termination has been proved, else a larger polynomial needs to be found and tested. If a function successfully terminates, its runtime is generated based on the same polynomial