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

junkrefs(str, r ' + acc, ty, st), ∀ str0, ty0, st0. junkrefs(str0, acc, ty0, st0) → (∃ refs, r0, refs0. acc = 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)))) ⊦ r = jvmref, ∃ refs, r0, refs0. r ' + acc = refs + r0 ' + refs0 ∧ validrefs(str, refs, ty, st) ∧ r0 ≠ jvmref ∧ ( ¬ is_valid_ref(str, r0, st) ∨ refs = [] ∧ ¬ st[r0 -- _type] .type ≤ ty ∨ refs ≠ [] ∧ ( is_obj(refs .last, st) ∧ (∃ fs. fs ' ∈ instfields(st[refs .last -- _type] .type .class) ∧ is_referencevalue(st[refs .last -- fs ']) ∧ r0 = st[refs .last -- fs '] .refval ∧ ¬ st[st[refs .last -- fs '] .refval -- _type] .type ≤ fs .type) ∨ is_array(refs .last, st) ∧ (∃ i. ¬ i < 0 ∧ ¬ st[refs .last -- _length] .intval ≤ i ∧ 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)))

User applied rule exists right

And obtained the following new goals

Proof step 94:
junkrefs(str, r ' + acc, ty, st), ∀ str0, ty0, st0. junkrefs(str0, acc, ty0, st0) → (∃ refs, r0, refs0. acc = 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)))) ⊦ r = jvmref, r ' + acc = [] + r ' + acc ∧ validrefs(str, [], ty, st) ∧ r ≠ jvmref ∧ ( ¬ is_valid_ref(str, r, st) ∨ [] = [] ∧ ¬ st[r -- _type] .type ≤ ty ∨ [] ≠ [] ∧ ( is_obj([] .last, st) ∧ (∃ fs. fs ' ∈ instfields(st[[] .last -- _type] .type .class) ∧ is_referencevalue(st[[] .last -- fs ']) ∧ r = st[[] .last -- fs '] .refval ∧ ¬ st[st[[] .last -- fs '] .refval -- _type] .type ≤ fs .type) ∨ is_array([] .last, st) ∧ (∃ i. ¬ i < 0 ∧ ¬ st[[] .last -- _length] .intval ≤ i ∧ is_referencevalue(st[[] .last -- i ']) ∧ r = st[[] .last -- i '] .refval ∧ ¬ st[st[[] .last -- i '] .refval -- _type] .type ≤ st[[] .last -- _type] .type .type))), ∃ refs, r0, refs0. r ' + acc = refs + r0 ' + refs0 ∧ validrefs(str, refs, ty, st) ∧ r0 ≠ jvmref ∧ ( ¬ is_valid_ref(str, r0, st) ∨ refs = [] ∧ ¬ st[r0 -- _type] .type ≤ ty ∨ refs ≠ [] ∧ ( is_obj(refs .last, st) ∧ (∃ fs. fs ' ∈ instfields(st[refs .last -- _type] .type .class) ∧ is_referencevalue(st[refs .last -- fs ']) ∧ r0 = st[refs .last -- fs '] .refval ∧ ¬ st[st[refs .last -- fs '] .refval -- _type] .type ≤ fs .type) ∨ is_array(refs .last, st) ∧ (∃ i. ¬ i < 0 ∧ ¬ st[refs .last -- _length] .intval ≤ i ∧ 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)))

Rule argument

[EXRARG : pos: right 2, [extquanttermlist: ([], r, acc) abort:F , discard:F , computed:F ]]

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : ([], r, acc)]]