Proof step 13 from proof in-below (previous step)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 14:

  n ∈ below(ns0, m) ↔ n ∈ ns0 ∧ n < m, n ∈ (n0 < m ⊃ below(ns0, m) ++ n0;below(ns0, m)), ∀ ns1, n, m. # ns1 < #(ns0 ++ n0) → true → (n ∈ below(ns1, m) ↔ n ∈ ns1 ∧ n < m) ⊦ n0 ∈ ns0, (n = n0 ∨ n ∈ ns0) ∧ n < m

• Proof step 18:

  n ∈ below(ns0, m) ↔ n ∈ ns0 ∧ n < m, n < m, n = n0 ∨ n ∈ ns0, ∀ ns1, n, m. # ns1 < #(ns0 ++ n0) → true → (n ∈ below(ns1, m) ↔ n ∈ ns1 ∧ n < m) ⊦ n0 ∈ ns0, n ∈ (n0 < m ⊃ below(ns0, m) ++ n0;below(ns0, m))

Rule argument

Additional information