Invariante de tabela dinâmica sob inserção

[Enunciado do exercício.]  Queremos mostrar que no início de cada iteração (linha 25) a poupança tem pelo menos 2mt moedas.

Eis a prova.- A propriedade vale no início da primeira iteração pois nessa ocasião m = t = 1. Suponha agora que a propriedade vale no início de uma iteração qualquer. Há dois casos a considerar:

  1. Se m < t, a iteração custará 1 moeda. No fim da iteração, m terá aumentado em 1 unidade e t terá permanecido constante, donde o valor da expressão 2mt terá aumentado em 2 unidades. Por outro lado, a poupança de moedas terá aumentado em 3−1 = 2 unidades. Logo, no início da próxima iteração, continuaremos tendo pelo menos 2mt moedas na poupança.
  2. Se m = t, a iteração começará com pelo menos 2mt = m moedas na poupança e custará m+1 moedas. Como a poupança ganha 3 novas moedas, teremos pelo menos 2 moedas na poupança no fim da iteração. Por outro lado, no fim da iteração, t estará valendo o dobro do valor original de m e m terá aumentado em 1 unidade. Logo, o novo valor da expressão 2mt será exatamente 2. Assim, no início da próxima iteração, a tabela continuará tendo pelo menos 2 = 2mt moedas na poupança.

Provamos assim que a poupança tem pelo menos 2mt moedas no início de cada iteração.