Proof step 15 from proof nextli-lemma (previous step)

User applied rule structural induction

And obtained the following new goals

• Proof step 16:

  lfgen(0)(0) = [], 0 ≤ n1, n1 ≤ n0, 0 ≤ n0, ∀ n. lfgen(n)(0) = [] ∧ (∀ m. m < n → lfgen(n)(m + 1) = nextli(lfgen(n)(m))) ⊦ lfgen(n1)(0) = lfgen(n0)(0)

• Proof step 20:

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

Rule argument

Additional information

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