Proof step 8 from proof fits-append (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ fits(r, sk ', st) ↔ r ≠ jvmref ∧ is_referencevalue(st[r -- sk]) ∧ (is_classtype(st[r -- _type] .type) → sk ∈ instfields(st[r -- _type] .type .class)) ∧ (is_arraytype(st[r -- _type] .type) → is_indexkey(sk) ∧ 0 ≤ sk .index ∧ sk .index < st[r -- _length] .intval)

• Proof step 7:

  ⊦ fits(r, sk ' + sks0, st) ↔ r ≠ jvmref ∧ is_referencevalue(st[r -- sk]) ∧ (is_classtype(st[r -- _type] .type) → sk ∈ instfields(st[r -- _type] .type .class)) ∧ (is_arraytype(st[r -- _type] .type) → is_indexkey(sk) ∧ 0 ≤ sk .index ∧ sk .index < st[r -- _length] .intval) ∧ fits(st[r -- sk] .refval, sks0, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, sk, r)]]