Proof step 68 from proof infinite-append-butlast (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

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

Rule argument

Additional information