Proof step 1 from proof infinite-append-prefixnextnli (conclusion) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 2:

  ∀ x, n. x ⊑ nextnli(x, n), ∀ x, n. ∃ y. nextnli(x, n) = x + y ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

• Proof step 97:

  ∀ x, n. x ⊑ nextnli(x, n) ⊦ ∀ x, n. ∃ y. nextnli(x, n) = x + y, ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Used formulas: ∀ x, n. ∃ y. nextnli(x, n) = x + y

Proof step 2 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule choice left

And obtained the following new goals

• Proof step 3:

  ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ x, n. x ⊑ nextnli(x, n) ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Proof step 3 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 4:

  ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Proof step 4 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

  ⊦ ∃ lf. lf(0) = x ∧ (∀ n. lf(n + 1) = nextnli(lf(n), n))

• Proof step 6:

  ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∃ lf. lf(0) = [] ∧ (∀ n. lf(n + 1) = nextnli(lf(n), n)) ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Used terms: [], nextnli

Proof step 5 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Lemma nextnli-lemma

Proof step 6 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  lf(0) = [], ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Proof step 7 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 8:

  ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# lf(n)) = ⌜lf(n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

• Proof step 9:

  lf(0) = [], ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Used terms: λ n. nextnli0(lf(n), n)

Proof step 8 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ii(0) = 0, lf(0) = [], (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Proof step 10 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 11:

  ii(0) = 0, lf(0) = [], (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ ⊦ ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Used terms: σ, ii

Proof step 11 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ii(0) = 0, lf(0) = [], (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦ ii(n0) ≤ ii(n0 + 1) ∧ ¬ # σ < ⌜ii(n0 + 1)⌝ ∧ σ.take(ii(n0 + 1)) = ⌜nextnli((σ.take(ii(n0))).l, n0)⌝ ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

Rule argument

Additional information

Proof step 12 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 13:

  ii(0) = 0, lf(0) = [], (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l ⊦ ii(n0) ≤ ii(n0 + 1) ∧ ¬ # σ < ⌜ii(n0 + 1)⌝ ∧ σ.take(ii(n0 + 1)) = ⌜nextnli((σ.take(ii(n0))).l, n0)⌝ ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

• Proof step 55:

  ii(0) = 0, lf(0) = [], (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ ⊦ ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ii(n0) ≤ ii(n0 + 1) ∧ ¬ # σ < ⌜ii(n0 + 1)⌝ ∧ σ.take(ii(n0 + 1)) = ⌜nextnli((σ.take(ii(n0))).l, n0)⌝ ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

Rule argument

Additional information

Used formulas: ∀ n0. lf(n0) = (σ.take(ii(n0))).l

Proof step 13 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  ii(0) = 0, lf(0) = [], ¬ ii(n0) ≤ ii(n0 + 1), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

• Proof step 16:

  ii(0) = 0, lf(0) = [], # σ < ⌜ii(n0 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

• Proof step 18:

  ii(0) = 0, lf(0) = [], σ.take(ii(n0 + 1)) ≠ ⌜nextnli((σ.take(ii(n0))).l, n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

• Proof step 37:

  ii(0) = 0, lf(0) = [], (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

Rule argument

Additional information

Proof step 14 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ii(0) = 0, lf(0) = [], ii(n0 + 1) < ii(n0), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

Rule argument

Additional information

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

Proof step 15 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m + n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: n0, n0 + 1

Proof step 16 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  # σ = ⌜ii(n)⌝ , ii(0) = 0, lf(0) = [], ii(n) < ii(n0 + 1), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ ¬ ∞ < n∞; (s) ⊦ ¬ finp(σ) → # σ = ∞; (s)

Proof step 17 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: n0

Proof step 18 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 19:

  ii(0) = 0, lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, σ.take(ii(n0 + 1)) ≠ ⌜nextnli((σ.take(ii(n0))).l, n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l ⊦

Rule argument

Additional information

Used terms: n0

Proof step 19 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  ii(0) = 0, lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], σ.take(ii(n0 + 1)) ≠ ⌜nextnli(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

Rule argument

Additional information

Proof step 20 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 21:

  ii(0) = 0, lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, lf(n0 + 1) = (σ.take(ii(n0 + 1))).l, σ.take(ii(n0 + 1)) ≠ ⌜nextnli(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l ⊦

Rule argument

Additional information

Used terms: n0 + 1

Proof step 21 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

  ii(0) = 0, lf(n0 + 1) = (σ.take(ii(n0 + 1))).l, lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], lf(n0 + 1) = nextnli(lf(n0), n0), σ.take(ii(n0 + 1)) ≠ ⌜nextnli(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 22 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ii(0) = 0, lf(n0 + 1) = nextnli(lf(n0), n0), lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, nextnli(lf(n0), n0) = (σ.take(ii(n0 + 1))).l, σ.take(ii(n0 + 1)) ≠ ⌜nextnli(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l ⊦

Rule argument

Additional information

Proof step 23 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  ii(0) = 0, lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], lf(n0 + 1) = nextnli(lf(n0), n0), nextnli(lf(n0), n0) = (σ.take(ii(n0 + 1))).l, nextnli(lf(n0), n0) = lf(n0) + nextnli0(lf(n0), n0), σ.take(ii(n0 + 1)) ≠ ⌜nextnli(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

Rule argument

Additional information

Used terms: lf(n0), n0

Proof step 24 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 25:

  (σ.take(ii(n0 + 1))).l = lf(n0) + nextnli0(lf(n0), n0), ii(0) = 0, lf(n0 + 1) = (σ.take(ii(n0 + 1))).l, lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, σ.take(ii(n0 + 1)) ≠ ⌜(σ.take(ii(n0 + 1))).l⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l ⊦

Rule argument

Additional information

Proof step 25 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  (σ.take(ii(n0 + 1))).l = lf(n0 + 1), ii(0) = 0, lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), σ.take(ii(n0 + 1)) ≠ ⌜lf(n0 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

Rule argument

Additional information

Proof step 26 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

  (σ.take(ii(n0 + 1))).l = lf(n0 + 1), ii(0) = 0, lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l, # σ.take(ii(n0 + 1)) ≠ # ⌜lf(n0 + 1)⌝ ∨ (∃ n. ¬(⌜n⌝ < # σ.take(ii(n0 + 1)) → σ.take(ii(n0 + 1))[n] = ⌜lf(n0 + 1)⌝ [n])) ⊦

Rule argument

Additional information

Used terms: ⌜lf(n0 + 1)⌝ , σ.take(ii(n0 + 1))

Proof step 27 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  (σ.take(ii(n0 + 1))).l = lf(n0 + 1), ii(0) = 0, lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), # σ.take(ii(n0 + 1)) ≠ ⌜# lf(n0 + 1)⌝ ∨ ¬(⌜n1⌝ < # σ.take(ii(n0 + 1)) → σ.take(ii(n0 + 1))[n1] = lf(n0 + 1)[n1]) ⊦

Rule argument

Additional information

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

Proof step 29 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

• Proof step 31:

  # (σ.take(ii(n0 + 1))).l = # lf(n0 + 1), ii(0) = 0, lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. n < # (σ.take(ii(n0 + 1))).l → (σ.take(ii(n0 + 1))).l[n] = lf(n0 + 1)[n], # σ.take(ii(n0 + 1)) ≠ ⌜# lf(n0 + 1)⌝ ∨ ¬(⌜n1⌝ < # σ.take(ii(n0 + 1)) → σ.take(ii(n0 + 1))[n1] = lf(n0 + 1)[n1]) ⊦

Rule argument

Additional information

Used terms: lf(n0 + 1), (σ.take(ii(n0 + 1))).l

Proof step 30 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  # (σ.take(ii(n0 + 1))).l = # lf(n0 + 1), ii(0) = 0, lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. n < # lf(n0 + 1) → (σ.take(ii(n0 + 1))).l[n] = lf(n0 + 1)[n], ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), # σ.take(ii(n0 + 1)) ≠ ⌜# lf(n0 + 1)⌝ ∨ ¬(⌜n1⌝ < # σ.take(ii(n0 + 1)) → σ.take(ii(n0 + 1))[n1] = lf(n0 + 1)[n1]) ⊦

Rule argument

Additional information

Proof step 32 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 33:

  # (σ.take(ii(n0 + 1))).l = # lf(n0 + 1), # σ = ⌜ii(n)⌝ , ii(0) = 0, lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, finp(σ), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. n < # lf(n0 + 1) → (σ.take(ii(n0 + 1))).l[n] = lf(n0 + 1)[n], ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), # σ.take(ii(n0 + 1)) ≠ ⌜# lf(n0 + 1)⌝ ∨ ¬(⌜n1⌝ < # σ.take(ii(n0 + 1)) → σ.take(ii(n0 + 1))[n1] = lf(n0 + 1)[n1]) ⊦

• Proof step 35:

  # (σ.take(ii(n0 + 1))).l = # lf(n0 + 1), ii(0) = 0, lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, ¬ finp(σ), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. n < # lf(n0 + 1) → (σ.take(ii(n0 + 1))).l[n] = lf(n0 + 1)[n], ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), # σ.take(ii(n0 + 1)) ≠ ⌜# lf(n0 + 1)⌝ ∨ ¬(⌜n1⌝ < # σ.take(ii(n0 + 1)) → σ.take(ii(n0 + 1))[n1] = lf(n0 + 1)[n1]) ⊦

Rule argument

Additional information

Proof step 33 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  # x = ii(n), # x.take(ii(n0 + 1)) = # lf(n0 + 1), ii(0) = 0, lf(n0) = x.take(ii(n0)), lf(0) = [], lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), x.take(ii(n0 + 1))[n1] ≠ lf(n0 + 1)[n1], lf(n0 + 1) ≠ [], n1 < # lf(n0 + 1), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n2. n2 < # lf(n0 + 1) → x.take(ii(n0 + 1))[n2] = lf(n0 + 1)[n2], ∀ n2. lf(n2) = x.take(ii(n2)), ∀ n2. ii(n2 + 1) = ii(n2) + # nextnli0(lf(n2), n2) ∧ ¬ ii(n) < ii(n2 + 1) ∧ x.drop(ii(n2)).take(# nextnli0(lf(n2), n2)) = nextnli0(lf(n2), n2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ ⌜x⌝ [n] = x[n]; (s) ⊦ ⌜x⌝ .take(n) = ⌜x.take(n)⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ ⌜x⌝ .l = x; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as)

Proof step 34 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n1

Proof step 35 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  ii(n0 + 1) = # lf(n0 + 1), ii(0) = 0, lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), lf(0) = [], lf(n0) = nf.take(ii(n0)), nf(n1) ≠ lf(n0 + 1)[n1], n1 < ii(n0 + 1), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. n < ii(n0 + 1) → nf(n) = lf(n0 + 1)[n], ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ nf.drop(ii(n)).take(# nextnli0(lf(n), n)) = nextnli0(lf(n), n), ∀ n. lf(n) = nf.take(ii(n)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ .l = x; (s) ⊦ ⌜nf⌝ .take(n) = ⌜nf.take(n)⌝ ; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜nf⌝ .drop(n) = ⌜nf.drop(n)⌝ ; (s) ⊦ ¬ ∞ < n∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic m < n, ¬ # σ < ⌜n⌝ ⊦ (σ.take(n)).l[m] = σ[m]; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ # x = 0 ↔ x = []; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) m < n, ¬ # σ < ⌜n⌝ ⊦ σ.take(n)[m] = σ[m]; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ¬ # σ < ⌜n⌝ ⊦ # σ.take(n) = ⌜n⌝ ; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) ¬ # σ < ⌜n⌝ ⊦ # (σ.take(n)).l = n; (s) ⊦ ¬ finp(σ) → # σ = ∞; (s)

Proof step 36 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n1

Proof step 37 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 38:

  # σ = ⌜ii(n)⌝ , ii(0) = 0, lf(0) = [], finp(σ), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n) ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

• Proof step 51:

  ii(0) = 0, lf(0) = [], ¬ finp(σ), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ n0. lf(n0) = (σ.take(ii(n0))).l, ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1) ⊦ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

Rule argument

Additional information

Proof step 38 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  # x = ii(n), ii(0) = 0, lf(0) = [], ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ x.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = nextnli0(lf(n0), n0), ∀ n0. lf(n0) = x.take(ii(n0)) ⊦ ∃ n0. ii(n) = ii(n0) ∧ nextnli(x, n0) = x ∧ (∀ m. n0 ≤ m → ii(m) = ii(n0))

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜x⌝ .l = x; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ finp(⌜x⌝ ); (s) ⊦ ⌜x⌝ .take(n) = ⌜x.take(n)⌝ ; (s) ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as)

Proof step 39 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 40:

  # x = ii(n), ii(0) = 0, lf(0) = [], ∀ n0. lf(n0) = x.take(ii(n0)), ∀ n0. ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ x.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = nextnli0(lf(n0), n0), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦ ii(n) = ii(n) ∧ nextnli(x, n) = x ∧ (∀ m. n ≤ m → ii(m) = ii(n))

Rule argument

Additional information

Used terms: n

Proof step 40 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  # x = ii(n), ii(0) = 0, lf(0) = [], ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ x.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = nextnli0(lf(n0), n0), ∀ n0. lf(n0) = x.take(ii(n0)) ⊦ nextnli(x, n) = x ∧ (n ≤ m → ii(m) = ii(n))

Rule argument

Additional information

Proof step 41 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 42:

  # x = ii(n), ii(0) = 0, lf(0) = [], nextnli(x, n) ≠ x, ∀ n0. lf(n0) = x.take(ii(n0)), ∀ n0. ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ x.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = nextnli0(lf(n0), n0), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

• Proof step 49:

  # x = ii(n), ii(0) = 0, lf(0) = [], ii(m) ≠ ii(n), n ≤ m, ∀ n0. lf(n0) = x.take(ii(n0)), ∀ n0. ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ x.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = nextnli0(lf(n0), n0), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

Rule argument

Additional information

Proof step 42 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 43:

  # x = ii(n), ii(0) = 0, lf(0) = [], nextnli(x, n) = x + nextnli0(x, n), nextnli(x, n) ≠ x, ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ x.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = nextnli0(lf(n0), n0), ∀ n0. lf(n0) = x.take(ii(n0)) ⊦

Rule argument

Additional information

Used terms: x, n

Proof step 43 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 44:

  # x = ii(n), ii(0) = 0, lf(0) = [], lf(n + 1) = nextnli(lf(n), n), nextnli(x, n) = x + nextnli0(x, n), nextnli(x, n) ≠ x, ∀ n0. lf(n0) = x.take(ii(n0)), ∀ n0. ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ x.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = nextnli0(lf(n0), n0), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n) ⊦

Rule argument

Additional information

Used terms: n

Proof step 44 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 45:

  # x = ii(n), ii(0) = 0, ii(n + 1) = ii(n) + # nextnli0(lf(n), n), lf(n + 1) = nextnli(lf(n), n), lf(0) = [], nextnli(x, n) = x + nextnli0(x, n), x.drop(ii(n)).take(# nextnli0(lf(n), n)) = nextnli0(lf(n), n), nextnli(x, n) ≠ x, ¬ ii(n) < ii(n + 1), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ n0. lf(n0) = x.take(ii(n0)) ⊦

Rule argument

Additional information

Used terms: n

Proof step 45 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  # x = ii(n), ii(n + 1) = ii(n) + # nextnli0(lf(n), n), ii(0) = 0, lf(0) = [], lf(n + 1) = nextnli(lf(n), n), nextnli(x, n) = x + nextnli0(x, n), x.drop(ii(n)).take(# nextnli0(lf(n), n)) = nextnli0(lf(n), n), nextnli(x, n) ≠ x, ii(n + 1) ≤ ii(n), ∀ n0. lf(n0) = x.take(ii(n0)), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 46 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 47:

  # x = ii(n), ii(0) = 0, ii(n + 1) = ii(n) + # nextnli0(lf(n), n), lf(n + 1) = nextnli(lf(n), n), lf(0) = [], nextnli(x, n) = x + nextnli0(x, n), x.drop(ii(n)).take(# nextnli0(lf(n), n)) = nextnli0(lf(n), n), nextnli(x, n) ≠ x, ii(n + 1) ≤ ii(n), n ≤ n → nextnli0(lf(n), n) = [] ∧ ii(n) = ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n0. lf(n0) = x.take(ii(n0)) ⊦

Rule argument

Additional information

Used terms: n

Proof step 47 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  # x = ii(n), ii(0) = 0, ii(n + 1) = ii(n), lf(n + 1) = nextnli(lf(n), n), lf(0) = [], nextnli(x, n) = x + nextnli0(x, n), nextnli0(lf(n), n) = [], nextnli(x, n) ≠ x, ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n0. lf(n0) = x.take(ii(n0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (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) ⊦ # [] = 0; (s) ⊦ x.take(0) = []; (s)

Proof step 48 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ # x = n → x.take(n) = x; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: n

Proof step 49 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  # x = ii(n), ii(0) = 0, lf(0) = [], ii(m) ≠ ii(n), n ≤ m, ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n), ∀ n0. ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0) ∧ ¬ ii(n) < ii(n0 + 1) ∧ x.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = nextnli0(lf(n0), n0), ∀ n0. lf(n0) = x.take(ii(n0)) ⊦

Rule argument

Additional information

Proof step 50 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: m

Proof step 51 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  ii(0) = 0, lf(0) = [], ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ nf.drop(ii(n)).take(# nextnli0(lf(n), n)) = nextnli0(lf(n), n), ∀ n0. lf(n0) = nf.take(ii(n0)) ⊦ ∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ finp(⌜nf⌝ ); (s) ⊦ ⌜x⌝ .l = x; (s) ⊦ ⌜nf⌝ .take(n) = ⌜nf.take(n)⌝ ; (s) ⊦ ⌜x⌝ = ⌜x0⌝ ↔ x = x0; (s) ⊦ ⌜nf⌝ .drop(n) = ⌜nf.drop(n)⌝ ; (s) ⊦ ¬ ∞ < n∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss)

Proof step 52 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 53:

  ii(0) = 0, lf(0) = [], ∀ n0. lf(n0) = nf.take(ii(n0)), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ nf.drop(ii(n)).take(# nextnli0(lf(n), n)) = nextnli0(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∃ 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 53 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  ii(0) = 0, lf(0) = [], ii(m) < ii(m + 1), n1 < ii(m + 1), ii(m) ≤ n1, ∀ n0. lf(n0) = nf.take(ii(n0)), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ nf.drop(ii(n)).take(# nextnli0(lf(n), n)) = nextnli0(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦ ∃ 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 54 from proof infinite-append-prefixnextnli (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 55 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  ii(0) = 0, lf(0) = [], lf(n2) ≠ (σ.take(ii(n2))).l, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦ ii(n0) ≤ ii(n0 + 1) ∧ ¬ # σ < ⌜ii(n0 + 1)⌝ ∧ σ.take(ii(n0 + 1)) = ⌜nextnli((σ.take(ii(n0))).l, n0)⌝ ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∃ m. ii(m) ≤ n1 ∧ n1 < ii(m + 1))

Rule argument

Additional information

Proof step 56 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 57:

  ii(0) = 0, lf(0) = [], lf(n2) ≠ (σ.take(ii(n2))).l, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ ⊦

Rule argument

Additional information

Proof step 57 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 58:

  ii(0) = 0, lf(0) = [], lf(n0 +1) ≠ (σ.take(ii(n0 +1))).l, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ ii, lf, σ, n, nextnli0, nextnli. ¬ ( ii(0) = 0 ∧ lf(0) = [] ∧ lf(n0) ≠ (σ.take(ii(n0))).l ∧ (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∧ (∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0)) ∧ (∀ n. lf(n + 1) = nextnli(lf(n), n)) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ )) ⊦

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;; ⊦ σ.take(0) = []; (s) ⊦ [].l = []; (s)

Proof step 58 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  ii(0) = 0, lf(0) = [], lf(n0 + 1) ≠ (σ.take(ii(n0 + 1))).l, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ ii0, lf0, σ0, n1, nextnli1, nextnli2. ii0(0) ≠ 0 ∨ lf0(0) ≠ [] ∨ lf0(n0) = (σ0.take(ii0(n0))).l ∨ ¬ (finp(σ0) ⊃ # σ0 = ⌜ii0(n1)⌝ ∧ (∀ m. n1 ≤ m → nextnli1(lf0(m), m) = [] ∧ ii0(m) = ii0(n1));∀ n. ∃ m. ii0(m) ≤ n ∧ n < ii0(m + 1)) ∨ ¬(∀ x0, n0. nextnli2(x0, n0) = x0 + nextnli1(x0, n0)) ∨ ¬(∀ n. lf0(n + 1) = nextnli2(lf0(n), n)) ∨ ¬(∀ m, n. m ≤ n → ii0(m) ≤ ii0(n)) ∨ ¬ (∀ n. ii0(n + 1) = ii0(n) + # nextnli1(lf0(n), n) ∧ ¬ # σ0 < ⌜ii0(n + 1)⌝ ∧ σ0.drop(ii0(n)).take(# nextnli1(lf0(n), n)) = ⌜nextnli1(lf0(n), n)⌝ ) ⊦

Rule argument

Additional information

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

Proof step 59 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 60:

  ii(0) = 0, lf(0) = [], lf(n0 + 1) ≠ (σ.take(ii(n0 + 1))).l, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ , ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ii(0) ≠ 0 ∨ lf(0) ≠ [] ∨ lf(n0) = (σ.take(ii(n0))).l ∨ ¬ (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) ∨ ¬(∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0)) ∨ ¬(∀ n. lf(n + 1) = nextnli(lf(n), n)) ∨ ¬(∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∨ ¬ (∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ ) ⊦

Rule argument

Additional information

Used terms: ii, lf, σ, n, nextnli0, nextnli

Proof step 60 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  ii(0) = 0, lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, lf(n0 + 1) ≠ (σ.take(ii(n0 + 1))).l, (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. ii(n + 1) = ii(n) + # nextnli0(lf(n), n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.drop(ii(n)).take(# nextnli0(lf(n), n)) = ⌜nextnli0(lf(n), n)⌝ ⊦

Rule argument

Additional information

Proof step 61 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 62:

  ii(0) = 0, ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0), lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , lf(n0 + 1) ≠ (σ.take(ii(n0 + 1))).l, ¬ # σ < ⌜ii(n0 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 62 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0), ii(0) = 0, lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , lf(n0 + 1) ≠ (σ.take(ii(n0 + 1))).l, ¬ # σ < ⌜ii(n0 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ n. lf(n + 1) = nextnli(lf(n), n), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Proof step 63 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 64:

  ii(0) = 0, ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0), lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], lf(n0 + 1) = nextnli(lf(n0), n0), σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , lf(n0 + 1) ≠ (σ.take(ii(n0 + 1))).l, ¬ # σ < ⌜ii(n0 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0) ⊦

Rule argument

Additional information

Used terms: n0

Proof step 64 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0), ii(0) = 0, lf(n0 + 1) = nextnli(lf(n0), n0), lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , nextnli(lf(n0), n0) ≠ (σ.take(ii(n0 + 1))).l, ¬ # σ < ⌜ii(n0 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ x0, n0. nextnli(x0, n0) = x0 + nextnli0(x0, n0), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Proof step 65 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 66:

  ii(0) = 0, ii(n0 + 1) = ii(n0) + # nextnli0(lf(n0), n0), lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], lf(n0 + 1) = nextnli(lf(n0), n0), nextnli(lf(n0), n0) = lf(n0) + nextnli0(lf(n0), n0), σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , nextnli(lf(n0), n0) ≠ (σ.take(ii(n0 + 1))).l, ¬ # σ < ⌜ii(n0 + 1)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used terms: lf(n0), n0

Proof step 66 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 67:

  ii(0) = 0, lf(n0 + 1) = nextnli(lf(n0), n0), lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, nextnli(lf(n0), n0) = lf(n0) + nextnli0(lf(n0), n0), σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , nextnli(lf(n0), n0) ≠ (σ.take(ii(n0) + # nextnli0(lf(n0), n0))).l, ¬ # σ < ⌜ii(n0) + # nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Proof step 67 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  ii(0) = 0, lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], lf(n0 + 1) = nextnli(lf(n0), n0), nextnli(lf(n0), n0) = lf(n0) + nextnli0(lf(n0), n0), σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , nextnli(lf(n0), n0) ≠ (σ.take(ii(n0) + # nextnli0(lf(n0), n0))).l, ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

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 68 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 69:

  ii(0) = 0, lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , lf(n0) + nextnli0(lf(n0), n0) ≠ (σ.take(ii(n0) + # nextnli0(lf(n0), n0))).l, ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Proof step 69 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  ii(0) = 0, lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], lf(n0 + 1) = lf(n0) + nextnli0(lf(n0), n0), σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , lf(n0 + 1) ≠ (σ.take(ii(n0) + # nextnli0(lf(n0), n0))).l, ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Proof step 70 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 71:

  ii(0) = 0, lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , lf(n0) + nextnli0(lf(n0), n0) ≠ (σ.take(ii(n0) + # nextnli0(lf(n0), n0))).l, ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Proof step 71 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

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

• Proof step 73:

  ii(0) = 0, lf(n0) = (σ.take(ii(n0))).l, lf(0) = [], σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), #(lf(n0) + nextnli0(lf(n0), n0)) ≠ # (σ.take(ii(n0) + # nextnli0(lf(n0), n0))).l ∨ (∃ n. ¬(n < #(lf(n0) + nextnli0(lf(n0), n0)) → (lf(n0) + nextnli0(lf(n0), n0))[n] = (σ.take(ii(n0) + # nextnli0(lf(n0), n0))).l[n])) ⊦

Rule argument

Additional information

Used terms: (σ.take(ii(n0) + # nextnli0(lf(n0), n0))).l, lf(n0) + nextnli0(lf(n0), n0)

Proof step 72 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 73 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  ii(0) = 0, lf(0) = [], lf(n0) = (σ.take(ii(n0))).l, σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), # lf(n0) ≠ ii(n0) ∨ ¬(n1 < # lf(n0) + # nextnli0(lf(n0), n0) → (lf(n0) + nextnli0(lf(n0), n0))[n1] = (σ.take(ii(n0) + # nextnli0(lf(n0), n0))).l[n1]) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ #(x + y) = # x + # y; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s) ¬ # σ < ⌜n⌝ ⊦ # (σ.take(n)).l = n; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s)

Proof step 74 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

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

• Proof step 76:

  # lf(n0) = # (σ.take(ii(n0))).l, ii(0) = 0, lf(0) = [], σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n. n < # lf(n0) → lf(n0)[n] = (σ.take(ii(n0))).l[n], # lf(n0) ≠ ii(n0) ∨ ¬(n1 < # lf(n0) + # nextnli0(lf(n0), n0) → (lf(n0) + nextnli0(lf(n0), n0))[n1] = (σ.take(ii(n0) + # nextnli0(lf(n0), n0))).l[n1]) ⊦

Rule argument

Additional information

Used terms: (σ.take(ii(n0))).l, lf(n0)

Proof step 75 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 76 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  # lf(n0) = ii(n0), ii(0) = 0, lf(0) = [], σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜nextnli0(lf(n0), n0)⌝ , (lf(n0) + nextnli0(lf(n0), n0))[n1] ≠ σ[n1], n1 < ii(n0) + # nextnli0(lf(n0), n0), ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used simplifier rules: m < n, ¬ # σ < ⌜n⌝ ⊦ (σ.take(n)).l[m] = σ[m]; (s) 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) ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic 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 ⊦ ¬ m + n < m; (s) ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) ⊦ # x = 0 ↔ x = []; (s) lels-trans: ⊦ ¬ n∞1 < n∞ ∧ n∞1 < n∞2 → n∞ < n∞2; (forward) from specification nat-inf lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m ≤ n → (n < m ↔ false); (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) ¬ # σ < ⌜n⌝ ⊦ # (σ.take(n)).l = n; (s)

Proof step 77 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

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

• Proof step 79:

  # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = # ⌜nextnli0(lf(n0), n0)⌝ , # lf(n0) = ii(n0), ii(0) = 0, lf(0) = [], (lf(n0) + nextnli0(lf(n0), n0))[n1] ≠ σ[n1], n1 < ii(n0) + # nextnli0(lf(n0), n0), ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ n. ⌜n⌝ < # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) → σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n] = ⌜nextnli0(lf(n0), n0)⌝ [n] ⊦

Rule argument

Additional information

Used terms: ⌜nextnli0(lf(n0), n0)⌝ , σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))

Proof step 78 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 79 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , # lf(n0) = ii(n0), ii(0) = 0, lf(0) = [], (lf(n0) + nextnli0(lf(n0), n0))[n1] ≠ σ[n1], n1 < ii(n0) + # nextnli0(lf(n0), n0), ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ n2. n2 < # nextnli0(lf(n0), n0) → σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n2] = nextnli0(lf(n0), n0)[n2] ⊦

Rule argument

Additional information

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

Proof step 80 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 81:

  ⊦ n < # x → (x + y)[n] = x[n]

• Proof step 82:

  # lf(n0) = ii(n0), # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , ii(0) = 0, lf(0) = [], (lf(n0) + nextnli0(lf(n0), n0))[n1] ≠ σ[n1], n1 < ii(n0) + # nextnli0(lf(n0), n0), ¬ n1 < # lf(n0), ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n2. n2 < # nextnli0(lf(n0), n0) → σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n2] = nextnli0(lf(n0), n0)[n2], ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

• Proof step 95:

  # lf(n0) = ii(n0), # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , ii(0) = 0, lf(0) = [], lf(n0)[n1] ≠ σ[n1], n1 < ii(n0) + # nextnli0(lf(n0), n0), n1 < # lf(n0), ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n2. n2 < # nextnli0(lf(n0), n0) → σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n2] = nextnli0(lf(n0), n0)[n2], ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used terms: n1, nextnli0(lf(n0), n0), lf(n0)

Proof step 81 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 82 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

  # lf(n0) = ii(n0), # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , ii(0) = 0, lf(0) = [], nextnli0(lf(n0), n0)[n1 - ii(n0)] ≠ σ[n1], nextnli0(lf(n0), n0) ≠ [], n1 < ii(n0) + # nextnli0(lf(n0), n0), ii(n0) ≤ n1, ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n2. n2 < # nextnli0(lf(n0), n0) → σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n2] = nextnli0(lf(n0), n0)[n2], ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

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 ⊦ # x = 0 ↔ x = []; (s) ⊦ m < m + n ↔ n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s)

Proof step 83 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 84:

  # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , # lf(n0) = ii(n0), ii(0) = 0, lf(0) = [], n1 = n3 + ii(n0), nextnli0(lf(n0), n0)[n3] ≠ σ[n1], nextnli0(lf(n0), n0) ≠ [], n1 < ii(n0) + # nextnli0(lf(n0), n0), ii(n0) ≤ n1, ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ n2. n2 < # nextnli0(lf(n0), n0) → σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n2] = nextnli0(lf(n0), n0)[n2] ⊦

Rule argument

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: n1, ii(n0), n3

Proof step 84 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 85:

  # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , # lf(n0) = ii(n0), ii(0) = 0, lf(0) = [], nextnli0(lf(n0), n0)[n3] ≠ σ[n3 + ii(n0)], nextnli0(lf(n0), n0) ≠ [], n3 < # nextnli0(lf(n0), n0), ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ n2. n2 < # nextnli0(lf(n0), n0) → σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n2] = nextnli0(lf(n0), n0)[n2] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m ≤ m + n; (s)

Proof step 85 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 86:

  # lf(n0) = ii(n0), # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , ii(0) = 0, lf(0) = [], nextnli0(lf(n0), n0)[n3] ≠ σ[n3 + ii(n0)], nextnli0(lf(n0), n0) ≠ [], n3 < # nextnli0(lf(n0), n0), ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , n3 < # nextnli0(lf(n0), n0) → σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n3] = nextnli0(lf(n0), n0)[n3], (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used terms: n3

Proof step 86 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 87:

  # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , # lf(n0) = ii(n0), σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n3] = nextnli0(lf(n0), n0)[n3], ii(0) = 0, lf(0) = [], nextnli0(lf(n0), n0)[n3] ≠ σ[n3 + ii(n0)], nextnli0(lf(n0), n0) ≠ [], n3 < # nextnli0(lf(n0), n0), ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2] ⊦

Rule argument

Additional information

Proof step 87 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 88:

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

• Proof step 89:

  # lf(n0) = ii(n0), # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n3] = nextnli0(lf(n0), n0)[n3], ii(0) = 0, lf(0) = [], nextnli0(lf(n0), n0)[n3] ≠ σ[n3 + ii(n0)], nextnli0(lf(n0), n0) ≠ [], n3 < # nextnli0(lf(n0), n0), ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦ n3 < # nextnli0(lf(n0), n0) ∧ ¬ # σ.drop(ii(n0)) < ⌜# nextnli0(lf(n0), n0)⌝

• Proof step 92:

  # lf(n0) = ii(n0), # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , σ.drop(ii(n0))[n3] = nextnli0(lf(n0), n0)[n3], ii(0) = 0, lf(0) = [], nextnli0(lf(n0), n0)[n3] ≠ σ[n3 + ii(n0)], nextnli0(lf(n0), n0) ≠ [], n3 < # nextnli0(lf(n0), n0), ¬ # σ.drop(ii(n0)) < ⌜# nextnli0(lf(n0), n0)⌝ , ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

Used terms: n3, # nextnli0(lf(n0), n0), σ.drop(ii(n0))

Proof step 88 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 89 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 90:

  # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , # lf(n0) = ii(n0), σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n3] = nextnli0(lf(n0), n0)[n3], ii(0) = 0, lf(0) = [], nextnli0(lf(n0), n0)[n3] ≠ σ[n3 + ii(n0)], nextnli0(lf(n0), n0) ≠ [], n3 < # nextnli0(lf(n0), n0), # σ.drop(ii(n0)) < ⌜# nextnli0(lf(n0), n0)⌝ , ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2] ⊦

Rule argument

Additional information

Proof step 90 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 91:

  ⊦ ⌜n⌝ < # σ ∧ finp(σ) → # σ.drop(n) = ⌜(# σ).n - n⌝

Rule argument

Additional information

Used simplifier rules: ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as) ¬ # x < n ⊦ # x.take(n) = n; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) ⊦ ⌜x⌝ .take(n) = ⌜x.take(n)⌝ ; (s) ¬ # x < n ⊦ # x.drop(n) = # x - n; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ¬ # x < n, m < n ⊦ x.take(n)[m] = x[m]; (s) ⊦ ⌜n⌝ .n = n; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) 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 let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (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 fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ # x = 0 ↔ x = []; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m < n → (n ≤ m ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic m + m0 < # x ⊦ x.drop(m)[m0] = x[m + m0]; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) lele-trans: ⊦ ¬ n∞1 < n∞ ∧ ¬ n∞2 < n∞1 → ¬ n∞2 < n∞; (forward) from specification nat-inf ⊦ m + m0 ≤ m ↔ m0 = 0; (s) ⊦ ⌜m⌝ < ∞; (s) ⊦ ¬ finp(σ) → # σ = ∞; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) ¬ # σ < ⌜n⌝ ⊦ # σ.take(n) = ⌜n⌝ ; (s) ⊦ # ⌜nf⌝ = ∞; (s) ⊦ ¬ ∞ < n∞; (s) m < n, ¬ # σ < ⌜n⌝ ⊦ σ.take(n)[m] = σ[m]; (s) ⊦ ⌜nf⌝ .drop(n) = ⌜nf.drop(n)⌝ ; (s) ⊦ nf.drop(n)(m) = nf(m + n); (s) ⊦ ⌜nf⌝ [n] = nf(n); (s) Used terms: ii(n0), σ

Proof step 91 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 92 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 93:

  # lf(n0) = ii(n0), σ.drop(ii(n0))[n3] = nextnli0(lf(n0), n0)[n3], ii(0) = 0, lf(0) = [], nextnli0(lf(n0), n0)[n3] ≠ σ[n3 + ii(n0)], nextnli0(lf(n0), n0) ≠ [], n3 < # nextnli0(lf(n0), n0), ¬ # σ.drop(ii(n0)) < ⌜# nextnli0(lf(n0), n0)⌝ , ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ m, n. m ≤ n → ii(m) ≤ ii(n), ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2] ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (s) ¬ # σ < ⌜n⌝ ⊦ # σ.take(n) = ⌜n⌝ ; (s)

Proof step 93 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 94:

  ⊦ ¬ # σ < ⌜n⌝ ∧ finp(σ) → # σ.drop(n) = ⌜(# σ).n - n⌝

Rule argument

Additional information

Used simplifier rules: ⊦ finp(σ) ↔ (∃ x. ⌜x⌝ = σ); (as) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ; (s) ⊦ ⌜n⌝ .n = n; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; (s) c: ⊦ m + n = n + m; from specification nat-basic ⊦ m ≤ n → (n < m ↔ false); (s) m + m0 < # x ⊦ x.drop(m)[m0] = x[m + m0]; (s) ⊦ ⌜x⌝ [n] = x[n]; (s) lels-trans: ⊦ ¬ n∞1 < n∞ ∧ n∞1 < n∞2 → n∞ < n∞2; (forward) from specification nat-inf ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0; (s) ⊦ ¬ m + n < m; (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 ⊦ ¬ # σ < ⌜n⌝ → (# σ.drop(n) < ⌜n0⌝ ↔ # σ < ⌜n + n0⌝ ); (s) ⊦ ¬ finp(σ) → # σ = ∞; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ ∞ < n∞; (s) ⊦ finp(σ) ↔ ¬(∃ nf. ⌜nf⌝ = σ); (ss) ⊦ ⌜nf⌝ .drop(n) = ⌜nf.drop(n)⌝ ; (s) ⊦ nf.drop(n)(m) = nf(m + n); (s) ⊦ ⌜nf⌝ [n] = nf(n); (s) Used terms: ii(n0), σ

Proof step 94 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 95 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 96:

  # lf(n0) = ii(n0), # σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0)) = ⌜# nextnli0(lf(n0), n0)⌝ , ii(0) = 0, lf(0) = [], lf(n0)[n1] ≠ σ[n1], n1 < ii(n0) + # nextnli0(lf(n0), n0), n1 < ii(n0), ¬ # σ < ⌜ii(n0)⌝ + ⌜# nextnli0(lf(n0), n0)⌝ , (finp(σ) ⊃ # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → nextnli0(lf(m), m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∀ n2. n2 < # nextnli0(lf(n0), n0) → σ.drop(ii(n0)).take(# nextnli0(lf(n0), n0))[n2] = nextnli0(lf(n0), n0)[n2], ∀ n2. n2 < ii(n0) → lf(n0)[n2] = σ[n2], ∀ m, n. m ≤ n → ii(m) ≤ ii(n) ⊦

Rule argument

Additional information

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

Proof step 96 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n1

Proof step 97 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 98:

  ∀ x, n. x ⊑ nextnli(x, n) ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∃ y. nextnli(x, n) = x + y

Rule argument

Additional information

Proof step 98 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 99:

  x ⊑ nextnli(x, n) ⊦ ∃ y. nextnli(x, n) = x + y, ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Used terms: x, n

Proof step 99 from proof infinite-append-prefixnextnli (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 100:

  ⊦ x ⊑ y ↔ (∃ z. x + z = y)

• Proof step 101:

  ∃ z. x + z = nextnli(x, n) ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)), ∃ y. nextnli(x, n) = x + y

Rule argument

Additional information

Used terms: nextnli(x, n), x

Proof step 100 from proof infinite-append-prefixnextnli (previous step) (back to tree)

A spec-lemma

Proof step 101 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 102:

  x + x0 = nextnli(x, n) ⊦ ∃ y. nextnli(x, n) = x + y, ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n) ≤ ii(n + 1) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ σ.take(ii(n + 1)) = ⌜nextnli((σ.take(ii(n))).l, n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ ⌜nextnli(σ.l, n)⌝ = σ ∧ (∀ m. n ≤ m → ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1))

Rule argument

Additional information

Proof step 102 from proof infinite-append-prefixnextnli (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: x0