[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 57 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) ⊦ jvmref -- mkfs(class0, ty, fieldvar) ' = _mode, 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))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 56:
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) ⊦ ty = void_type, 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 : ⊦ ¬ mkfs (class0, void_type, fieldvar) ' ∈ statfields(class)], [CSIMPSEQ : ⊦ okval(val, void_type) ↔ is_referencevalue(val)], [CSIMPSEQ : ⊦ mkfs(class1, ty, fieldvar) = mkfs(class2, ty0, fieldvar0) ↔ ¬ ¬ ( class1 = class2 ∧ ty = ty0 ∧ fieldvar = fieldvar0)], [CSIMPSEQ : ⊦ fs ' = fs0 ' ↔ fs = fs0], [CSIMPSEQ : ⊦ _mode = jvmref -- sk ↔ sk = mkfs (`java.lang.Object' .class, void_type, `mode' .field) '])]]