|
|
|---|
|
|
|
|---|
A monotonicity property of execution limits.
If the execution of a construct with a certain limit does not return an error (for exhausting the limit or other reason), neither does the execution of the same construct with a larger limit (and with the same computation state and function environment of course), and in addition it returns the same non-error outcome. This is a form of monotonicity, which maps the numeric order of limit to a (non-explicated) ordering of error vs. non-error outcomes.
This is proved by induction, but since there are two limits involved, the induction schema of the execution functions does not work here. We need one that involves two limits, tested and decremented ``in parallel'', in the same way as the execution functions do for one limit. Since some of the recursive calls of the execution functions take as arguments results of previous recursive calls, the induction schema with two limits needs to return the same results as the execution functions. So we define the mutually recursive clique exec-2limits to be exactly like the mutually recursive clique exec but with two limits, handled in parallel, instead of one.
Using the induction scheme defined by exec-2limits, we prove our desired theorems. But first, we need to prove that the execution functions with two limits return the same results as the normal execution functions, when one limits is the same as or larger than the other. This is because, in the proofs of our desired theorems, calls of the exec-2limits functions show up in subgoals, and thus we need to rewrite them away, to calls of the regular execution functions.