Not if that language doesn't actually check the totality of your proof and ensures that the base case holds.
1. build a table tab[n]
2. check that for every i, tab[i] == maxDollars_spec[i]
if you take the latter approach i proposed (bottom up) there is nothing to check the totality of.