[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 30 from proof validrefs-junkrefs (previous step)

r1 ' + refs1 = refs + r0 ' + refs0, st[r -- mkfs(class, ty1, fieldvar) '] = refval(r1), validrefs(str, refs, ty1, st), mkfs(class, ty1, fieldvar) ' ∈ instfields(st[r -- _type] .type .class), is_obj(str, r, st), st[r -- _type] .type ≤ ty, junkrefs(str, r1 ' + refs1, ty1, st), r1 ∈ refs, ∀ str0, ty0, st0. junkrefs(str0, r1 ' + refs1, ty0, st0) → (∃ refs, r0, refs0. r1 ' + refs1 = refs + r0 ' + refs0 ∧ validrefs(str0, refs, ty0, st0) ∧ r0 ≠ jvmref ∧ ( ¬ is_valid_ref(str0, r0, st0) ∨ refs = [] ∧ ¬ st0[r0 -- _type] .type ≤ ty0 ∨ refs ≠ [] ∧ ( is_obj(refs .last, st0) ∧ (∃ fs. fs ' ∈ instfields(st0[refs .last -- _type] .type .class) ∧ is_referencevalue(st0[refs .last -- fs ']) ∧ r0 = st0[refs .last -- fs '] .refval ∧ ¬ st0[st0[refs .last -- fs '] .refval -- _type] .type ≤ fs .type) ∨ is_array(refs .last, st0) ∧ (∃ i. 0 ≤ i ∧ i < st0[refs .last -- _length] .intval ∧ is_referencevalue(st0[refs .last -- i ']) ∧ r0 = st0[refs .last -- i '] .refval ∧ ¬ st0[st0[refs .last -- i '] .refval -- _type] .type ≤ st0[refs .last -- _type] .type .type)))), ¬ is_valid_ref(str, r0, st) ∨ is_obj(refs .last, st) ∧ mkfs(class0, ty2, fieldvar0) ' ∈ instfields(st[refs .last -- _type] .type .class) ∧ is_referencevalue(st[refs .last -- mkfs(class0, ty2, fieldvar0) ']) ∧ r0 = st[refs .last -- mkfs(class0, ty2, fieldvar0) '] .refval ∧ ¬ st[st[refs .last -- mkfs(class0, ty2, fieldvar0) '] .refval -- _type] .type ≤ ty2 ∨ is_array(refs .last, st) ∧ 0 ≤ i ∧ i < st[refs .last -- _length] .intval ∧ is_referencevalue(st[refs .last -- i ']) ∧ r0 = st[refs .last -- i '] .refval ∧ ¬ st[st[refs .last -- i '] .refval -- _type] .type ≤ st[refs .last -- _type] .type .type ⊦ refs = [], r0 = jvmref, r = jvmref, validrefs(str, r ' + refs, ty, st)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 21:
⊦ is_obj(str, r, st) ∧ st[r -- _type] .type ≤ ty → ( validrefs(str, r ' + refs, ty, st) ↔ refs = [] ∨ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ refs .first = st[r -- fs '] .refval ∧ validrefs(str, refs, fs .type, st)))
Proof step 29:
is_obj(str, r, st) ∧ st[r -- _type] .type ≤ ty, r1 ' + refs1 = refs + r0 ' + refs0, st[r -- mkfs(class, ty1, fieldvar) '] = refval(r1), validrefs(str, refs, ty1, st), mkfs(class, ty1, fieldvar) ' ∈ instfields(st[r -- _type] .type .class), is_obj(str, r, st), st[r -- _type] .type ≤ ty, junkrefs(str, r1 ' + refs1, ty1, st), r1 ∈ refs, ∀ str0, ty0, st0. junkrefs(str0, r1 ' + refs1, ty0, st0) → (∃ refs, r0, refs0. r1 ' + refs1 = refs + r0 ' + refs0 ∧ validrefs(str0, refs, ty0, st0) ∧ r0 ≠ jvmref ∧ ( ¬ is_valid_ref(str0, r0, st0) ∨ refs = [] ∧ ¬ st0[r0 -- _type] .type ≤ ty0 ∨ refs ≠ [] ∧ ( is_obj(refs .last, st0) ∧ (∃ fs. fs ' ∈ instfields(st0[refs .last -- _type] .type .class) ∧ is_referencevalue(st0[refs .last -- fs ']) ∧ r0 = st0[refs .last -- fs '] .refval ∧ ¬ st0[st0[refs .last -- fs '] .refval -- _type] .type ≤ fs .type) ∨ is_array(refs .last, st0) ∧ (∃ i. 0 ≤ i ∧ i < st0[refs .last -- _length] .intval ∧ is_referencevalue(st0[refs .last -- i ']) ∧ r0 = st0[refs .last -- i '] .refval ∧ ¬ st0[st0[refs .last -- i '] .refval -- _type] .type ≤ st0[refs .last -- _type] .type .type)))), ¬ is_valid_ref(str, r0, st) ∨ is_obj(refs .last, st) ∧ mkfs(class0, ty2, fieldvar0) ' ∈ instfields(st[refs .last -- _type] .type .class) ∧ is_referencevalue(st[refs .last -- mkfs(class0, ty2, fieldvar0) ']) ∧ r0 = st[refs .last -- mkfs(class0, ty2, fieldvar0) '] .refval ∧ ¬ st[st[refs .last -- mkfs(class0, ty2, fieldvar0) '] .refval -- _type] .type ≤ ty2 ∨ is_array(refs .last, st) ∧ 0 ≤ i ∧ i < st[refs .last -- _length] .intval ∧ is_referencevalue(st[refs .last -- i ']) ∧ r0 = st[refs .last -- i '] .refval ∧ ¬ st[st[refs .last -- i '] .refval -- _type] .type ≤ st[refs .last -- _type] .type .type ⊦ refs = [], r0 = jvmref, r = jvmref, refs = [] ∨ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ refs .first = st[r -- fs '] .refval ∧ validrefs(str, refs, fs .type, st))

Rule argument

[crewrite-arg: validrefs-class , F , [st, ty, refs, r, str] → [st, ty, refs, r, str] ]

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, ty, refs, r, str)]]