Proof step 1 from proof diag-theorem-butlast (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) )

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 ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 2 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 3:

  ∀ n, a. nextl(n, a) ≠ [] ⊦ ∃ lf. lf(0) = a ' ∧ (∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [])

• Proof step 4:

  ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ ∀ n, a. nextl(n, a) ≠ [], ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) )

• Proof step 6:

  ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∃ lf. lf(0) = a ' ∧ (∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ []) ⊦ ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) )

Rule argument

Additional information

Used terms: nextl, a

Proof step 3 from proof diag-theorem-butlast (previous step) (back to tree)

Lemma nextl-lemma-butlast-nonempty

Proof step 4 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  nextl(n, a0) = [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) )

Rule argument

Additional information

Proof step 5 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n, a0

Proof step 6 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  lf(0) = a ', ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) )

Rule argument

Additional information

Proof step 7 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 8:

  ∀ n. lf(n).last = lf(n + 1).head ∧ lf(n) ≠ [] ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n) = ⌜lf(n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n) + 1⌝ ∧ (∀ m. n ≤ m → lf(m).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

• Proof step 9:

  lf(0) = a ', ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [] ⊦ ∀ n. lf(n + 1).last = lf((n + 1) + 1).head ∧ lf(n + 1) ≠ [], ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) )

• Proof step 13:

  lf(0) = a ', ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n) + 1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ⊦ ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) )

Rule argument

Additional information

Used terms: λ n. lf(n + 1)

Proof step 8 from proof diag-theorem-butlast (previous step) (back to tree)

Lemma infinite-append-butlast

Proof step 9 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  lf(0) = a ', ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ), lf(n + 1).last = lf(2 + n).head ∧ lf(n + 1) ≠ []

Rule argument

Additional information

Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 10 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  lf(0) = a ', lf((n + 1) + 1) = nextl(n + 1, lf(n + 1).last), lf(n + 1) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [] ⊦ ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ), lf(n + 1).last = lf(2 + n).head ∧ lf(n + 1) ≠ []

Rule argument

Additional information

Used terms: n + 1

Proof step 11 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  lf(0) = a ', lf(2 + n) = nextl(n + 1, lf(n + 1).last), lf(n + 1).last ≠ lf(2 + n).head, lf(n + 1) ≠ [], ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) )

Rule argument

Additional information

Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 12 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n + 1, lf(n + 1).last

Proof step 13 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  ii(0) = 0, lf(0) = a ', (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m)) ;∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) )

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 ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 14 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 15:

  ii(0) = 0, lf(0) = a ', (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Used terms: σ, ii

Proof step 15 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ii(0) = 0, lf(0) = a ', (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ σ[0] = a ∧ σ ≠ [] ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ ⌜ii(n0 + 1)⌝ < # σ ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

Rule argument

Additional information

Proof step 16 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 17:

  ii(0) = 0, ii(0 + 1) = ii(0) + # lf(0 + 1) - 1, lf(0) = a ', (σ from ii(0)) to # lf(0 + 1) = ⌜lf(0 + 1)⌝ , ⌜ii(0 + 1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ σ[0] = a ∧ σ ≠ [] ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ ⌜ii(n0 + 1)⌝ < # σ ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

Rule argument

Additional information

Used terms: 0

Proof step 17 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  ii(0) = 0, ii(1) = # lf(1) - 1, lf(0) = a ', σ to # lf(1) = ⌜lf(1)⌝ , σ ≠ [], ⌜ii(1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ⌜ii(n0 + 1)⌝ < # σ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # [] = ⌜0⌝ ; (s) ⊦ σ from 0 = σ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s)

Proof step 18 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 19:

  ii(1) = # lf(1) - 1, ii(0) = 0, lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), σ to # lf(1) = ⌜lf(1)⌝ , lf(n0) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ⌜ii(n0 + 1)⌝ < # σ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: n0

Proof step 19 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

  ii(0) = 0, ii(1) = # lf(1) - 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', σ to # lf(1) = ⌜lf(1)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , lf(n0) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ⌜ii(n0 + 1)⌝ < # σ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: n0

Proof step 20 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(1) = # lf(1) - 1, ii(0) = 0, lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to # lf(1) = ⌜lf(1)⌝ , lf(n0) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Proof step 21 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

  ii(0) = 0, ii(1) = # lf(1) - 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(0 + 1) = nextl(0, lf(0).last), σ to # lf(1) = ⌜lf(1)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , lf(0) ≠ [], lf(n0) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: 0

Proof step 22 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ii(0) = 0, ii(1) = # nextl(0, a) - 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), σ to # nextl(0, a) = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , lf(n0) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s) ⊦ a '.last = a; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic

Proof step 23 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  nextl(0, a).head = a, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(1) = # nextl(0, a) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to # nextl(0, a) = ⌜nextl(0, a)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: 0, a

Proof step 24 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  nextl(0, a).head = a, ii(0) = 0, ii(1) = # nextl(0, a) - 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), σ to # nextl(0, a) = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Proof step 25 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 26:

  # nextl(0, a) = m0 + 1, nextl(0, a).head = a, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(1) = m0, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to # nextl(0, a) = ⌜nextl(0, a)⌝ , # nextl(0, a) ≠ 0, lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: # nextl(0, a), m0

Proof step 26 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  # nextl(0, a) = ii(1) + 1, nextl(0, a).head = a, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s)

Proof step 27 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 28:

  # nextl(0, a) = ii(1) + 1, a0 = a, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a0 + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: nextl(0, a), a0, y

Proof step 28 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  # nextl(0, a) = ii(1) + 1, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s)

Proof step 29 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 30:

  # nextl(0, a) = ii(1) + 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. σ[ii(n)] = lf(n).last ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

• Proof step 53:

  # nextl(0, a) = ii(1) + 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ ∀ n. σ[ii(n)] = lf(n).last, (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used formulas: ∀ n. σ[ii(n)] = lf(n).last

Proof step 30 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 31:

  # nextl(0, a) = ii(1) + 1, σ[ii(n0)] = lf(n0).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. σ[ii(n)] = lf(n).last, ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: n0

Proof step 31 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  # nextl(0, a) = ii(1) + 1, σ[ii(n0)] = lf(n0).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, σ[ii(n0)]), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. σ[ii(n)] = lf(n).last, ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ σ[0] = a

Rule argument

Additional information

Proof step 32 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 33:

  # nextl(0, a) = ii(1) + 1, σ[ii(n0)] = lf(n0).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, σ[ii(n0)]), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. σ[ii(n)] = lf(n).last ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

• Proof step 52:

  # nextl(0, a) = ii(1) + 1, σ[ii(n0)] = lf(n0).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, σ[ii(n0)]), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , σ[0] ≠ a, lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. σ[ii(n)] = lf(n).last ⊦

Rule argument

Additional information

Proof step 33 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 34:

  # nextl(0, a) = ii(1) + 1, σ[ii(n0)] = lf(n0).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, σ[ii(n0)]), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, finp(σ), a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. σ[ii(n)] = lf(n).last, ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m))

• Proof step 48:

  # nextl(0, a) = ii(1) + 1, σ[ii(n0)] = lf(n0).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, σ[ii(n0)]), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), ¬ finp(σ), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. σ[ii(n)] = lf(n).last, ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)

Rule argument

Additional information

Proof step 34 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, x[ii(n0)] = lf(n0).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, x[ii(n0)]), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, x to ii(1) + 1 = nextl(0, a), (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), lf(n0) ≠ [], nextl(0, a) ≠ [], x ≠ [], ii(n0 + 1) < # x, ii(1) < # x, a ∈ nextl(0, a), ii(1) ≤ ii(n), ii(n0 + 1) ≤ ii(n), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n), ∀ n1. x[ii(n1)] = lf(n1).last, ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1) ⊦ ∃ n1. ii(n1) + 1 = # x ∧ (∀ m. n1 ≤ m → nextl(m, x[ii(m)]) = x[ii(m)] ' ∧ ii(n1) = ii(m))

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 ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ # x = 0 ↔ x = []; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ⊦ ⌜x⌝ [n] = x[n]; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; (s) ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ finp(⌜x⌝ ); (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as)

