Proof step 9 from proof in-ecs-n (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  wlar[n0] = wl-entry(m0, stat), n0 < # wlar, m ∈ ecs(wlar, n0), ∀ wlar, m. n0 ≤ # wlar → (m ∈ ecs(wlar, n0) ↔ (∃ n1. n1 < n0 ∧ wlar[n1].ec = m)) ⊦ ∃ n. ¬ n0 < n ∧ wlar[n].ec = m

• Proof step 14:

  wlar[n0] = wl-entry(m0, stat), m = m0, n0 < # wlar, ∀ wlar, m. n0 ≤ # wlar → (m ∈ ecs(wlar, n0) ↔ (∃ n1. n1 < n0 ∧ wlar[n1].ec = m)) ⊦ ∃ n. ¬ n0 < n ∧ wlar[n].ec = m

Rule argument

Additional information