RecursiveUnboundedNaturalMultiplyIncBug - Multiply

Lemma #1 (state index: 0, recursion metric)

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

Lemma #2 (state index: 9, requires clause)

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

Lemma #3 (state index: 10, recursion metric)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ m₀ ≠ 0
∧ 0 + 1 ≥ 0
∧ m₀ > 0 + 1
∧ m₀ – 1 ≥ 0
 
⇒ m₀ – 1 < m₀

Lemma #4 (state index: 14, parameter mode)

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

Lemma #5 (state index: 14, parameter mode)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ 0 + 1 ≥ 0
∧ m₀ – 1 ≥ 0
∧ n₀ × (m₀ – 1) ≥ 0
∧ n₀ × (m₀ – 1) + n₀ ≥ 0
∧ m₀ > 0 + 1
∧ m₀ ≠ 0
 
⇒ m₀ – 1 = m₀

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

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ 0 + 1 ≥ 0
∧ m₀ ≤ 0 + 1
∧ m₀ ≠ 0
 
⇒ m₀ = m₀

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

  n₀ ≥ 0
∧ 0 ≥ 0
 
⇒ 0 = n₀ × 0

Lemma #8 (state index: 14, ensures clause)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ 0 + 1 ≥ 0
∧ m₀ – 1 ≥ 0
∧ n₀ × (m₀ – 1) ≥ 0
∧ n₀ × (m₀ – 1) + n₀ ≥ 0
∧ m₀ > 0 + 1
∧ m₀ ≠ 0
 
⇒ n₀ × (m₀ – 1) + n₀ = n₀ × (m₀ – 1)

Lemma #9 (state index: 14, ensures clause)

  n₀ ≥ 0
∧ m₀ ≥ 0
∧ 0 ≥ 0
∧ 0 + 1 ≥ 0
∧ m₀ ≤ 0 + 1
∧ m₀ ≠ 0
 
⇒ n₀ = n₀ × m₀