[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 104 from proof validrefs-all-same (previous step)

st0[r -- _length] = intval(i0), st[r -- _type] = typeval(mkarraytype(ty1)), st[r -- _length] = intval(i0), st0[r -- _type] = typeval(mkarraytype(ty1)), is_arrayref(r, i0, st), r -- _length ∈ st, is_referencevalue(refval(r)) ∧ ( refval(r) .refval ≠ jvmref → refval(r) .refval -- _type ∈ st ∧ is_typevalue(st[refval(r) .refval -- _type]) ∧ st[refval(r) .refval -- _type] .type ≤ mkarraytype(ty1)), type∃(str, ty1), r -- _type ∈ st0, r ∈ st0, r ∈ st, mkarraytype(ty1) ≤ ty, r -- _type ∈ st, r -- _length ∈ st0, 0 ≤ i0, ∀ j0. ¬ j0 < 0 ∧ ¬ i0 ≤ j0 → okval(st[r -- j0 '], ty1), ∀ r0. (r0 = r ∨ r0 ∈ refs0) ∧ r0 ≠ jvmref → st[r0 -- _type] = st0[r0 -- _type] ∧ (is_classtype(st[r0 -- _type] .type) → (∀ sk. sk ∈ instfields(st[r0 -- _type] .type .class) → st[r0 -- sk] = st0[r0 -- sk])) ∧ ( is_arraytype(st[r0 -- _type] .type) → st[r0 -- _length] = st0[r0 -- _length] ∧ (∀ i. ¬ i < 0 ∧ ¬ st[r0 -- _length] .intval ≤ i → st[r0 -- i '] = st0[r0 -- i '])), ∀ str0, ty0, st1, st2. validrefs(str0, refs0, ty0, st1) ∧ (∀ r0. r0 ∈ refs0 ∧ r0 ≠ jvmref → st1[r0 -- _type] = st2[r0 -- _type] ∧ (is_classtype(st1[r0 -- _type] .type) → (∀ sk. sk ∈ instfields(st1[r0 -- _type] .type .class) → st1[r0 -- sk] = st2[r0 -- sk])) ∧ ( is_arraytype(st1[r0 -- _type] .type) → st1[r0 -- _length] = st2[r0 -- _length] ∧ (∀ i. 0 ≤ i ∧ i < st1[r0 -- _length] .intval → st1[r0 -- i '] = st2[r0 -- i ']))) → validrefs(str0, refs0, ty0, st2), refs0 = [] ∨ 0 ≤ i ∧ i < i0 ∧ is_referencevalue(st[r -- i ']) ∧ refs0 .first = st[r -- i '] .refval ∧ validrefs(str, refs0, ty1, st), ∀ i. ¬ i < 0 ∧ ¬ i0 ≤ i → st[r -- i '] = st0[r -- i '] ⊦ r = jvmref, ty1 .jtelemtype = void_type, ty1 .jtelemtype = abstract_type, validrefs(str, r ' + refs0, ty, st0), (0 ≤ j ∧ j < i0 → okval(st0[r -- j '], ty1)) ∧ is_arrayref(r, i0, st0)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 103:
st0[r -- _type] = typeval(mkarraytype(ty1)), st[r -- _length] = intval(i0), st[r -- _type] = typeval(mkarraytype(ty1)), st0[r -- _length] = intval(i0), 0 ≤ i0, r -- _length ∈ st0, r -- _type ∈ st, mkarraytype(ty1) ≤ ty, r ∈ st, r ∈ st0, r -- _type ∈ st0, type∃(str, ty1), r -- _length ∈ st, is_arrayref(r, i0, st), ∀ i. ¬ i < 0 ∧ ¬ i0 ≤ i → st[r -- i '] = st0[r -- i '], refs0 = [] ∨ 0 ≤ i ∧ i < i0 ∧ is_referencevalue(st[r -- i ']) ∧ refs0 .first = st[r -- i '] .refval ∧ validrefs(str, refs0, ty1, st), ∀ str0, ty0, st1, st2. validrefs(str0, refs0, ty0, st1) ∧ (∀ r0. r0 ∈ refs0 ∧ r0 ≠ jvmref → st1[r0 -- _type] = st2[r0 -- _type] ∧ (is_classtype(st1[r0 -- _type] .type) → (∀ sk. sk ∈ instfields(st1[r0 -- _type] .type .class) → st1[r0 -- sk] = st2[r0 -- sk])) ∧ ( is_arraytype(st1[r0 -- _type] .type) → st1[r0 -- _length] = st2[r0 -- _length] ∧ (∀ i. 0 ≤ i ∧ i < st1[r0 -- _length] .intval → st1[r0 -- i '] = st2[r0 -- i ']))) → validrefs(str0, refs0, ty0, st2), ∀ r0. (r0 = r ∨ r0 ∈ refs0) ∧ r0 ≠ jvmref → st[r0 -- _type] = st0[r0 -- _type] ∧ (is_classtype(st[r0 -- _type] .type) → (∀ sk. sk ∈ instfields(st[r0 -- _type] .type .class) → st[r0 -- sk] = st0[r0 -- sk])) ∧ ( is_arraytype(st[r0 -- _type] .type) → st[r0 -- _length] = st0[r0 -- _length] ∧ (∀ i. ¬ i < 0 ∧ ¬ st[r0 -- _length] .intval ≤ i → st[r0 -- i '] = st0[r0 -- i '])), ∀ j0. ¬ j0 < 0 ∧ ¬ i0 ≤ j0 → okval(st[r -- j0 '], ty1) ⊦ ty1 .jtelemtype = abstract_type, ty1 .jtelemtype = void_type, r = jvmref, validrefs(str, r ' + refs0, ty, st0), (0 ≤ j ∧ j < i0 → okval(st0[r -- j '], ty1)) ∧ is_arrayref(r, i0, st0)

Rule argument

[emptyarg]

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ is_typevalue(typeval(ty))], [CSIMPSEQ : ⊦ is_arraytype(mkarraytype(ty))], [CSIMPSEQ : ⊦ ty ≤ ty], [CSIMPSEQ : ⊦ mkarraytype(ty) .type = ty], [CSIMPSEQ : ⊦ typeval(ty) .type = ty], [CSIMPSEQ : ⊦ ty0 ≤ mkarraytype(ty) ↔ is_arraytype(ty0) ∧ ty0 .type ≤ ty], [CSIMPSEQ : ⊦ refval(r) .refval = r], [CSIMPSEQ : ⊦ is_referencevalue(refval(r))])]]