INDUÇÃO MATEMÁTICA

RAUL H.C. LOPES

1. Indução matemática

1.1. Conjunto indutivamente definido. Considere a seguinte definição, encontrada em [5].

Definição de um conjunto indutivo. Um conjunto de números reais é chamado de conjunto indutivo se ele tem as seguintes propriedades:

(1) O número 1 pertence ao conjunto.

(2) Para todo x pertencente ao conjunto, o número x + 1 também pertence ao conjunto.

Essa definição apresenta um método para computar números reais a partir de um elemento inicial: o número 1. Note que essa definição limita-se a estabelecer como encontrar elementos de um conjunto indutivo de reais (os inteiros positivos): ela nem tenta cobrir todo o conjunto de reais e nem mesmo determinar exatamente todos os elementos do conjunto indutivo em questão.

Veja agora a seguinte definição retirada da mesma fonte.

Definição de inteiros positivos. Um número real é chamado inteiro positivo se ele pertence a todo conjunto indutivo.

A definição acima, claramente referindo-se e complementando a anterior, tentar definir exatamente o conjunto dos inteiros positivos estabelecendo que ele é a interseção de todos os conjuntos possíveis de se obter, usando a primeira definição.

Além de estabelecer um “método para enumerar” todos os elementos do conjunto de inteiros positivos, essas duas definições sugerem: i um método para testar se qualquer z é um inteiro postivo: tal teste consistiria em verificar se z é o elemento inicial do conjunto definido ou se ele pode ser reescrito como x + 1, para algum x pertencente ao conjunto definido.

ii um método de prova de propriedades sobre conjuntos de inteiros positivos. Para provar a propriedade P n, para todo n inteiro positivo basta: 1 Provar que a propriedade P é válida para o elemento inicial do

conjunto de interesse; 2 Provar que P k implica P (k + 1), ou seja, que, para qualquer

elemento do conjunto em questao, se P vale para esse elemento, então P vale para o seu sucessor.

Exemplo 1. Provar que para todo n

+i : 1 ≤ i < n : i = \frac{n(n − 1)}{2}

Prova.

Aplicar o método de prova acima delineado demanda:

• Identificar a propriedade a provar. Seja P uma função que mapeia um inteiro para booleanos (conjunto {T rue, F alse}), definido por

P = λn.+i : 1 ≤ i < n : i = \frac{n(n − 1)}{2}

Dada esta definição, a propriedade que se deseja provar seria

∧n : : P n

• Garantir que a propriedade trata de conjuntos indutivos, no caso inteiros positivos. Isto demanda ser mais preciso na definição do n: assumir que o objetivo é provar P para todo inteiro prositivo. Logo, P assume a seguinte definição:

P = λn.+i : i ∈ ℤ^{+} ∧ 1 ≤ i < n : i = \frac{n(n − 1)}{2}

O objetivo agora é provar:

∧n : n ∈ ℤ^{+} : P n

• Provar que a nova propriedade vale para 1.

P 1 =(ii ∈ ℤ^{+} ∧ 1 ≤ i < 1 : i : =\frac{1(1 − 1)}{2})

= ⟨Axioma Empty Range⟩

0 = \frac{1(1 − 1)}{2}

= ⟨Aritmética⟩

0 = 0

= ⟨Reflexividade de =⟩ T rue

Observações importantes sobre o trecho de prova acima:

– Por transitividade da igualdade, o trecho mostra que P 1 = T rue, o que diz em essência que P 1 é verdadeiro.

– Cada passo de prova é um processo de reescrita baseado em algum axioma.

– A igualdade é usada como equivalência lógica: duas expressões com valores booleanos iguais são logicamente equivalentes.

• Provar que, quando P k é verdadeiro, onde k ∈ ℤ^{+}, então P (k+ 1) também é verdadeiro. Reescrevendo P (k + 1):

P (k + 1) = (+i : i ∈ ℤ^{+} ∧ 1 ≤ i < k + 1 : i = \frac{(k + 1)(k + 1 − 1)}{2})

Note que assumir P k como verdadeiro, consiste em assumir

+i : i ∈ ℤ^{+} ∧ 1 ≤ i < k : i = \frac{k(k − 1)}{2}

+i : i ∈ ℤ^{+} ∧ 1 ≤ i < k + 1 : i

=⟨Definição Indutiva de Somatória⟩

+i : i ∈ ℤ^{+} ∧ 1 ≤ i < k : i + k

=⟨Assumindo P k⟩

\frac{k(k − 1)}{2} + k

