Proof step 16 from proof nextnli-lemma (previous step)

User applied rule structural induction

And obtained the following new goals

• Proof step 17:

  0 ≤ n1, n1 ≤ n0, 0 ≤ n0, ∀ n. lfgen(n)(0) = x ∧ (∀ m. m < n → lfgen(n)(m + 1) = nextnli(lfgen(n)(m), m)) ⊦ lfgen(n1)(0) = lfgen(n0)(0)

• Proof step 21:

  m0 +1 ≤ n1, n1 ≤ n0, m0 +1 ≤ n0, ∀ n. lfgen(n)(0) = x ∧ (∀ m. m < n → lfgen(n)(m + 1) = nextnli(lfgen(n)(m), m)), ∀ n0, n1, lfgen, x, nextnli. m0 ≤ n0 ∧ n1 ≤ n0 ∧ m0 ≤ n1 ∧ (∀ n. lfgen(n)(0) = x ∧ (∀ m. m < n → lfgen(n)(m + 1) = nextnli(lfgen(n)(m), m))) → lfgen(n1)(m0) = lfgen(n0)(m0) ⊦ lfgen(n1)(m0 +1) = lfgen(n0)(m0 +1)

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;