McCarthy 91 Function / McCarthy 91 函数

English

The McCarthy 91 function is defined recursively by

mc91(n) = n - 10                 when n > 100
mc91(n) = mc91(mc91(n + 11))     when 0 <= n <= 100

For every nonnegative integer input, prove that the supplied implementation returns n - 10 when n > 100, and returns 91 otherwise.

The implementation and contract are fixed. Add proof code only inside starter.c; changing the implementation or specification is rejected by the judge and consumes an attempt.

中文

McCarthy 91 函数递归定义如下：

mc91(n) = n - 10                 当 n > 100 时
mc91(n) = mc91(mc91(n + 11))     当 0 <= n <= 100 时

请证明：对于任意非负整数输入，当 n > 100 时，给定实现返回 n - 10；否则返回 91。

实现和契约均为固定内容。你只能在 starter.c 中添加证明代码；修改实现或规约将被判定为失败，并消耗一次提交机会。