Recursion invariant

A relationship between a recursive procedure's arguments, accumulated state and original input that holds at every reachable recursive call. For accumulator-based exponentiation by squaring, $accbas{e}^{remaining}=x^n$ is a recursion invariant under exact arithmetic. The base case converts it into the desired result, while the recursive step and a decreasing argument justify preservation and termination.