=⟨Aritmética⟩

\frac{k(k + 1)}{2}

Observações importantes sobre o trecho de prova acima:

• Neste trecho de prova, foi feita a opção de se reescrever o lado esquerdo da igualdade que P (k + 1) representa até encontrar o lado direito dessa mesma igualdade.

• Cada passo da prova foi novamente um passo de reescrever alguma fórmula usando um axioma ou uma hipótese previamente apressentados.

• A transitividade da igualdade novamente garante a consistência da prova.

• Você é livre para escolher seu estilo de prova, mas cada passo

deve ser logicamente justificado.

□

4 RAUL H.C. LOPES

O princípio de prova delineado acima e usado no Exemplo 1 é formalizado como Princípio da Indução Matemática. Definição 1. Princípio da Indução Matemática sobre ℕ

(∀n : n ∈ ℕ : P n) = P 0 ∧ (∀k : k ∈ ℕ : P k ⇒ P (k + 1))

Exercício 1. Prove que (∀n0 : n0ℕ : (∀n : n ∈ ℕn0 ≤ n : P n) = P n_{0} ∧ (∀k : k ∈ ℕ ∧ k ≤ n_{0} : P k ⇒ P (k + 1))) Exemplo 2. Prove que

(∀n : n ∈ ℕ ∧ n ≥ 4 : n^{2} ≤ 2^{n})

Prova.

(∀n : n ∈ ℕ ∧ n ≥ 4 : n^{2} ≤ 2^{n})

=⟨Exercício 1⟩

(4^{2} ≤ 2^{4}) ∧ (∀k : k ∈ ℕ ∧ k ≥ 4 : k^{2} ≤ 2^{k} ⇒ (k + 1)^{2} ≤ 2^{k+1})

Prova de: 4^{2} ≤ 2^{4}

4^{2} ≤ 2^{4}

=⟨Aritmética⟩

T rue

Prova de: (∀k : k ∈ ℕ ∧ k ≥ 4 : k^{2} ≤ 2^{k} ⇒ (k + 1)^{2} ≤ 2^{k+1})
HI: k_{0} ∈ ℕ, k_{0} ≥ 4, P k = k_{0}^{2} ≤ 2^{k_{0}}
Prova de: (k_{0} + 1)^{2} ≤ 2^{k_{0}+1}

(k_{0} + 1)^{2}

=⟨Aritmética⟩

k_{0}^{2} + (2k_{0} + 1)

≤⟨P k⟩

2^{k_{0}} + (2k_{0} + 1)

≤⟨when k_{0} ≥ 3, 2k_{0} + 1 ≤ k_{0}^{2}⟩

2^{k_{0}} + k_{0}^{2}

≤⟨P k⟩

2^{k_{0}} + 2^{k_{0}}

=⟨Aritmética⟩

2^{k_{0}+1}

□

Exercício 2. Prove por indução:

(1) (+i : 1 ≤ i ≤ n : i) = n(n + 1)/2

(2) (+i : 0 ≤ i < n : 2^{i}) = 2^{n} − 1

(3) (+i : 0 ≤ i < n : 3^{i}) = (3^{n} − 1)/2

(4) (+i : 1 ≤ i ≤ n : i^{2}) = n(n + 1)(2n + 1)/6

(5) (+i : 0 ≤ i ≤ n : i.2^{i}) = (n − 1).2^{n+1} + 2

(6) (+i : 0 ≤ i ≤ n : (2i + 1)^{2}) = (n + 1)(2n + 1)(2n + 3)/3

(7) (+i : 0 ≤ i ≤ n : i(i + 1)(i + 2)) = n(n + 1)(n + 2)(n + 3)/4 (8) ∀n, a : n ≥ 1 ∧ a ≠ 1 : (+i : 0 ≤ i < n : a^{i}) = (1 − a^{n})/(1 − a)

(9) ∀n : n ≥ 1 : (+i : 1 ≤ i ≤ n : 1/(i.(i + 1))) = n/(n + 1)

(10) ∀n : n ≥ 3 : n + 1 < 2^{n}

(11) ∀n : n ≥ 4 : n^{2} ≤ 2^{n}

(12) ∀n : n ≥ 7 : 3^{n} < n!

1.2. Ouro de tolo? Já dá para conjecturar: o método de prova acima, o chamado Princípio da Indução, deve ser aplicável à prova de propriedades de qualquer conjunto contável. Então... Dado o conjunto de humanos, que nem mesmo é infinito, ficamos tentados a realizar aplicações mais interessantes.

