Proof step 14 from proof ac-dups-04 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ is_fskey(fv .1) ∧ fv .1 .fs .class ≠ class → addclass(class, fv ' + fis, st) = addclass(class, fis, st)

• Proof step 8:

  ¬ (is_fskey((sk × val) .1) ∧ (sk × val) .1 .fs .class ≠ class1), is_fskey(sk) ⊦ addclass(class1, (sk × val) ' + (sk × val0) ', st) = addclass(class1, (sk × val) ', st)

• Proof step 13:

  is_fskey((sk × val) .1) ∧ (sk × val) .1 .fs .class ≠ class1, is_fskey(sk) ⊦ addclass(class1, (sk × val0) ', st) = addclass(class1, (sk × val) ', st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, (sk × val0) ', sk × val, class1)]]