[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 147 from proof compat-addobj (previous step)

st[r0 -- _type] = typeval(mkarraytype(ty0)), st[r0 -- _length] = intval(i), st[r0 -- j '] = refval(r1), okval(refval(r1), ty0), r0 -- _length ∈ st, is_arrayref(r0, i, st), r0 ∈ st, r0 -- _type ∈ st, compatstatic(str, st), compatmode(str, st), newref(r, st), is_predefined_class(class), 0 ≤ i, j < i, 0 ≤ j, 0 < i, r1 ≠ jvmref → r1 -- _type ∈ st ∧ is_typevalue(st[r1 -- _type]) ∧ is_reftype(st[r1 -- _type] .type) ∧ (has_classtype(st[r1 -- _type] .type) → tdname+∃(str, st[r1 -- _type] .type .jtelemtype .class)) ∧ (is_classtype(st[r1 -- _type] .type) → class+∃(str, st[r1 -- _type] .type .class)) ∧ is_subtype(str, st[r1 -- _type] .type, ty0), ¬ has_classtype(ty0) ∨ tdname+∃(str, ty0 .jtelemtype .class), ∀ j0. ¬ j0 < 0 ∧ ¬ i ≤ j0 → compat(str, st[r0 -- j0 '], ty0, st) ⊦ r0 = jvmref, r = jvmref, (ty0 = void_type ∨ is_reftype(ty0)) ∧ ( r1 ≠ jvmref → (r1 = r ∨ r1 -- _type ∈ st) ∧ is_typevalue(st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) ∧ is_reftype((st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type) ∧ ( has_classtype((st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type) → class∃(str, (st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type .jtelemtype .class) ∨ interface∃(str, (st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type .jtelemtype .class) ∨ is_predefined_class((st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type .jtelemtype .class)) ∧ ( is_classtype((st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type) → class+∃(str, (st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type .class)) ∧ is_subtype(str, (st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type, ty0))

Heuristic weak cut applied rule cut formula

And obtained the following new goals

Proof step 146:
st[r0 -- _type] = typeval(mkarraytype(ty0)), st[r0 -- _length] = intval(i), st[r0 -- j '] = refval(r1), okval(refval(r1), ty0), r0 -- _length ∈ st, is_arrayref(r0, i, st), r0 ∈ st, r0 -- _type ∈ st, compatstatic(str, st), compatmode(str, st), newref(r, st), is_predefined_class(class), 0 ≤ i, j < i, 0 ≤ j, 0 < i, r1 ≠ jvmref → r1 -- _type ∈ st ∧ is_typevalue(st[r1 -- _type]) ∧ is_reftype(st[r1 -- _type] .type) ∧ (has_classtype(st[r1 -- _type] .type) → tdname+∃(str, st[r1 -- _type] .type .jtelemtype .class)) ∧ (is_classtype(st[r1 -- _type] .type) → class+∃(str, st[r1 -- _type] .type .class)) ∧ is_subtype(str, st[r1 -- _type] .type, ty0), ¬ has_classtype(ty0) ∨ tdname+∃(str, ty0 .jtelemtype .class), ∀ j0. ¬ j0 < 0 ∧ ¬ i ≤ j0 → compat(str, st[r0 -- j0 '], ty0, st) ⊦ r1 -- _type = r -- _type, r0 = jvmref, r = jvmref, (ty0 = void_type ∨ is_reftype(ty0)) ∧ ( r1 ≠ jvmref → (r1 = r ∨ r1 -- _type ∈ st) ∧ is_typevalue(st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) ∧ is_reftype((st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type) ∧ ( has_classtype((st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type) → class∃(str, (st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type .jtelemtype .class) ∨ interface∃(str, (st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type .jtelemtype .class) ∨ is_predefined_class((st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type .jtelemtype .class)) ∧ ( is_classtype((st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type) → class+∃(str, (st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type .class)) ∧ is_subtype(str, (st[r -- _type, typeval(mkclasstype(class))][r1 -- _type]) .type, ty0))

Rule argument

[fma-arg: r1 -- _type = r -- _type]

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ r -- sk = r0 -- sk0 ↔ r = r0 ∧ sk = sk0], [CSIMPFORWARD : ⊦ r -- sk ∈ st → r ∈ st], [CSIMPSEQ : ⊦ newref(r, st) ∧ r0 ∈ st → r ≠ r0], [CSIMPSEQ : ⊦ ¬ has_classtype(ty) → ¬ is_classtype(ty)], [CSIMPSEQ : ⊦ (st[rk, val][rk]) = val], [CSIMPSEQ : ⊦ is_typevalue(typeval(ty))], [CSIMPSEQ : ⊦ typeval(ty) .type = ty], [CSIMPSEQ : ⊦ is_reftype(mkclasstype(class))], [CSIMPSEQ : ⊦ r ∈ st → ¬ newref(r, st)])], [EXTRAFMAS : (r1 -- _type = r -- _type)]]