Proof step 11 from proof isempty-ext (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

  n0 + n < # buf ⊦ buf[n0 + n] = empty ∧ isempty(buf, n0, n) ↔ (∀ n1. n0 ≤ n1 ∧ ¬ n0 + n < n1 → buf[n1] = empty), isempty(buf, n0, n), ∀ n2. n0 ≤ n2 ∧ n2 < n0 + n → buf[n2] = empty

• Proof step 14:

  n0 + n < # buf, isempty(buf, n0, n), ∀ n2. n0 ≤ n2 ∧ n2 < n0 + n → buf[n2] = empty ⊦ buf[n0 + n] = empty ∧ isempty(buf, n0, n) ↔ (∀ n1. n0 ≤ n1 ∧ ¬ n0 + n < n1 → buf[n1] = empty)

Rule argument

Additional information