The 91 function was introduced in papers published by Zohar Manna, Amir Pnueli and John McCarthy in 1970.
These papers represented early developments towards the application of formal methods to program verification.
As the field of Formal Methods advanced, this example appeared repeatedly in the research literature.
It is easier to reason about tail-recursive control flow, this is an equivalent (extensionally equal) definition: As one of the examples used to demonstrate such reasoning, Manna's book includes a tail-recursive algorithm equivalent to the nested-recursive 91 function.
Many of the papers that report an "automated verification" (or termination proof) of the 91 function only handle the tail-recursive version.
For the downward induction step, let n ≤ 89 and assume M(i) = 91 for all n < i ≤ 100, then This proves M(n) = 91 for all n ≤ 100, including negative values.
[1] John Cowles developed a formal proof that Knuth's generalized function was total, using the ACL2 theorem prover.