Proof step 35 from proof compatarray-mode (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ compatarray(str, r, st) ↔ is_arraytype(st[r -- _type] .type) ∧ r -- _length ∈ st ∧ is_integervalue(st[r -- _length]) ∧ 0 ≤ st[r -- _length] .intval ∧ is_arrayref(r, st[r -- _length] .intval, st) ∧ (∀ j. 0 ≤ j ∧ j < st[r -- _length] .intval → compat(str, st[r -- j '], st[r -- _type] .type .type, st))

• Proof step 34:

  ⊦ r = jvmref, is_arraytype((st[_mode, val][r -- _type]) .type) ∧ r -- _length ∈ st[_mode, val] ∧ is_integervalue(st[_mode, val][r -- _length]) ∧ 0 ≤ (st[_mode, val][r -- _length]) .intval ∧ is_arrayref(r, (st[_mode, val][r -- _length]) .intval, st[_mode, val]) ∧ (∀ j. 0 ≤ j ∧ j < (st[_mode, val][r -- _length]) .intval → compat(str, st[_mode, val][r -- j '], (st[_mode, val][r -- _type]) .type .type, st[_mode, val])) ↔ compatarray(str, r, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[_mode, val], r, str)]]