Exercício 3. Prove que todas as garotas loiras têm olhos claros.

Para obter a prova acima, você pode:

(1) Esquecer o Princípio da Indução e partir para o experimento. Que tal na sua turma de Estruturas de Dados? É claro que isso demanda definir: i O que são garotas? Ok! Isso pode não ser politicamente correto!

ii O que são olhos claros?

(2) Tentar Princípio da Indução, mas quem são P k e P (k + 1)? Aliás, esse é o ponto fundamental de toda a prova por indução: indentificar P k, a hipótese de indução, e realizar o passo indutivo para obter P (k + 1).

Ok! De volta ao reino de ℕ...

Veja o seguinte “teorema”e sua “prova”, retirados de [3].

Teorema Suspeito 1. Dados inteiros positivos a e n, a^{n−1} = 1.

Prova Suspeita. 1 Para n = 1, a^{1−1} = a^{0} = 1. 2 Para n = k + 1,

a^{(k+1)−1} = a^{k} = a^{k−1} · a = \frac{a^{k−1} · a^{k−1}}{a^{(k−2)}} = \frac{1 · 1}{1} = 1

O que está errado? Talvez o fato de que para se obter a prova para n = k + 1, foram usados como hipóteses o fato de que a assertiva seria válida para n = k e n = k − 1? Não! Na verdade, como mostrado na próxima seção, esse é um raciocínio válido.

1.3. Indução para Well-founded sets. Considere a seguinte série, conhecida como série de Fibonacci^{1}.

Definição 2. A série de Fibonacci é o conjunto indutivo dos F_{i}, definidos por:

F_{0} =0
F_{1} =1
F_{n} =F_{n−1} + F_{n−2}, para n > 1

Exemplo 3. Prove que

(∀n : n ∈ ℕ : F_{n} < 2^{n})

Prova.

(∀n : n ∈ ℕ : F_{n} < 2^{n})

=⟨definição 1.1⟩

F_{0} < 2^{0} ∧ (∀k : k ∈ ℕ : F_{k} < 2^{k} ⇒ F_{k+1} < 2^{k+1})

Prova de: F_{0} < 2^{0}

F_{0} < 2_{0}

=⟨F (axioma 0) e Aritmética⟩

0 < 1

=

T rue

Prova de: (∀k : k ∈ ℕ : F_{k} < 2^{k} ⇒ F_{k+1} < 2^{k+1})
HI: k ∈ ℕ, P k = F_{k} < 2^{k}

F_{k+1} < 2^{k+1}

=⟨F (axioma 2)⟩

F_{k} + F_{k−1} < ⟨P k⟩

2^{k} + F_{k−1}

⟨Nenhuma hipótese sobre F_{k−1}⟩

1Veja em [2] e [3] história, fatos e folclore em torno do números de Fibonacci.

O Exemplo 1.3 não pode ser completado porque não há hipóteses sobre o valor de F_{k−1}. A seguinte variante do princípio da indução poderia ajudar, se usada com cuidado.

Definição 3. Princípio da Indução Forte.

(∀n : n ∈ ℕ : P n) = (∀n : n ∈ ℕ : (∀k : k ∈ ℕ ∧ k < n : P k ⇒ P n))

O Exemplo 1.3 poderia agora ser completado desde que se definição 1.3 para assumir que F_{k−1} < 2^{k−1}. Mas, seguindo o mesmo raciocínio, a seguinte prova também seria trivialmente obtida.

Exemplo 4. Use a definição 1.3 e o raciocínio do Exemplo 1.3 para provar que todos os números da série de Fibonacci são pares.

Humm... Mas, 1, 3, 5 todos estão na série de Fibonacci e são ímpares. Bem, talvez sejam apenas uns poucos, uma minoria. Basta disfarçar e fingir que não estão lá. O teorema seria “aproximadamente válido.” Ou... “esquece tudo: essa tal de Ciência da Computação não funciona porque o fundamento matemático não é confiável.” Ou… O que está errado? A série de Fibonacci é um conjunto indutivo com dois elementos iniciais: F_{0} = 0 e F_{1} = 1. O chamado caso base da prova por indução deve demandar a prova de que a propriedade em questão vale para esses dois elementos. No Exemplo 1.3, no caso base, demanda-se provar que F_{1} é par. A prova falha nesse ponto.

Considere o seguinte problema.^{2}

Exercício 4. Para qualquer número n ≥ 8, é possível obter a partir de uma soma de fatores todos iguais a 3 ou 5.

