Proof step 8 from proof datasize-le-h (previous step)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 9:

  buf[m1] = empty, m1 < # buf, m ≤ datasize(buf, m1), ∀ buf, m. m1 ≤ # buf → (m ≤ datasize(buf, m1) ↔ (∃ n. m ≤ n + 1 ∧ n < m1 ∧ buf[n] ≠ empty)) ∨ m = 0 ⊦ m = 0, ∃ n. m ≤ n + 1 ∧ ¬ m1 < n ∧ buf[n] ≠ empty

• Proof step 12:

  m1 < # buf, m ≤ m1 + 1, ∀ buf, m. m1 ≤ # buf → (m ≤ datasize(buf, m1) ↔ (∃ n. m ≤ n + 1 ∧ n < m1 ∧ buf[n] ≠ empty)) ∨ m = 0 ⊦ buf[m1] = empty, m = 0, ∃ n. m ≤ n + 1 ∧ ¬ m1 < n ∧ buf[n] ≠ empty

Rule argument

Additional information