Proof step 21 from proof initsubset-put-statfield-int (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ validstatfield(str, rk .key, st0[rk, val]) ∧ init⊆(str, st, st0) ∧ rk .ref = jvmref ∧ (¬ is_fskey(rk .key) ∨ rk .key .fs .type ≠ void_type ∨ rk .key .fs .field ≠ `initstate' .field ∧ rk ≠ _uninit) → init⊆(str, st, st0[rk, val])

• Proof step 20:

  ¬ ( validstatfield(str, (jvmref -- mkfs(class, int_type, fieldvar) ') .key, st0[jvmref -- mkfs(class, int_type, fieldvar) ', intval(i)]) ∧ init⊆(str, st, st0) ∧ (jvmref -- mkfs(class, int_type, fieldvar) ') .ref = jvmref ∧ ( ¬ is_fskey((jvmref -- mkfs(class, int_type, fieldvar) ') .key) ∨ (jvmref -- mkfs(class, int_type, fieldvar) ') .key .fs .type ≠ void_type ∨ (jvmref -- mkfs(class, int_type, fieldvar) ') .key .fs .field ≠ `initstate' .field ∧ jvmref -- mkfs(class, int_type, fieldvar) ' ≠ _uninit)), init⊆(str, st, st0) ⊦ init⊆(str, st, st0[jvmref -- mkfs(class, int_type, fieldvar) ', intval(i)])

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (intval(i), jvmref -- mkfs(class, int_type, fieldvar) ', st0, st, str)]]