Proof step 39 from proof ac-dups-03 (conclusion)

User applied rule structural induction

And obtained the following new goals

• Proof step 11:

  ⊦ addclass(class1, [] + (sk × val) ' + fis1 + (sk × val0) ' + fis0, st) = addclass(class1, [] + (sk × val) ' + fis1 + fis0, st)

• Proof step 38:

  ∀ class1, sk, val, fis1, val0, fis2, st. addclass(class1, fis0 + (sk × val) ' + fis1 + (sk × val0) ' + fis2, st) = addclass(class1, fis0 + (sk × val) ' + fis1 + fis2, st) ⊦ addclass(class1, (fv + fis0) + (sk × val) ' + fis1 + (sk × val0) ' + fis2, st) = addclass(class1, (fv + fis0) + (sk × val) ' + fis1 + fis2, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ([CSIMPGEN : fieldinits generated by [], +;])]]