Proof step 35 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 36:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, x[ii(n0)] = lf(n0).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, x[ii(n0)]), nextl(0, a) = a ' + x0, (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), x to ii(1) + 1 = nextl(0, a), lf(n0) ≠ [], nextl(0, a) ≠ [], x ≠ [], ii(1) < # x, ii(n0 + 1) < # x, a ∈ nextl(0, a), ii(n0 + 1) ≤ ii(n), ii(1) ≤ ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1), ∀ n1. x[ii(n1)] = lf(n1).last, ∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ ii(n) + 1 = # x ∧ (∀ m. n ≤ m → nextl(m, x[ii(m)]) = x[ii(m)] ' ∧ ii(n) = ii(m))

Rule argument

Additional information

Used terms: n

Proof step 36 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, x[ii(n0)] = lf(n0).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, x[ii(n0)]), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, x to ii(1) + 1 = nextl(0, a), (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), lf(n0) ≠ [], nextl(0, a) ≠ [], x ≠ [], ii(n0 + 1) < # x, ii(1) < # x, a ∈ nextl(0, a), ii(1) ≤ ii(n), ii(n0 + 1) ≤ ii(n), n ≤ m, ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n), ∀ n1. x[ii(n1)] = lf(n1).last, ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1) ⊦ nextl(m, x[ii(m)]) = x[ii(m)] ' ∧ ii(n) = ii(m)

