Proof step 1 from proof ex-first-nontau (conclusion) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ ext !(α) = [] ↔ (∀ n. ⌜n⌝ < # α → ext(α[n]) = None)

• Proof step 3:

  ∃ n. ¬(⌜n⌝ < # α → ext(α[n]) = None) ⊦ ∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)

Rule argument

Additional information

Used terms: ext, α

Proof step 2 from proof ex-first-nontau (previous step) (back to tree)

Lemma remtau-empty-equiv

Proof step 3 from proof ex-first-nontau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ext(α[n]) ≠ None, ⌜n⌝ < # α ⊦ ∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)

Rule argument

Additional information

Proof step 4 from proof ex-first-nontau (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 5:

  ext(α[n]) ≠ None, ⌜n⌝ < # α, ∀ n0, ext, α. n0 < n → ext(α[n0]) ≠ None ∧ ⌜n0⌝ < # α → (∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)) ⊦ ∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: n

Proof step 5 from proof ex-first-nontau (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 6:

  ext(α[n]) ≠ None, ⌜n⌝ < # α, ∀ n0, ext, α. n0 < n → ext(α[n0]) ≠ None ∧ ⌜n0⌝ < # α → (∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)) ⊦ ∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None), ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)

Rule argument

Additional information

Used terms: n

Proof step 6 from proof ex-first-nontau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ext(α[m]) ≠ None, ext(α[n]) ≠ None, m < n, ⌜n⌝ < # α, ∀ n0, ext, α. n0 < n → ext(α[n0]) ≠ None ∧ ⌜n0⌝ < # α → (∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)) ⊦ ∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)

Rule argument

Additional information

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

Proof step 7 from proof ex-first-nontau (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 8:

  ext(α[m]) ≠ None, ext(α[n]) ≠ None, ⌜n⌝ < # α, m < n, ∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None), ∀ n0, ext, α. n0 < n → ext(α[n0]) ≠ None ∧ ⌜n0⌝ < # α → (∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)) ⊦ ∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)

Rule argument

Additional information

Used simplifier rules: lsle-trans: ⊦ n∞ < n∞1 ∧ ¬ n∞2 < n∞1 → n∞ < n∞2; (forward) from specification nat-inf ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m < n → ¬ n < m; (s) Used terms: m, ext, α

Proof step 8 from proof ex-first-nontau (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ext(α[m]) ≠ None, ext(α[n]) ≠ None, ext(α[n0]) ≠ None, ⌜n0⌝ < # α, m < n, ⌜n⌝ < # α, ∀ m. m < n0 → ext(α[m]) = None, ∀ n0, ext, α. n0 < n → ext(α[n0]) ≠ None ∧ ⌜n0⌝ < # α → (∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)) ⊦ ∃ n. ⌜n⌝ < # α ∧ ext(α[n]) ≠ None ∧ (∀ m. m < n → ext(α[m]) = None)

Rule argument

Additional information

Proof step 9 from proof ex-first-nontau (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n0