[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 60 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) ⊦ compat(str, st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) '], ty, st[_mode, val])

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 54:
⊦ compat(str, val, ty, st) ↔ okval(val, ty) ∧ ( is_referencevalue(val) ∧ val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ is_reftype(st[val .refval -- _type] .type) ∧ (has_classtype(st[val .refval -- _type] .type) → tdname+∃(str, st[val .refval -- _type] .type .jtelemtype .class)) ∧ (is_classtype(st[val .refval -- _type] .type) → class+∃(str, st[val .refval -- _type] .type .class)) ∧ asgcomp(str, val, ty, st))
Proof step 59:
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]))

Rule argument

[crewrite-arg: value-compat , F , [st, ty, val, str] → [st[_mode, val], ty, st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) '], str] ]

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[_mode, val], ty, st[_mode, val][jvmref -- mkfs(class0, ty, fieldvar) '], str)]]