Rule argument

Additional information

Proof step 37 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 38:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, x[ii(n0)] = lf(n0).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, x[ii(n0)]), lf(m + 1) = nextl(m, lf(m).last), nextl(0, a) = a ' + x0, (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), x to ii(1) + 1 = nextl(0, a), lf(m) ≠ [], lf(n0) ≠ [], nextl(0, a) ≠ [], x ≠ [], ii(1) < # x, ii(n0 + 1) < # x, a ∈ nextl(0, a), n ≤ m, ii(n0 + 1) ≤ ii(n), ii(1) ≤ ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1), ∀ n1. x[ii(n1)] = lf(n1).last, ∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ nextl(m, x[ii(m)]) = x[ii(m)] ' ∧ ii(n) = ii(m)

Rule argument

Additional information

Used terms: m

Proof step 38 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, x[ii(n0)] = lf(n0).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(m + 1) = nextl(m, lf(m).last), lf(n0 + 1) = nextl(n0, x[ii(n0)]), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, x to ii(1) + 1 = nextl(0, a), (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), lf(m) ≠ [], lf(n0) ≠ [], nextl(0, a) ≠ [], x ≠ [], ii(n0 + 1) < # x, ii(1) < # x, a ∈ nextl(0, a), ii(1) ≤ ii(n), ii(n0 + 1) ≤ ii(n), n ≤ m, ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n), ∀ n1. x[ii(n1)] = lf(n1).last, ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1) ⊦ nextl(m, x[ii(m)]) = x[ii(m)] ' ∧ ii(n) = ii(m)

Rule argument

Additional information

Proof step 39 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 40:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, x[ii(n0)] = lf(n0).last, x[ii(m)] = lf(m).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, x[ii(n0)]), lf(m + 1) = nextl(m, lf(m).last), nextl(0, a) = a ' + x0, (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), x to ii(1) + 1 = nextl(0, a), lf(m) ≠ [], lf(n0) ≠ [], nextl(0, a) ≠ [], x ≠ [], ii(1) < # x, ii(n0 + 1) < # x, a ∈ nextl(0, a), n ≤ m, ii(n0 + 1) ≤ ii(n), ii(1) ≤ ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1), ∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ nextl(m, x[ii(m)]) = x[ii(m)] ' ∧ ii(n) = ii(m)

Rule argument

Additional information

Used terms: m

Proof step 40 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, x[ii(m)] = lf(m).last, x[ii(n0)] = lf(n0).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(m + 1) = nextl(m, x[ii(m)]), lf(n0 + 1) = nextl(n0, x[ii(n0)]), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, x to ii(1) + 1 = nextl(0, a), (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), lf(m) ≠ [], lf(n0) ≠ [], nextl(0, a) ≠ [], x ≠ [], ii(n0 + 1) < # x, ii(1) < # x, a ∈ nextl(0, a), ii(1) ≤ ii(n), ii(n0 + 1) ≤ ii(n), n ≤ m, ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1) ⊦ lf(m + 1) = x[ii(m)] ' ∧ ii(n) = ii(m)

