> you can write an inductive proof that x^2 * (x^2 - 1) is divisible by 4 for all x
my friend you should either read the article more closely or think harder. he's not proving that the recurrence relation is correct (that would be meaningless - a recurrence relation is just given), he's proving that DP/memoization computes the same values as the recurrence relation.
the obvious indicator is that no property of any numbers is checked here - just that one function agrees with another:
theorem maxDollars_spec_correct : ∀ n, maxDollars n = maxDollars_spec n
this is the part that's undecidable (i should've said that instead of "impossible")
my friend you should either read the article more closely or think harder. he's not proving that the recurrence relation is correct (that would be meaningless - a recurrence relation is just given), he's proving that DP/memoization computes the same values as the recurrence relation.
the obvious indicator is that no property of any numbers is checked here - just that one function agrees with another:
this is the part that's undecidable (i should've said that instead of "impossible")https://en.wikipedia.org/wiki/Richardson%27s_theorem