Proof step 34 from proof ac-shift-02 (conclusion)

User applied rule structural induction

And obtained the following new goals

• Proof step 1:

  ⊦ addclass(class1, [], st) = st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', initval(done)]

• Proof step 2:

  ⊦ addclass(class1, (mkfs(class1, ty, fieldvar) ' × val) ', st) = (st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', initval(done)][jvmref -- mkfs(class1, ty, fieldvar) ', val])

• Proof step 33:

  ∀ class1, st, ty, fieldvar, val. (addclass(class1, fis0, st)[jvmref -- mkfs(class1, ty, fieldvar) ', val]) = addclass(class1, fis0[mkfs(class1, ty, fieldvar) ', val], st) ⊦ (addclass(class1, fv + fis0, st)[jvmref -- mkfs(class1, ty, fieldvar) ', val]) = addclass(class1, (fv + fis0)[mkfs(class1, ty, fieldvar) ', val], st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ([CSIMPGEN : fieldinits generated by [], +;], [CSIMPSEQ : ⊦ [][sk, val] = (sk × val) '])]]