Rule argument

Additional information

Proof step 41 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 42:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, x[ii(n0)] = lf(n0).last, x[ii(m)] = lf(m).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, x[ii(n0)]), lf(m + 1) = nextl(m, x[ii(m)]), nextl(0, a) = a ' + x0, (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), x to ii(1) + 1 = nextl(0, a), lf(m) ≠ [], lf(n0) ≠ [], nextl(0, a) ≠ [], x ≠ [], ii(1) < # x, ii(n0 + 1) < # x, a ∈ nextl(0, a), n ≤ m, ii(n0 + 1) ≤ ii(n), ii(1) ≤ ii(n), n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ lf(m + 1) = x[ii(m)] ' ∧ ii(n) = ii(m)

Rule argument

Additional information

Used terms: m

Proof step 42 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, lf(m + 1).tail = [], x[ii(n)] = lf(m).last, x[ii(n0)] = lf(n0).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(m) = ii(n), lf(m + 1) = nextl(m, x[ii(n)]), lf(n0 + 1) = nextl(n0, x[ii(n0)]), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, x to ii(1) + 1 = nextl(0, a), (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), lf(m) ≠ [], lf(n0) ≠ [], lf(m + 1) ≠ x[ii(n)] ', nextl(0, a) ≠ [], x ≠ [], ii(n0 + 1) < # x, ii(1) < # x, a ∈ nextl(0, a), ii(1) ≤ ii(n), ii(n0 + 1) ≤ ii(n), n ≤ m, ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1) ⊦

Rule argument

Additional information

Proof step 43 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 44:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, lf(m + 1).tail = [], x[ii(n0)] = lf(n0).last, x[ii(n)] = lf(m).last, ii(m) = ii(n), ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(m + 1) = [], lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, x[ii(n0)]), lf(m + 1) = nextl(m, x[ii(n)]), nextl(0, a) = a ' + x0, (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), x to ii(1) + 1 = nextl(0, a), lf(m) ≠ [], lf(n0) ≠ [], lf(m + 1) ≠ x[ii(n)] ', nextl(0, a) ≠ [], x ≠ [], ii(1) < # x, ii(n0 + 1) < # x, a ∈ nextl(0, a), n ≤ m, ii(n0 + 1) ≤ ii(n), ii(1) ≤ ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦

• Proof step 46:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, x[ii(n0)] = lf(n0).last, x[ii(n)] = lf(m).last, ii(m) = ii(n), ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, x[ii(n0)]), lf(m + 1) = nextl(m, x[ii(n)]), lf(m + 1) = a0 + x1, nextl(0, a) = a ' + x0, (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), x to ii(1) + 1 = nextl(0, a), x1 = [], lf(m + 1) ≠ [], lf(m) ≠ [], lf(n0) ≠ [], lf(m + 1) ≠ x[ii(n)] ', nextl(0, a) ≠ [], x ≠ [], ii(1) < # x, ii(n0 + 1) < # x, a ∈ nextl(0, a), n ≤ m, ii(n0 + 1) ≤ ii(n), ii(1) ≤ ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → (head = x.head ∧ tail = x.tail ↔ x = head + tail); (elim) Used terms: lf(m + 1), head, tail

Proof step 44 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  # nextl(0, a) = ii(1) + 1, ii(n) + 1 = # x, [].tail = [], [] = nextl(m, x[ii(n)]), x[ii(n0)] = lf(n0).last, x[ii(n)] = lf(m).last, ii(m) = ii(n), ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(m + 1) = [], lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, x[ii(n0)]), nextl(0, a) = a ' + x0, (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), x to ii(1) + 1 = nextl(0, a), lf(n0) ≠ [], lf(m) ≠ [], nextl(0, a) ≠ [], x ≠ [], ii(1) < # x, ii(n0 + 1) < # x, a ∈ nextl(0, a), n ≤ m, ii(n0 + 1) ≤ ii(n), ii(1) ≤ ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s)

