[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 148 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, okval(refval(r1), ty0) ∧ ( is_referencevalue(refval(r1)) ∧ refval(r1) .refval ≠ jvmref → refval(r1) .refval -- _type ∈ st[r -- _type, typeval(mkclasstype(class))] ∧ is_typevalue(st[r -- _type, typeval(mkclasstype(class))][refval(r1) .refval -- _type]) ∧ is_reftype((st[r -- _type, typeval(mkclasstype(class))][refval(r1) .refval -- _type]) .type) ∧ ( has_classtype((st[r -- _type, typeval(mkclasstype(class))][refval(r1) .refval -- _type]) .type) → tdname+∃(str, (st[r -- _type, typeval(mkclasstype(class))][refval(r1) .refval -- _type]) .type .jtelemtype .class)) ∧ ( is_classtype((st[r -- _type, typeval(mkclasstype(class))][refval(r1) .refval -- _type]) .type) → class+∃(str, (st[r -- _type, typeval(mkclasstype(class))][refval(r1) .refval -- _type]) .type .class)) ∧ asgcomp(str, refval(r1), ty0, st[r -- _type, typeval(mkclasstype(class))]))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 147:
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))

Rule argument

[emptyarg]

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ asgcomp(str, val, ty, st) ↔ ¬ is_referencevalue(val) ∨ val .refval = jvmref ∨ is_subtype (str, st[val .refval -- _type] .type, ty)], [CSIMPSEQ : ⊦ tdname∃(str, class) ↔ class∃(str, class) ∨ interface∃(str, class)], [CSIMPSEQ : ⊦ tdname+∃(str, class) ↔ tdname∃(str, class) ∨ is_predefined_class(class)], [CSIMPSEQ : ⊦ r -- sk = r0 -- sk0 ↔ ¬ ¬ (r = r0 ∧ sk = sk0)], [CSIMPSEQ : ⊦ rk ∈ st[rk0, val] ↔ rk = rk0 ∨ rk ∈ st], [CSIMPSEQ : ⊦ refval(r) .refval = r], [CSIMPSEQ : ⊦ is_referencevalue(refval(r))], [CSIMPSEQ : ⊦ okval(refval(r), ty) ↔ ty = void_type ∨ is_reftype(ty)])]]