Proof step 13 from proof leninv-succ (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  # nσ = ∞, stutf(nσ), ∀ m. (∃ m0. nσ[m0] = m - 1 ∧ ¬(∀ m1. m0 < m1 → nσ[m1] = m - 1)) → ¬ n + 1 < m, ∃ m. nσ[m] = n ∧ ¬(∀ m0. m < m0 → nσ[m0] = nσ[m]) ⊦ ∃ m. nσ[m] = n ∧ (∀ m0. m < m0 → nσ[m0] = nσ[m] + 1)

• Proof step 74:

  # nσ = ∞, stutf(nσ), ∃ m. nσ[m] = n ∧ (∀ m0. m < m0 → nσ[m0] = nσ[m] + 1) ⊦ (∃ m. nσ[m] = n ∧ ¬(∀ m0. m < m0 → nσ[m0] = nσ[m])) ∧ (∀ m. (∃ m0. nσ[m0] = m - 1 ∧ ¬(∀ m1. m0 < m1 → nσ[m1] = m - 1)) → ¬ n + 1 < m)

Rule argument

Additional information