Proof step 21 from proof ac-refs (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 14:

  ¬ (is_fskey((sk × val) .1) ∧ (sk × val) .1 .fs .class ≠ class), ∀ class, st. addclass(class, fis0, st) .refs = st .refs ++ jvmref ⊦ addclass(class, (sk × val) ' + fis0, st) .refs = st .refs ++ jvmref

• Proof step 20:

  is_fskey((sk × val) .1) ∧ (sk × val) .1 .fs .class ≠ class, ∀ class, st. addclass(class, fis0, st) .refs = st .refs ++ jvmref ⊦ addclass(class, fis0, st) .refs = st .refs ++ jvmref

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, fis0, sk × val, class)]]