IterativeUnboundedNaturalAddDecBug

State Index	Path Conditions	Facts	Obligations
procedure Add (updates n: Natural, restores m: Natural)
0		n₀ ≥ 0 m₀ ≥ 0
variable k, z: Natural
1		n₁ ≥ 0 m₁ ≥ 0 z₁ ≥ 0 k₁ ≥ 0 n₁ = n₀ m₁ = m₀ k₁ = 0 z₁ = 0	n₁ + m₁ = n₁ + m₁ k₁ + m₁ = k₁ + m₁ z₁ = 0 m₁ ≠ z₁ ⇒ m₁ > 0
loop maintains n + m = #n + #m and k + m = #k + #m and z = 0 decreases m while not AreEqual (m, z) do
2	m₂ ≠ z₂	n₂ ≥ 0 m₂ ≥ 0 z₂ ≥ 0 k₂ ≥ 0 n₂ + m₂ = n₁ + m₁ k₂ + m₂ = k₁ + m₁ z₂ = 0 m₂ ≥ 0
Increment (n)
3	m₂ ≠ z₂	n₃ ≥ 0 m₃ ≥ 0 k₃ ≥ 0 z₃ ≥ 0 n₃ = n₂ + 1 m₃ = m₂ k₃ = k₂ z₃ = z₂
Increment (k)
4	m₂ ≠ z₂	n₄ ≥ 0 m₄ ≥ 0 k₄ ≥ 0 z₄ ≥ 0 k₄ = k₃ + 1 n₄ = n₃ m₄ = m₃ z₄ = z₃	n₄ + m₄ = n₁ + m₁ k₄ + m₄ = k₁ + m₁ z₄ = 0 m₄ ≥ 0 m₄ < m₂
end loop
5		n₅ ≥ 0 m₅ ≥ 0 z₅ ≥ 0 k₅ ≥ 0 m₅ = z₅ n₅ + m₅ = n₁ + m₁ k₅ + m₅ = k₁ + m₁ z₅ = 0
m :=: k
6		n₆ ≥ 0 m₆ ≥ 0 z₆ ≥ 0 k₆ ≥ 0 m₆ = k₅ k₆ = m₅ n₆ = n₅ z₆ = z₅	m₆ = m₀ n₆ = n₀ + m₆
end Add