[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 29 from proof initsubset-put-statfield-01 (previous step)

validstatfield(str, sk, st), sk ∈ statfields(class3), tdname∃(str, class3), initdone(class3, st0), initdone(class3, st), class ≠ class3 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ class2 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ class1 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ class0 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ `java.lang.Object' .class ∨ ty ≠ void_type ∨ fieldvar ≠ `uninit' .field, initdone(class0, st) → initdone(class0, st0), initerror(class1, st) → initerror(class1, st0), ∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0), ∀ class, sk. initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0), ¬ mkfs(class, ty, fieldvar) ' ∈ statfields(class) ∨ ¬ tdname∃(str, class), ty ≠ void_type ∨ fieldvar ≠ `initstate' .field ∧ (class ≠ `java.lang.Object' .class ∨ fieldvar ≠ `uninit' .field) ⊦ validstatfield(str, sk, st0[jvmref -- mkfs(class, ty, fieldvar) ', val])

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 14:
⊦ sk ≠ sk0 ∧ ( ¬ is_fskey(sk) ∨ sk .fs .type ≠ void_type ∨ sk .fs ≠ mkfs(`java.lang.Object' .class, void_type, `uninit' .field) ∧ (¬ is_fskey(sk0) ∨ sk .fs ≠ mkfs(sk0 .fs .class, void_type, `initstate' .field))) → (validstatfield(str, sk0, st[jvmref -- sk, val]) ↔ validstatfield(str, sk0, st))
Proof step 26:
¬ ( mkfs(class, ty, fieldvar) ' ≠ sk ∧ ( ¬ is_fskey(mkfs(class, ty, fieldvar) ') ∨ mkfs(class, ty, fieldvar) ' .fs .type ≠ void_type ∨ mkfs(class, ty, fieldvar) ' .fs ≠ mkfs(`java.lang.Object' .class, void_type, `uninit' .field) ∧ (¬ is_fskey(sk) ∨ mkfs(class, ty, fieldvar) ' .fs ≠ mkfs(sk .fs .class, void_type, `initstate' .field)))), validstatfield(str, sk, st), sk ∈ statfields(class3), tdname∃(str, class3), initdone(class3, st0), initdone(class3, st), class ≠ class3 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ class2 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ class1 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ class0 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ `java.lang.Object' .class ∨ ty ≠ void_type ∨ fieldvar ≠ `uninit' .field, initdone(class0, st) → initdone(class0, st0), initerror(class1, st) → initerror(class1, st0), ∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0), ∀ class, sk. initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0), ¬ mkfs(class, ty, fieldvar) ' ∈ statfields(class) ∨ ¬ tdname∃(str, class), ty ≠ void_type ∨ fieldvar ≠ `initstate' .field ∧ (class ≠ `java.lang.Object' .class ∨ fieldvar ≠ `uninit' .field) ⊦ validstatfield(str, sk, st0[jvmref -- mkfs(class, ty, fieldvar) ', val])
Proof step 28:
mkfs(class, ty, fieldvar) ' ≠ sk ∧ ( ¬ is_fskey(mkfs(class, ty, fieldvar) ') ∨ mkfs(class, ty, fieldvar) ' .fs .type ≠ void_type ∨ mkfs(class, ty, fieldvar) ' .fs ≠ mkfs(`java.lang.Object' .class, void_type, `uninit' .field) ∧ (¬ is_fskey(sk) ∨ mkfs(class, ty, fieldvar) ' .fs ≠ mkfs(sk .fs .class, void_type, `initstate' .field))), validstatfield(str, sk, st), sk ∈ statfields(class3), tdname∃(str, class3), initdone(class3, st0), initdone(class3, st), class ≠ class3 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ class2 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ class1 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ class0 ∨ ty ≠ void_type ∨ fieldvar ≠ `initstate' .field, class ≠ `java.lang.Object' .class ∨ ty ≠ void_type ∨ fieldvar ≠ `uninit' .field, initdone(class0, st) → initdone(class0, st0), initerror(class1, st) → initerror(class1, st0), ∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0), ∀ class, sk. initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0), ¬ mkfs(class, ty, fieldvar) ' ∈ statfields(class) ∨ ¬ tdname∃(str, class), ty ≠ void_type ∨ fieldvar ≠ `initstate' .field ∧ (class ≠ `java.lang.Object' .class ∨ fieldvar ≠ `uninit' .field) ⊦ validstatfield(str, sk, st0)

Rule argument

[crewrite-arg: validstatfield-put-statfield , F , [val, sk, st, sk0, str] → [val, mkfs(class, ty, fieldvar) ', st0, sk, str] ]

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (val, mkfs(class, ty, fieldvar) ', st0, sk, str)]]