Proof step 5 from proof stutf-maxinf-is-fin (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  (∀ n. ∃ n0. n < n0 ∧ ⌜n0⌝ < # nσ ∧ nσ[n0] = m) ∨ (∀ n. ¬ ⌜n⌝ < # nσ ∨ nσ[n] ≠ m), stutf(nσ) ⊦ # nσ = ∞ ∧ (∃ n. ∀ n0. ¬ n0 < n → nσ[n0] = m) ∨ (∀ n. ⌜n⌝ < # nσ → nσ[n] < m)

• Proof step 33:

  # nσ = ∞ ∧ (∃ n. ∀ n0. ¬ n0 < n → nσ[n0] = m) ∨ (∀ n. ⌜n⌝ < # nσ → nσ[n] < m), stutf(nσ) ⊦ (∀ n. ∃ n0. n < n0 ∧ ⌜n0⌝ < # nσ ∧ nσ[n0] = m) ∨ (∀ n. ¬ ⌜n⌝ < # nσ ∨ nσ[n] ≠ m)

Rule argument

Additional information