Proof step 45 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m + 1

Proof step 46 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  # nextl(0, a) = ii(1) + 1, a0 ' = nextl(m, x[ii(n)]), ii(n) + 1 = # x, x[ii(n0)] = lf(n0).last, x[ii(n)] = lf(m).last, ii(m) = ii(n), ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(m + 1) = a0 ', lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, x[ii(n0)]), nextl(0, a) = a ' + x0, (x from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), x to ii(1) + 1 = nextl(0, a), a0 ≠ x[ii(n)], lf(n0) ≠ [], lf(m) ≠ [], nextl(0, a) ≠ [], x ≠ [], ii(1) < # x, ii(n0 + 1) < # x, a ∈ nextl(0, a), n ≤ m, ii(n0 + 1) ≤ ii(n), ii(1) ≤ ii(n), ∀ n1. ii(n1 + 1) = ii(n1) + # lf(n1 + 1) - 1 ∧ ii(n1 + 1) < # x ∧ (x from ii(n1)) to # lf(n1 + 1) = lf(n1 + 1), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ []; (s) ⊦ a ' = a0 ' ↔ a = a0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ a + x = a ' + x; (s)

Proof step 47 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a '.head = a; (s) Used terms: m, x[ii(n)]

Proof step 48 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  # nextl(0, a) = ii(1) + 1, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, nf(ii(n0)) = lf(n0).last, nf to ii(1) + 1 = nextl(0, a), (nf from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), lf(n0) ≠ [], nextl(0, a) ≠ [], a ∈ nextl(0, a), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. nf(ii(n)) = lf(n).last, ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ (nf from ii(n)) to # lf(n + 1) = lf(n + 1) ⊦ ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; (s) ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; (s) ⊦ ⌜m⌝ < ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ ¬ finp(⌜nf⌝ ); (s) ⊦ [] ≠ ⌜nf⌝ ; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) ⊦ ¬ finp(σ) → # σ = ∞; (s)

Proof step 49 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 50:

  # nextl(0, a) = ii(1) + 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, nf(ii(n0)) = lf(n0).last, (nf from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), nf to ii(1) + 1 = nextl(0, a), lf(n0) ≠ [], nextl(0, a) ≠ [], a ∈ nextl(0, a), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ (nf from ii(n)) to # lf(n + 1) = lf(n + 1), ∀ n. nf(ii(n)) = lf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1) ⊦ ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)

Rule argument

Additional information

Used terms: n1

Proof step 50 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  # nextl(0, a) = ii(1) + 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, nf(ii(n0)) = lf(n0).last, (nf from ii(n0)) to # lf(n0 + 1) = lf(n0 + 1), nf to ii(1) + 1 = nextl(0, a), lf(n0) ≠ [], nextl(0, a) ≠ [], ii(m) < ii(m + 1), n1 < ii(m + 1), a ∈ nextl(0, a), ii(m) ≤ n1, ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ (nf from ii(n)) to # lf(n + 1) = lf(n + 1), ∀ n. nf(ii(n)) = lf(n).last, ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)

Rule argument

Additional information

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

Proof step 51 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: m

Proof step 52 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a '.last = a; (s) Used terms: 0

Proof step 53 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  # nextl(0, a) = ii(1) + 1, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Proof step 54 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 55:

  # nextl(0, a) = ii(1) + 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n2)) to # lf(n2 + 1) = ⌜lf(n2 + 1)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n2 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: n2

Proof step 55 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  # nextl(0, a) = ii(1) + 1, ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, (σ from ii(n2)) to # lf(n2 + 1) = ⌜lf(n2 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n2 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Proof step 56 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

  ⊦ σ0 = σ1 ↔ # σ0 = # σ1 ∧ (∀ n. ⌜n⌝ < # σ0 → σ0[n] = σ1[n])

• Proof step 58:

  #((σ from ii(n2)) to # lf(n2 + 1)) = # ⌜lf(n2 + 1)⌝ , # nextl(0, a) = ii(1) + 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n2 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. ⌜n⌝ < #((σ from ii(n2)) to # lf(n2 + 1)) → ((σ from ii(n2)) to # lf(n2 + 1))[n] = ⌜lf(n2 + 1)⌝ [n] ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: ⌜lf(n2 + 1)⌝ , (σ from ii(n2)) to # lf(n2 + 1)

