Proof step 1 from proof leninv-inf-strong (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  stutf(nσ) ⊦ leninv(nσ) = ∞ ↔ # nσ = ∞ ∧ (∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0]) ∧ (∀ m. ∃ m0. m < nσ[m0])

Rule argument

Additional information

Proof step 2 from proof leninv-inf-strong (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ stutf(nσ) → (leninv(nσ) = ∞ ↔ # nσ = ∞ ∧ (∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0]))

• Proof step 4:

  stutf(nσ) ⊦ # nσ = ∞ ∧ (∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0]) ↔ # nσ = ∞ ∧ (∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0]) ∧ (∀ m. ∃ m0. m < nσ[m0])

Rule argument

Additional information

Used terms: nσ

Proof step 3 from proof leninv-inf-strong (previous step) (back to tree)

Lemma leninv-inf

Proof step 4 from proof leninv-inf-strong (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # nσ = ∞, stutf(nσ), ∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0] ⊦ ∃ m0. n < nσ[m0]

Rule argument

Additional information

Proof step 5 from proof leninv-inf-strong (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  # nσ = ∞, stutf(nσ), ∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0] ⊦ ∃ m0. 0 < nσ[m0]

• Proof step 10:

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

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;

Proof step 6 from proof leninv-inf-strong (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  # nσ = ∞, stutf(nσ), ∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0] ⊦ ∃ m0. nσ[m0] ≠ 0

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 7 from proof leninv-inf-strong (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 8:

  # nσ = ∞, stutf(nσ), ∃ m0. 0 < m0 ∧ nσ[0] < nσ[m0] ⊦ ∃ m0. nσ[m0] ≠ 0

Rule argument

Additional information

Used terms: 0

Proof step 8 from proof leninv-inf-strong (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # nσ = ∞, nσ[n] ≠ 0, n ≠ 0, stutf(nσ) ⊦ ∃ m0. nσ[m0] ≠ 0

Rule argument

Additional information

Used simplifier rules: stutf-zero: ⊦ stutf(nσ) → nσ[0] = 0; ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 9 from proof leninv-inf-strong (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n

Proof step 10 from proof leninv-inf-strong (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)

Proof step 11 from proof leninv-inf-strong (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used terms: nσ

Proof step 12 from proof leninv-inf-strong (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 13 from proof leninv-inf-strong (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used terms: n

Proof step 14 from proof leninv-inf-strong (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # nσ = ∞, nσ[n] = n0 + 1, stutf(nσ), n0 + 1 ≤ n0 + 1, ∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0] ⊦ ∃ m0. n0 + 1 < nσ[m0]

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m + 1 ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 15 from proof leninv-inf-strong (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 16:

  # nσ = ∞, nσ[n] = n0 + 1, stutf(nσ), n0 + 1 ≤ n0 + 1, ∃ m0. n < m0 ∧ nσ[n] < nσ[m0] ⊦ ∃ m0. n0 + 1 < nσ[m0]

Rule argument

Additional information

Used terms: n

Proof step 16 from proof leninv-inf-strong (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  # nσ = ∞, nσ[n] = n0 + 1, n0 + 1 < nσ[n1], n < n1, stutf(nσ), n0 + 1 ≤ n0 + 1 ⊦ ∃ m0. n0 + 1 < nσ[m0]

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 17 from proof leninv-inf-strong (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n1