Exercício 5. Prove que os princípios da definição 1.1 e definição 1.3 são equivalentes

1.4. Classe indutiva.

Definição 4. 𝔛 é uma classe indutiva se:

(i) seus elementos são gerados a partir de uma das seguintes operações:

1. existe uma especificação inicial B de um conjunto de elementos que pertencem a 𝔛 (chamados elementos iniciais);

2. existe um conjunto M de operações que aplicadas a elementos

de 𝔛 produzem novos elementos de 𝔛. (ii) Todos elemento de 𝔛 pode ser obtido começando com um ou mais

elementos de B e aplicando a cada passo uma operação de M a elementos obtidos em algum passo anterior ou obtidos de B.

2Retirado das notas de aula de Tom Leighton, do curso de Mathematics for Computer Science, MIT, Setembro/97.

comum dizer que X é a menor classe (ou o fecho universial da classe), cujos elementos iniciais são dados por B e que tem novos elementos construídos por aplicações repetidas de M. ^{3}

Exemplo 5. A série de Fibonacci é uma classe indutiva, cujos elementos iniciais são F_{0} = e F_{1} = 1. Qualquer F_{n}, para n > 1, é obtido da soma de F_{n−1} e F_{n_{2}}.

O Princípio da Indução fica mais claro quando aplicado ao conceito de classe indutiva.

Definição 5. Uma propriedade P é válida para todos os elementos de uma classe indutiva 𝔛 se:

(i) P é válida para todos os elementos iniciais de 𝔛 (P é válida para os elementos gerados por B).

(ii) Qualquer operação M (que permite gerar elementos de 𝔛 a partir de elementos já conhecidos) preserva a validade de P.

Exemplo 6. Uma propriedade é válida para classe da série de Fibonacci, introduzida na definição 1.3 se ela for válida para seus elementos iniciais: 0 e 1. Logo, a propriedade de que todos os elementos da classe são pares, do Exemplo 1.3, não é válida.

Exercício 6. Reveja sua prova do Exemplo 1.3 à luz do conceito de classe indutiva.

Exercício 7. Seja ϕ = (1 + \sqrt{5})/2. Prove que

ϕ^{n−2} ≤ F_{n} ≤ ϕ^{n−1}

2. Well-Founded Sets

O princípio da Indução apresentado na definição 1.3 pode ser generalizado para qualquer conjunto que possa ser caraterizado como well founded. Classes indutivas podem ser caraterizadas a partir do conceito de well-foundedness.

Definição 6. Elemento Minimal. Dado um par ⟨U, ≺⟩, y é um elemento minimal de S, denotado por y ∈ ↓(U, ≺), se

y ∈ S ∧ (∀x : x ≺ y : x ∉ S : .)

Definição 7. Um conjunto U é dito well founded por uma relação ≺, denotado por wff(U, ≺), quando todo subconjunto não vazio de U tem um elemento minimal.

3Veja capítulos iniciais [1] sobre conceitos de classe indutiva, algoritmo, e questes definidas e semi-definidas.

Definição 8. Indução Matemática sobre Well-Founded Sets. Dado um par ⟨U, ≺⟩, tal que wff(U, ≺), a sequinte equivalência define o princípio de prova por indução para propriedades sobre U:

(∀x : x ∈ U : P x)

= (∀x : x ∈ U : (∀y : y ∈ U ∧ y ≺ u : P y) ⇒ P x)

A definição 2 e a definição 2 Note que a definição 2 permite provar P x se for possível provar que P x vale quando P valer para todos os elementos que precedem x. Isso equivale dizer que essa definição demanda provar que P k sempre que k é um elemento minimal em wff(U, ≺). Isso é explicitamente colocado na definição 2.

Definição 9. Indução Matemática sobre Well-Founded Sets (alternativa). Dado um par ⟨U, ≺⟩, tal que wff(U, ≺), a sequinte equivalência define o princípio de prova por indução para propriedades sobre U:

(∀x : x ∈ U : P x)

=

(∀y : y ∈ ↓(U, ≺) : P y)∧(∀x : x ∈ U : (∀y : y ∈ U ∧ y ≺ u : P y) ⇒ P x)

Teorema 1. Qualquer M ⊆ ℕ, tal que M não é vazio, tem um elemento mínimo.

Demonstração. Assumindo que M ⊆ ℕ e que M não tem elemento mínimo, chega-se à contradição de que M é vazio. Por Princípio da Indução Forte, prova-se que ∀n : n ∈ ℕ : n ∉ M.