Proof step 57 from proof diag-theorem-butlast (previous step) (back to tree)

A spec-lemma

Proof step 58 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , # nextl(0, a) = ii(1) + 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n2 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n3. n3 < # lf(n2 + 1) → ((σ from ii(n2)) to # lf(n2 + 1))[n3] = lf(n2 + 1)[n3] ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s)

Proof step 59 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 60:

  # nextl(0, a) = ii(1) + 1, #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n2 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), 0 < # lf(n2 + 1) → ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2 + 1)[0], (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: 0

Proof step 60 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , # nextl(0, a) = ii(1) + 1, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n2 + 1)⌝ < # σ, a ∈ nextl(0, a), lf(n2 + 1) ≠ [] → ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2 + 1).head, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: ⊦ x ≠ [] → x[0] = x.head; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 61 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 62:

  # nextl(0, a) = ii(1) + 1, #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), lf(n2 + 1) = nextl(n2, lf(n2).last), nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n2 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), lf(n2 + 1) ≠ [] → ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2 + 1).head, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: n2

Proof step 62 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 63:

  #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , # nextl(0, a) = ii(1) + 1, nextl(n2, lf(n2).last).head = lf(n2).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, lf(n2 + 1) = nextl(n2, lf(n2).last), lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], nextl(n2, lf(n2).last) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n2 + 1)⌝ < # σ, a ∈ nextl(0, a), lf(n2 + 1) ≠ [] → ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2 + 1).head, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: n2, lf(n2).last

Proof step 63 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , # nextl(0, a) = ii(1) + 1, lf(n2 + 1).head = lf(n2).last, ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, lf(n2 + 1) = nextl(n2, lf(n2).last), lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n2 + 1) ≠ [], lf(n0) ≠ [], lf(n2) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n2 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Proof step 64 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 65:

  # nextl(0, a) = ii(1) + 1, #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , ii(n2) + # lf(n2 + 1) = m0 + 1, lf(n2 + 1).head = lf(n2).last, ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2).last, ii(n2 + 1) = m0, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), lf(n2 + 1) = nextl(n2, lf(n2).last), nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , ii(n2) + # lf(n2 + 1) ≠ 0, σ[ii(n2)] ≠ lf(n2).last, lf(n2 + 1) ≠ [], lf(n0) ≠ [], lf(n2) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n2 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: ii(n2) + # lf(n2 + 1), m0

Proof step 65 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  # nextl(0, a) = ii(1) + 1, #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, lf(n2 + 1).head = lf(n2).last, ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), lf(n2 + 1) = nextl(n2, lf(n2).last), nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], lf(n2 + 1) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n2 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

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 ⊦ m + 1 ≠ 0; (s)

Proof step 66 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 67:

  #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , # nextl(0, a) = ii(1) + 1, ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2).last, a0 = lf(n2).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(n2 + 1) = nextl(n2, lf(n2).last), lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), lf(n2 + 1) = a0 + x1, nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], lf(n2 + 1) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n2 + 1)⌝ < # σ, a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: lf(n2 + 1), a0, y

Proof step 67 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  # nextl(0, a) = ii(1) + 1, #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n2 + 1) = lf(n2).last ' + x1, nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], lf(n2 + 1) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n2 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), lf(n2).last ∈ lf(n2 + 1), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s)

Proof step 68 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  m < n, ¬ # σ < ⌜n⌝ ⊦ (σ to n)[m] = σ[m]

• Proof step 70:

  #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , # nextl(0, a) = ii(1) + 1, ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(n2 + 1) = lf(n2).last ' + x1, lf(n2 + 1) = nextl(n2, lf(n2).last), lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], lf(n2 + 1) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n2 + 1)⌝ < # σ, lf(n2).last ∈ lf(n2 + 1), a ∈ nextl(0, a), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a, 0 < # lf(n2 + 1) ∧ ¬ #(σ from ii(n2)) < ⌜# lf(n2 + 1)⌝

