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

st[jvmref -- mkfs(class1, ty, fieldvar) '] = refval(r0), jvmref -- mkfs(class1, ty, fieldvar) ' ∈ st, initdone(class0, st), is_predefined_class(class), newref(r, st), compatmode(str, st), compatrefs(str, st), mkfs(class1, ty, fieldvar) ' ∈ statfields(class0), jvmref ∈ st, okval(refval(r0), ty), r0 ≠ jvmref → r0 -- _type ∈ st ∧ is_typevalue(st[r0 -- _type]) ∧ is_reftype(st[r0 -- _type] .type) ∧ (has_classtype(st[r0 -- _type] .type) → tdname+∃(str, st[r0 -- _type] .type .jtelemtype .class)) ∧ (is_classtype(st[r0 -- _type] .type) → class+∃(str, st[r0 -- _type] .type .class)) ∧ is_subtype(str, st[r0 -- _type] .type, ty), class∃(str, class0) ∨ interface∃(str, class0), ∀ sk. sk ∈ statfields(class0) → jvmref -- sk ∈ st ∧ is_fskey(sk) ∧ compat(str, st[jvmref -- sk], sk .fs .type, st) ⊦ okval(refval(r0), ty) ∧ ( is_referencevalue(refval(r0)) ∧ refval(r0) .refval ≠ jvmref → refval(r0) .refval -- _type ∈ st[r -- _type, typeval(mkclasstype(class))] ∧ is_typevalue(st[r -- _type, typeval(mkclasstype(class))][refval(r0) .refval -- _type]) ∧ is_reftype((st[r -- _type, typeval(mkclasstype(class))][refval(r0) .refval -- _type]) .type) ∧ ( has_classtype((st[r -- _type, typeval(mkclasstype(class))][refval(r0) .refval -- _type]) .type) → tdname+∃(str, (st[r -- _type, typeval(mkclasstype(class))][refval(r0) .refval -- _type]) .type .jtelemtype .class)) ∧ ( is_classtype((st[r -- _type, typeval(mkclasstype(class))][refval(r0) .refval -- _type]) .type) → class+∃(str, (st[r -- _type, typeval(mkclasstype(class))][refval(r0) .refval -- _type]) .type .class)) ∧ asgcomp(str, refval(r0), ty, st[r -- _type, typeval(mkclasstype(class))]))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 79:
st[jvmref -- mkfs(class1, ty, fieldvar) '] = refval(r0), jvmref -- mkfs(class1, ty, fieldvar) ' ∈ st, initdone(class0, st), is_predefined_class(class), newref(r, st), compatmode(str, st), compatrefs(str, st), mkfs(class1, ty, fieldvar) ' ∈ statfields(class0), jvmref ∈ st, okval(refval(r0), ty), r0 ≠ jvmref → r0 -- _type ∈ st ∧ is_typevalue(st[r0 -- _type]) ∧ is_reftype(st[r0 -- _type] .type) ∧ (has_classtype(st[r0 -- _type] .type) → tdname+∃(str, st[r0 -- _type] .type .jtelemtype .class)) ∧ (is_classtype(st[r0 -- _type] .type) → class+∃(str, st[r0 -- _type] .type .class)) ∧ is_subtype(str, st[r0 -- _type] .type, ty), class∃(str, class0) ∨ interface∃(str, class0), ∀ sk. sk ∈ statfields(class0) → jvmref -- sk ∈ st ∧ is_fskey(sk) ∧ compat(str, st[jvmref -- sk], sk .fs .type, st) ⊦ (ty = void_type ∨ is_reftype(ty)) ∧ ( r0 ≠ jvmref → (r0 = r ∨ r0 -- _type ∈ st) ∧ is_typevalue(st[r -- _type, typeval(mkclasstype(class))][r0 -- _type]) ∧ is_reftype((st[r -- _type, typeval(mkclasstype(class))][r0 -- _type]) .type) ∧ ( has_classtype((st[r -- _type, typeval(mkclasstype(class))][r0 -- _type]) .type) → class∃(str, (st[r -- _type, typeval(mkclasstype(class))][r0 -- _type]) .type .jtelemtype .class) ∨ interface∃(str, (st[r -- _type, typeval(mkclasstype(class))][r0 -- _type]) .type .jtelemtype .class) ∨ is_predefined_class((st[r -- _type, typeval(mkclasstype(class))][r0 -- _type]) .type .jtelemtype .class)) ∧ ( is_classtype((st[r -- _type, typeval(mkclasstype(class))][r0 -- _type]) .type) → class+∃(str, (st[r -- _type, typeval(mkclasstype(class))][r0 -- _type]) .type .class)) ∧ is_subtype(str, (st[r -- _type, typeval(mkclasstype(class))][r0 -- _type]) .type, ty))

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)])]]