IterativeUnboundedNaturalAddDecBug - Add

Lemma #1 (state index: 1, loop invariant)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
 
⇒ n₀ + m₀ = n₀ + m₀

Lemma #2 (state index: 1, loop invariant)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
 
⇒ 0 + m₀ = 0 + m₀

Lemma #3 (state index: 1, loop invariant)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
 
⇒ 0 = 0

Lemma #4 (state index: 1, loop metric)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
 
⇒ m₀ ≠ 0 ⇒ m₀ > 0

Lemma #5 (state index: 4, loop invariant)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ m₂ ≠ 0
∧ n₂ ≥ 0
∧ m₂ ≥ 0
∧ k₂ ≥ 0
∧ n₂ + m₂ = n₀ + m₀
∧ k₂ + m₂ = 0 + m₀
∧ n₂ + 1 ≥ 0
∧ k₂ + 1 ≥ 0
 
⇒ n₂ + 1 + m₂ = n₀ + m₀

Lemma #6 (state index: 4, loop invariant)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ m₂ ≠ 0
∧ n₂ ≥ 0
∧ m₂ ≥ 0
∧ k₂ ≥ 0
∧ n₂ + m₂ = n₀ + m₀
∧ k₂ + m₂ = 0 + m₀
∧ n₂ + 1 ≥ 0
∧ k₂ + 1 ≥ 0
 
⇒ k₂ + 1 + m₂ = 0 + m₀

Lemma #7 (state index: 4, loop invariant)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ m₂ ≠ 0
∧ n₂ ≥ 0
∧ m₂ ≥ 0
∧ k₂ ≥ 0
∧ n₂ + m₂ = n₀ + m₀
∧ k₂ + m₂ = 0 + m₀
∧ n₂ + 1 ≥ 0
∧ k₂ + 1 ≥ 0
 
⇒ 0 = 0

Lemma #8 (state index: 4, loop metric)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ m₂ ≠ 0
∧ n₂ ≥ 0
∧ m₂ ≥ 0
∧ k₂ ≥ 0
∧ n₂ + m₂ = n₀ + m₀
∧ k₂ + m₂ = 0 + m₀
∧ n₂ + 1 ≥ 0
∧ k₂ + 1 ≥ 0
 
⇒ m₂ ≥ 0

Lemma #9 (state index: 4, loop metric)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ m₂ ≠ 0
∧ n₂ ≥ 0
∧ m₂ ≥ 0
∧ k₂ ≥ 0
∧ n₂ + m₂ = n₀ + m₀
∧ k₂ + m₂ = 0 + m₀
∧ n₂ + 1 ≥ 0
∧ k₂ + 1 ≥ 0
 
⇒ m₂ < m₂

Lemma #10 (state index: 6, parameter mode)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ n₅ ≥ 0
∧ k₅ ≥ 0
∧ n₅ + 0 = n₀ + m₀
∧ k₅ + 0 = 0 + m₀
 
⇒ k₅ = m₀

Lemma #11 (state index: 6, ensures clause)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ n₅ ≥ 0
∧ k₅ ≥ 0
∧ n₅ + 0 = n₀ + m₀
∧ k₅ + 0 = 0 + m₀
 
⇒ n₅ = n₀ + k₅