Proof step 26 from proof ac-new (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 17:

  ¬ (is_fskey(fv .1) ∧ fv .1 .fs .class ≠ class1), ∀ r, class1, st. newref(r, addclass(class1, fis0, st)) ↔ newref(r, st) ⊦ newref(r, addclass(class1, fv ' + fis0, st)) ↔ newref(r, st)

• Proof step 25:

  is_fskey(fv .1) ∧ fv .1 .fs .class ≠ class1, ∀ r, class1, st. newref(r, addclass(class1, fis0, st)) ↔ newref(r, st) ⊦ newref(r, addclass(class1, fis0, st)) ↔ newref(r, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, fis0, fv, class1)]]