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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n0)).take(# 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 ', σ.drop(ii(0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# lf(n + 1)) = lf(n + 1) ⊦ σ(0) = a ∧ σ ≠ [] ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ(ii(n0))) - 1 ∧ ⌜ii(n0 + 1)⌝ < # σ ∧ σ.drop(ii(n0)).take(# 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 ', σ.take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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) ⊦ σ.drop(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), σ.take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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 ', σ.take(# lf(1)) = lf(1), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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), σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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), σ.take(# lf(1)) = lf(1), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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), σ.take(# nextl(0, a)) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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), σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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), σ.take(# nextl(0, a)) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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), σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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), σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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.take(ii(1) + 1) = nextl(0, a), x.drop(ii(n0)).take(# 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.drop(ii(n1)).take(# 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⌝ .take(n) = x.take(n); (s) ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(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.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), x.take(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.drop(ii(n1)).take(# 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.take(ii(1) + 1) = nextl(0, a), x.drop(ii(n0)).take(# 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.drop(ii(n1)).take(# 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.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), x.take(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.drop(ii(n1)).take(# 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.take(ii(1) + 1) = nextl(0, a), x.drop(ii(n0)).take(# 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.drop(ii(n1)).take(# 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.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), x.take(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.drop(ii(n1)).take(# 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.take(ii(1) + 1) = nextl(0, a), x.drop(ii(n0)).take(# 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.drop(ii(n1)).take(# 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.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), x.take(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.drop(ii(n1)).take(# 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.take(ii(1) + 1) = nextl(0, a), x.drop(ii(n0)).take(# 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.drop(ii(n1)).take(# 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.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), x.take(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.drop(ii(n1)).take(# 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.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), x.take(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.drop(ii(n1)).take(# 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.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), x.take(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.drop(ii(n1)).take(# 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.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), x.take(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.drop(ii(n1)).take(# 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.take(ii(1) + 1) = nextl(0, a), nf.drop(ii(n0)).take(# 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.drop(ii(n)).take(# lf(n + 1)) = lf(n + 1) ⊦ ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)

Rule argument

Additional information

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

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.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), nf.take(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.drop(ii(n)).take(# 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.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), nf.take(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.drop(ii(n)).take(# 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, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n2)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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, σ.drop(ii(n2)).take(# lf(n2 + 1)) = lf(n2 + 1), σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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:

  ⊦ x = y ↔ # x = # y ∧ (∀ n. n < # x → x(n) = y(n))

• Proof step 58:

  # σ.drop(ii(n2)).take(# 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, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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 < # σ.drop(ii(n2)).take(# lf(n2 + 1)) → σ.drop(ii(n2)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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: σ.drop(ii(n2)).take(# lf(n2 + 1)), 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:

  # nextl(0, a) = ii(1) + 1, # σ.drop(ii(n2)).take(# 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, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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. n < # lf(n2 + 1) → σ.drop(ii(n2)).take(# lf(n2 + 1))(n) = lf(n2 + 1)(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), ∀ n. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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 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:

  # σ.drop(ii(n2)).take(# 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, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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), 0 < # lf(n2 + 1) → σ.drop(ii(n2)).take(# 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. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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:

  # nextl(0, a) = ii(1) + 1, # σ.drop(ii(n2)).take(# 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, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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), lf(n2 + 1) ≠ [] → σ.drop(ii(n2)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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:

  # σ.drop(ii(n2)).take(# 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), lf(n2 + 1) = nextl(n2, lf(n2).last), nextl(0, a) = a ' + x0, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(ii(1) + 1) = nextl(0, a), σ(ii(n2)) ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n0 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n2 + 1)⌝ < # σ, a ∈ nextl(0, a), lf(n2 + 1) ≠ [] → σ.drop(ii(n2)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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:

  # nextl(0, a) = ii(1) + 1, # σ.drop(ii(n2)).take(# lf(n2 + 1)) = # lf(n2 + 1), nextl(n2, lf(n2).last).head = lf(n2).last, ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ(ii(n2)) ≠ lf(n2).last, lf(n2) ≠ [], lf(n0) ≠ [], nextl(n2, lf(n2).last) ≠ [], nextl(0, a) ≠ [], σ ≠ [], ⌜ii(n2 + 1)⌝ < # σ, ⌜ii(1)⌝ < # σ, ⌜ii(n0 + 1)⌝ < # σ, a ∈ nextl(0, a), lf(n2 + 1) ≠ [] → σ.drop(ii(n2)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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:

  # nextl(0, a) = ii(1) + 1, # σ.drop(ii(n2)).take(# lf(n2 + 1)) = # lf(n2 + 1), lf(n2 + 1).head = lf(n2).last, σ.drop(ii(n2)).take(# lf(n2 + 1))(0) = lf(n2).last, ii(n2 + 1) = ii(n2) + # lf(n2 + 1) - 1, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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:

  # σ.drop(ii(n2)).take(# lf(n2 + 1)) = # lf(n2 + 1), # nextl(0, a) = ii(1) + 1, ii(n2) + # lf(n2 + 1) = m0 + 1, lf(n2 + 1).head = lf(n2).last, σ.drop(ii(n2)).take(# lf(n2 + 1))(0) = lf(n2).last, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, ii(0) = 0, ii(n2 + 1) = m0, lf(1) = nextl(0, a), lf(0) = a ', lf(n0 + 1) = nextl(n0, lf(n0).last), lf(n2 + 1) = nextl(n2, lf(n2).last), nextl(0, a) = a ' + x0, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(ii(1) + 1) = nextl(0, a), ii(n2) + # lf(n2 + 1) ≠ 0, σ(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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:

  # σ.drop(ii(n2)).take(# lf(n2 + 1)) = # lf(n2 + 1), # nextl(0, a) = ii(1) + 1, ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, lf(n2 + 1).head = lf(n2).last, σ.drop(ii(n2)).take(# lf(n2 + 1))(0) = lf(n2).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, lf(n0).last), lf(n2 + 1) = nextl(n2, lf(n2).last), nextl(0, a) = a ' + x0, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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:

  # nextl(0, a) = ii(1) + 1, # σ.drop(ii(n2)).take(# lf(n2 + 1)) = # lf(n2 + 1), ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, σ.drop(ii(n2)).take(# lf(n2 + 1))(0) = lf(n2).last, a0 = lf(n2).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), lf(n2 + 1) = a0 + x1, nextl(0, a) = a ' + x0, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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:

  # σ.drop(ii(n2)).take(# lf(n2 + 1)) = # lf(n2 + 1), # nextl(0, a) = ii(1) + 1, ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, σ.drop(ii(n2)).take(# lf(n2 + 1))(0) = lf(n2).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, lf(n0).last), lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n2 + 1) = lf(n2).last ' + x1, nextl(0, a) = a ' + x0, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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), 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. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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⌝ ⊦ σ.take(n)(m) = σ(m)

• Proof step 70:

  # nextl(0, a) = ii(1) + 1, # σ.drop(ii(n2)).take(# lf(n2 + 1)) = # lf(n2 + 1), ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, σ.drop(ii(n2)).take(# lf(n2 + 1))(0) = lf(n2).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n2 + 1) = lf(n2).last ' + x1, lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ, 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, 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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# nextl(n0, σ(ii(n0)))) = nextl(n0, σ(ii(n0))) ∧ ii(n0 + 1) = ii(n0) + # nextl(n0, σ(ii(n0))) - 1 ∧ σ(0) = a, 0 < # lf(n2 + 1) ∧ ¬ # σ.drop(ii(n2)) < ⌜# lf(n2 + 1)⌝

• Proof step 72:

  # nextl(0, a) = ii(1) + 1, # σ.drop(ii(n2)).take(# lf(n2 + 1)) = # lf(n2 + 1), ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, σ.drop(ii(n2))(0) = lf(n2).last, ii(0) = 0, ii(n0 + 1) = ii(n0) + # lf(n0 + 1) - 1, lf(n2 + 1) = lf(n2).last ' + x1, lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n0 + 1) = nextl(n0, lf(n0).last), lf(0) = a ', lf(1) = nextl(0, a), nextl(0, a) = a ' + x0, σ.take(ii(1) + 1) = nextl(0, a), σ.drop(ii(n0)).take(# 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)⌝ < # σ, 0 < # lf(n2 + 1), lf(n2).last ∈ lf(n2 + 1), a ∈ nextl(0, a), ¬ # σ.drop(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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: σ.drop(ii(n2)), # lf(n2 + 1), 0

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:

  # σ.drop(ii(n2)).take(# lf(n2 + 1)) = # lf(n2 + 1), # nextl(0, a) = ii(1) + 1, ii(n2) + # lf(n2 + 1) = ii(n2 + 1) + 1, σ.drop(ii(n2)).take(# lf(n2 + 1))(0) = lf(n2).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, lf(n0).last), lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n2 + 1) = lf(n2).last ' + x1, nextl(0, a) = a ' + x0, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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)⌝ < # σ, # σ.drop(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. ii(n + 1) = ii(n) + # lf(n + 1) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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 ⌝, ⌝; ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) m < n ⊦ nf.take(n)(m) = nf(m); (s) ⊦ nf.drop(n)(0) = nf(n); (s) ⊦ ⌜nf⌝ .drop(n) = ⌜nf.drop(n)⌝ ; (s) ⊦ ⌜nf⌝ .take(n) = nf.take(n); (s) ⊦ # nf.take(n) = n; (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⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) ⊦ ⌜x⌝ .take(n) = x.take(n); (s) ⊦ ⌜x⌝ (n) = x(n); (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ¬ # x < n ⊦ # x.drop(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, σ.drop(ii(n2))(0) = lf(n2).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, lf(n0).last), lf(n2 + 1) = nextl(n2, lf(n2).last), lf(n2 + 1) = lf(n2).last ' + x1, nextl(0, a) = a ' + x0, σ.drop(ii(n0)).take(# lf(n0 + 1)) = lf(n0 + 1), σ.take(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), lf(n2).last ∈ lf(n2 + 1), ¬ # σ.drop(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)⌝ < # σ ∧ σ.drop(ii(n)).take(# 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)) ∧ σ.drop(ii(n0)).take(# 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⌝ ⊦ # σ.take(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⌝ < # σ → σ.drop(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(σ) ↔ ¬(∃ 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