Proof step 18 from proof instore-afterputs (previous step)

User applied rule structural induction

And obtained the following new goals

• Proof step 7:

  r ∈ st, r -- sk ∈ st, unique_al([]), instore(r, class, [], st) ⊦ _type = sk, sk ∈ [], _type ∈ [], instore(r, class, [], st[r -- sk, refval(r1)])

• Proof step 17:

  ∀ r, st, sk, class, r1. r ∈ st ∧ r -- sk ∈ st ∧ unique_al(fis0) ∧ instore(r, class, fis0, st) → _type = sk ∨ sk ∈ fis0 ∨ _type ∈ fis0 ∨ instore(r, class, fis0, st[r -- sk, refval(r1)]), r ∈ st, r -- sk ∈ st, unique_al(fv + fis0), instore(r, class, fv + fis0, st) ⊦ _type = sk, sk ∈ fv + fis0, _type ∈ fv + fis0, instore(r, class, fv + fis0, st[r -- sk, refval(r1)])

Rule argument

Additional information

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