(1) Para n = 0, n ∉ M ou n seria mínimo, pois M ⊆ ℕ e 0 é mínimo em ℕ.

(2) Assumindo-se que ∀k ∈ ℕ : ≤≤ 0kn : k ∉ M, conclui-se que k+1 ∉

M, ou k + 1 seria mínimo de M.

Logo M é vazio, ou M tem mínimo.

□

Exercício 8. Construa a prova do Exercício 1.4 usando a definição 2.

3. Indução e computação

Esta seção deverá ser completamente revisada (correção de alguns erros sérios e atualização de notação e terminologia.) No entao, os eexercícios propostos podem (e devem) ser resolvidos usando a teoria apresentada nas seções anteriores. Have fun!

3.1. Tipos como conjuntos indutivos. Tipos de dados são representações em alguma linguagem de programação de classes indutivas. Na verdade, qualuqer computação pode ser vista como a atividade de enumerar os elementos de uma class indutiva.

Exemplo 7. Considere a classe Natnum como a menor classe que contém:

(i) Z, como único elemento inicial; (ii) (Sx), quando x já pertence a Natnum.

3.2. Admissibilidade de funções. Uma representação em Haskell para a classe Natnum seria:

  data Natnum = Z | (S Natnum)

Um exemplo de função seria:

  itsum m Z = m
  itsum m (S n) = itsum (S m) n

A função itsum acima definida permite introduzir dois conceitos importantes:

1. Admissibilidade da função: a função acima será dita admissível porque existe uma medida de complexidade dos seus argumentos que é sempre decrescente em qualquer chamada recursiva da mesma. Nessa função, o segundo argumento da chamada recursiva é sempre mais simples que o segundo argumento da chamada que a precede.

Por exemplo, assuma um mapeamento f : Natnum → ℕ que associa:

f.(m, Z) =0
f.(m, (Sn)) =f.n + 1

Claramente f ’e uma medida de complexidade para os argumentos de chamada de itsum decresce a cada chamada recursiva, formando um cadeia finita decrescente, com mínimo em (m, Z).

2. Diferentemente da função recsum abaixo, itsum pode ser avaliada por um processo de repetição substituições simples da chamada original pela chamada recursiva.

  recsum m Z = m
  recsum m (S n) = S(recsum m n)

A computação de recsum demanda que uma memória seja mantida das sucessivas chamadas recursivas para os S sejam adicionados ao resultado final da chamada não recursiva.

Uma função interessante de se definir para a aritmética de Peano é a de subtração. Veja as seguintes definições.

  pred Z = Z
  pred (S m) = m

  recsub m Z = m
  recsub m (S n) = pred(recsub m n)

Nenhuma das definições concorda inteiramente com a aritmética de Peano: nesse sistema formal, zero não tem predecessor. Na definição acima, o objeto Z, introduzido para representar zero, tem como predecessor, via função pred, o próprio Z. Isso afeta diretamente a operação de subtração: a diferença de m e n quando o segundo é maior fica igual a zero.

Uma definição alternativa para a diferença de dois Natnum, é dada pela função iterativa itsub.

  itsub (m,Z) = m
  itsub (Z,n) = Z
  itsub ((S m),(S n)) = itsub (m,n)

Antes de mais nada, note que itsub é admissível.

Exercício 9. Prove que

itsub(m, (Sn)) = pred(itsub(m, n))

Use indução sobre n (segundo argumento do (m, n) da chamada recursiva.) No passo indutiva, considere dois casos: quando m é Z e quando m é (S u) para algum u.

3.3. Generalizando indução. É importante observar que a medidade complexidade de argumentos de uma função não precisa se restringir a um único argumento. Como exposto em [2] (ver também [4], página 20, exercício 15) podemos generalizar todo o conceito de indução matemática e de admissibilidade funções se, dado um conjunto S (de inteiros, Natnum, tuplas, etc), pudermos estabelecer um relação ≺ tal que:

• toda a cadeia em S tem um mínimo x: para todo y ∈ S existe um mínimo x tal que x ≺ x_{1} ≺ x_{2} ≺ … ≺ y.

• Se, para x, y, z ∈ S, x ≺ y e y ≺ z, então x ≺ z. Nessa situação S é dito bem fundado. Uma função recursiva é admissível se os argumentos das suas chamadas

recursivas admitem algum relação de precedência que determina um relação bem fundada.

  gcd m n = if m < n
            then gcd m (n-m)
            else if m > n
            then gcd (m-n) n
            else m

A relação abaixo

