Proof step 13 from proof maxinf-skolemf (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  np(n0), ∀ n1, n2, np. n1 - n2 < n - n0 → np(n2) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n1 < n0 ∧ np(n0)) ⊦ np(n), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n0. n < n0 ∧ np(n0)

• Proof step 30:

  np(n0), ∀ n1, n2, np. n1 - n2 < n - n0 → np(n2) → (∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0))) ∨ (∃ n0. n1 < n0 ∧ np(n0)) ⊦ n < n1 → ¬ np(n1), ∃ n. np(n) ∧ (∀ n0. n < n0 → ¬ np(n0)), ∃ n0. n < n0 ∧ np(n0)

Rule argument

Additional information