[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 59 from proof compatstatic-mode (previous step)

jvmref -- mkfs(class0, ty, fieldvar) ' ∈ st, initdone(class, st), mkfs(class0, ty, fieldvar) ' ∈ statfields(class), jvmref ∈ st, okval(st[jvmref -- mkfs(class0, ty, fieldvar) '], ty), class∃(str, class) ∨ interface∃(str, class), ∀ sk. sk ∈ statfields(class) → jvmref -- sk ∈ st ∧ is_fskey(sk) ∧ compat(str, st[jvmref -- sk], sk .fs .type, st), is_referencevalue(st[jvmref -- mkfs(class0, ty, fieldvar) ']) ∧ st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval ≠ jvmref → st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type ∈ st ∧ is_typevalue(st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type]) ∧ is_reftype(st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type) ∧ ( has_classtype(st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type) → tdname+∃(str, st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type .jtelemtype .class)) ∧ ( is_classtype(st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type) → class+∃(str, st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type .class)) ∧ is_subtype(str, st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type, ty) ⊦ okval(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) '], ty) ∧ ( is_referencevalue(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) ∧ (st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval ≠ jvmref → (st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type ∈ st[_mode, val] ∧ is_typevalue(st[_mode, val][(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type]) ∧ is_reftype((st[_mode, val][(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type]) .type) ∧ ( has_classtype((st[_mode, val][(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type]) .type) → tdname+∃(str, (st[_mode, val][(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type]) .type .jtelemtype .class)) ∧ ( is_classtype((st[_mode, val][(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type]) .type) → class+∃(str, (st[_mode, val][(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type]) .type .class)) ∧ asgcomp(str, st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) '], ty, st[_mode, val]))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 58:
jvmref -- mkfs(class0, ty, fieldvar) ' ∈ st, initdone(class, st), mkfs(class0, ty, fieldvar) ' ∈ statfields(class), jvmref ∈ st, okval(st[jvmref -- mkfs(class0, ty, fieldvar) '], ty), class∃(str, class) ∨ interface∃(str, class), ∀ sk. sk ∈ statfields(class) → jvmref -- sk ∈ st ∧ is_fskey(sk) ∧ compat(str, st[jvmref -- sk], sk .fs .type, st), is_referencevalue(st[jvmref -- mkfs(class0, ty, fieldvar) ']) ∧ st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval ≠ jvmref → st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type ∈ st ∧ is_typevalue(st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type]) ∧ is_reftype(st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type) ∧ ( has_classtype(st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type) → tdname+∃(str, st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type .jtelemtype .class)) ∧ ( is_classtype(st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type) → class+∃(str, st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type .class)) ∧ is_subtype(str, st[st[jvmref -- mkfs(class0, ty, fieldvar) '] .refval -- _type] .type, ty) ⊦ okval(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) '], ty) ∧ ( is_referencevalue(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) ∧ (st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval ≠ jvmref → (st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type ∈ st ∧ is_typevalue(st[(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type]) ∧ is_reftype(st[(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type] .type) ∧ ( has_classtype(st[(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type] .type) → class∃(str, st[(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type] .type .jtelemtype .class) ∨ interface∃(str, st[(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type] .type .jtelemtype .class) ∨ is_predefined_class(st[(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type] .type .jtelemtype .class)) ∧ ( is_classtype(st[(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type] .type) → class+∃(str, st[(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _type] .type .class)) ∧ is_subtype(str, st[(st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) ']) .refval -- _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 ≠ jvmref → (st[_mode, val][r -- sk]) = st[r -- sk]], [CSIMPSEQ : ⊦ r -- _type ∈ st[_mode, val] ↔ r -- _type ∈ st])]]