(m_{0}, n_{0}) ≺ (m_{1}, n_{1}) quando m_{0} < m_{1}
(m_{0}, n_{0}) ≺ (m_{1}, n_{1}) quando (m_{0} = m_{1}) ∧ (n_{0} < n_{1})

e o fato de que nas chamadas recursivas de gcd os argumentos de chamada são sempre maiores ou iguais do zero pode ser usada para provar que a definição de gcd é admissível ( sempre termina.)

Por outro lado, usando indução forte, a relação ≺ acima e o fato de que o maior divisor de m e n é também o maior divisor de m e m − n (quando m é maior do que n), permite provar que a função acima calcula corretamente o maior divisor comum de dois inteiros positivos.

3.4. Tipos abstratos de dados.

Exercício 10. Crie em Haskell um tipo de dados para representar seu indutivo da questão 7.

Exercício 11. Crie em Haskell, ao menos, as seguintes funções sobre o tipo da questão 10, defina e prove condições de correção para as mesmas:

(1) Funções recursiva e iterativa para cáclculo de:

• soma de dois objetos;

• diferença de dois objetos;

• produto de dois objetos;

• divião de dois objetos;

• resto da divisão inteira de dois objetos.

(2) Funções implementar os relações lógicas, apresentando condições de correção:

(a) igualdade;

(b) desigualdade; (c) menor que;

(d) maior que;

Exemplo 8. Dadas as definições de mult, recdiv e itmod, é possivel provar que

m = recsum(multq(Sn))r,

quando

q =recdivm(Sn)
r =itmodm(Sn)

o que corresponde ao teorema m = q ∗ n + r, com n maior do zero. Para maior clareza, as seguintes abreviações serão usadas:

m + n em lugar de recsum m n; m − n em lugar de itsub(m,n); m ∗ n em lugar de mult m n; m/n em lugar de recdiv m n; m%n em lugar de itmod m n.

Demonstração. Por indução forte sobre m.

1. m = Z.

m =((m/(Sn)) ∗ (Sn)) + (m%(Sn))
=⟨substituindo m⟩
((Z/(Sn)) ∗ (Sn)) + (Z%(Sn))
=⟨definições de recdiv, itmod⟩
(Z ∗ (Sn)) + Z
=⟨definição de mult⟩
Z + Z
=⟨definição de recsum⟩
Z

2. Assumindo que a propriedade é verdadeira para todo k menor ou igual a m, provamos que a mesma vale para k = (Sm). Há dois caos a considerar:

(i) lt(Sm)(Sn), ou seja, (Sm) menor do que (Sn).

(Sm) =(((Sm)/(Sn)) ∗ (Sn)) + ((Sm)%(Sn))
=⟨definições de recdiv e itmod⟩
(Z ∗ (Sn)) + (Sm)
=⟨definição de mult⟩
Z + (Sm)
=⟨definição de recsum⟩
(Sm)

(ii) quando (Sm) é maior ou igual a (Sn).

(Sm) =(((Sm)/(Sn)) ∗ (Sn)) + ((Sm)%(Sn))
=⟨definições de recdiv e itmod⟩

(S(((Sm) − (Sn))/(Sn)) ∗ (Sn)) + (((Sm) − (Sn))%(Sn))

=⟨definição de mult⟩

((((Sm) − (Sn))/(Sn)) ∗ (Sn)) + (Sn) + (((Sm) − (Sn))%(Sn))

=⟨comutatividade e associatividade de recsum⟩

(((((Sm) − (Sn))/(Sn)) ∗ (Sn)) + (((Sm) − (Sn))%(Sn))) + (Sn)

=⟨hipótese de indução
⟩((Sm) − (Sn)) + (Sn)
=(Sm)

□

Exercício 12. Repita o exercício anterior em um provador de teoremas (e.g. Isabelle, PVS), formalizando as provas correspondentes.

Referências

[1] Haskell B. Curry, Foundations of mathematical logic, Dover Publications, Inc., 1977.

[2] David Gries and Fred B.Schneider, A logical approach to discrete mathematics, Springer-Verlag, 1993.

[3] Donald E. Knuth, Fundamental algorithms, third ed., The Art of Computer Programming, vol. I, Addison-Wesley, 1998.

[4] , Sorting and searching, The Art of Computer Programming, vol. III, Addison-Wesley, 1998.

[5] Tom M.Apostol, Calculus: One-variable calculus, with an introduction to linear algebra, second edition ed., vol. I, John Wiley & Sons, Inc., 1967.