• Proof step 72:

  #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , # nextl(0, a) = ii(1) + 1, ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, (σ from ii(n2))[0] = lf(n2).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, lf(n2 + 1) = lf(n2).last ' + x1, lf(n2 + 1) = nextl(n2, lf(n2).last), lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), nextl(0, a) = a ' + x0, (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], lf(n2 + 1) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n2 + 1)⌝ < # σ, 0 < # lf(n2 + 1), lf(n2).last ∈ lf(n2 + 1), a ∈ nextl(0, a), ¬ #(σ from ii(n2)) < ⌜# lf(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used terms: 0, # lf(n2 + 1), σ from ii(n2)

Proof step 69 from proof diag-theorem-butlast (previous step) (back to tree)

A spec-lemma

Proof step 70 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  # nextl(0, a) = ii(1) + 1, #((σ from ii(n2)) to # lf(n2 + 1)) = ⌜# lf(n2 + 1)⌝ , ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, ((σ from ii(n2)) to # lf(n2 + 1))[0] = lf(n2).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n2 + 1) = lf(n2).last ' + x1, nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], lf(n2 + 1) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n2 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, #(σ from ii(n2)) < ⌜# lf(n2 + 1)⌝ , a ∈ nextl(0, a), lf(n2).last ∈ lf(n2 + 1), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 71 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule structural induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) m < n ⊦ (nf to n)[m] = nf(m); (s) ⊦ ((nf from n))(0) = nf(n); (s) ⊦ ⌜nf⌝ from n = ⌜nf from n⌝ ; (s) ⊦ ⌜nf⌝ to n = ⌜nf to n⌝ ; (s) ⊦ # ⌜nf to n⌝ = ⌜n⌝ ; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ finp(⌜x⌝ ); (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf ⊦ ⌜x⌝ from n = ⌜x from n⌝ ; (s) ⊦ ⌜x⌝ to n = ⌜x to n⌝ ; (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ¬ # x < n ⊦ #(x from n) = # x - n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n ↔ ¬ n ≤ m; (ss) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ x ≠ [] → x[0] = x.head; (s) ⊦ m < n → n ≠ 0; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ m + n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s)

Proof step 72 from proof diag-theorem-butlast (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 73:

  # nextl(0, a) = ii(1) + 1, ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, (σ from ii(n2))[0] = lf(n2).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n2 + 1) = lf(n2).last ' + x1, nextl(0, a) = a ' + x0, σ to ii(1) + 1 = ⌜nextl(0, a)⌝ , (σ from ii(n0)) to # lf(n0 + 1) = ⌜lf(n0 + 1)⌝ , σ[ii(n2)] ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], lf(n2 + 1) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n2 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), lf(n2).last ∈ lf(n2 + 1), ¬ #(σ from ii(n2)) < ⌜# lf(n2 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → lf(m + 1).tail = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).head = a, ∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ [], ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n + 1) = ⌜lf(n + 1)⌝ ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ + ⌜1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)) ∧ (σ from ii(n0)) to # nextl(n0, σ[ii(n0)]) = ⌜nextl(n0, σ[ii(n0)])⌝ ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ[ii(n0)]) - 1 ∧ σ[0] = a

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ¬ # σ < ⌜n⌝ ⊦ #(σ to n) = ⌜n⌝ ; (s)

Proof step 73 from proof diag-theorem-butlast (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 74:

  ⊦ ⌜n⌝ + ⌜m⌝ < # σ → (σ from n)[m] = σ[n + m]

Rule argument

Additional information

Used simplifier rules: ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ n∞ + ⌜0⌝ = n∞; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf lsle-trans: ⊦ n∞ < n∞1 ∧ ¬ n∞2 < n∞1 → n∞ < n∞2; (forward) from specification nat-inf ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as) ⊦ ¬ finp(σ) → # σ = ∞; (s) ⊦ ⌜m⌝ < ∞; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list a: ⊦ (x + y) + z = x + y + z; from specification list eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m + m0 ≤ m ↔ m0 = 0; (s) ⊦ # x = 0 ↔ x = []; (s) Used terms: 0, ii(n2), σ

Proof step 74 from proof diag-theorem-butlast (previous step) (back to tree)

A spec-lemma