IterativeUnboundedNaturalAddInvBug - 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 metric)

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

Lemma #4 (state index: 4, requires clause)

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

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

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ m₂ ≠ z₂
∧ n₂ ≥ 0
∧ m₂ ≥ 0
∧ z₂ ≥ 0
∧ k₂ ≥ 0
∧ n₂ + m₂ = n₀ + m₀
∧ k₂ + m₂ = 0 + m₀
∧ n₂ + 1 ≥ 0
∧ k₂ + 1 ≥ 0
∧ m₂ – 1 ≥ 0
 
⇒ n₂ + 1 + (m₂ – 1) = n₀ + m₀

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

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ m₂ ≠ z₂
∧ n₂ ≥ 0
∧ m₂ ≥ 0
∧ z₂ ≥ 0
∧ k₂ ≥ 0
∧ n₂ + m₂ = n₀ + m₀
∧ k₂ + m₂ = 0 + m₀
∧ n₂ + 1 ≥ 0
∧ k₂ + 1 ≥ 0
∧ m₂ – 1 ≥ 0
 
⇒ k₂ + 1 + (m₂ – 1) = 0 + m₀

Lemma #7 (state index: 5, loop metric)

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

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

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

Lemma #9 (state index: 7, parameter mode)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ n₆ ≥ 0
∧ z₆ ≥ 0
∧ k₆ ≥ 0
∧ n₆ + z₆ = n₀ + m₀
∧ k₆ + z₆ = 0 + m₀
 
⇒ k₆ = m₀

Lemma #10 (state index: 7, ensures clause)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ n₆ ≥ 0
∧ z₆ ≥ 0
∧ k₆ ≥ 0
∧ n₆ + z₆ = n₀ + m₀
∧ k₆ + z₆ = 0 + m₀
 
⇒ n₆ = n₀ + k₆