Proof step 1 from proof nextl-nextj-lemma-butlast (conclusion)

User applied rule cut formula

And obtained the following new goals

• Proof step 2:

  ∀ m. ∃ lf, jj. lf(0) = a ' ∧ jj(0) = n0 ∧ (∀ n. n ≤ m → lf(n + 1) = nextl(jj(n), lf(n).last) ∧ jj(n + 1) = nextj(jj(n), lf(n).last)) ⊦ ∃ lf, jj. lf(0) = a ' ∧ jj(0) = n0 ∧ (∀ n. lf(n + 1) = nextl(jj(n), lf(n).last) ∧ jj(n + 1) = nextj(jj(n), lf(n).last))

• Proof step 42:

  ⊦ ∀ m. ∃ lf, jj. lf(0) = a ' ∧ jj(0) = n0 ∧ (∀ n. n ≤ m → lf(n + 1) = nextl(jj(n), lf(n).last) ∧ jj(n + 1) = nextj(jj(n), lf(n).last)), ∃ lf, jj. lf(0) = a ' ∧ jj(0) = n0 ∧ (∀ n. lf(n + 1) = nextl(jj(n), lf(n).last) ∧ jj(n + 1) = nextj(jj(n), lf(n).last))

Rule argument

Additional information

Used formulas: ∀ m. ∃ lf, jj. lf(0) = a ' ∧ jj(0) = n0 ∧ (∀ n. n ≤ m → lf(n + 1) = nextl(jj(n), lf(n).last) ∧ jj(n + 1) = nextj(jj(n), lf(n).last))