[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 58 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 ∧ 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 weak cut applied rule cut formula

And obtained the following new goals

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

Rule argument

[fma-arg: jvmref -- mkfs(class0, ty, fieldvar) ' = _mode]

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ _mode = jvmref -- sk ↔ sk = mkfs (`java.lang.Object' .class, void_type, `mode' .field) '], [CSIMPSEQ : ⊦ fs ' = fs0 ' ↔ fs = fs0], [CSIMPSEQ : ⊦ mkfs(class, ty, fieldvar) = mkfs(class0, ty0, fieldvar0) ↔ class = class0 ∧ ty = ty0 ∧ fieldvar = fieldvar0], [CSIMPSEQ : ⊦ jvmref -- mkfs (`java.lang.Object' .class, void_type, `mode' .field) ' = _mode], [CSIMPSEQ : ⊦ okval(val, void_type) ↔ is_referencevalue(val)], [CSIMPSEQ : ⊦ ¬ mkfs (class0, void_type, fieldvar) ' ∈ statfields(class)])], [EXTRAFMAS : (jvmref -- mkfs(class0, ty, fieldvar) ' = _mode)]]