IterativeUnboundedNaturalAdd

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₃	m₄ > 0
Decrement (m)
5	m₂ ≠ z₂	n₅ ≥ 0 m₅ ≥ 0 k₅ ≥ 0 z₅ ≥ 0 m₅ = m₄ – 1 n₅ = n₄ k₅ = k₄ z₅ = z₄	n₅ + m₅ = n₁ + m₁ k₅ + m₅ = k₁ + m₁ z₅ = 0 m₅ ≥ 0 m₅ < m₂
end loop
6		n₆ ≥ 0 m₆ ≥ 0 z₆ ≥ 0 k₆ ≥ 0 m₆ = z₆ n₆ + m₆ = n₁ + m₁ k₆ + m₆ = k₁ + m₁ z₆ = 0
m :=: k
7		n₇ ≥ 0 m₇ ≥ 0 z₇ ≥ 0 k₇ ≥ 0 m₇ = k₆ k₇ = m₆ n₇ = n₆ z₇ = z₆	m₇ = m₀ n₇ = n₀ + m₇
end Add