Proof step 14 from proof disjoint-nopathex (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ disjoint(str, refs, st) ↔ ¬ (∃ refs1, refs2. refs1 ≠ [] ∧ refs2 ≠ [] ∧ refs1 .first ∈ refs ∧ refs2 .first ∈ refs ∧ refs1 .first ≠ refs2 .first ∧ refs1 .last = refs2 .last ∧ refs1 .last ≠ jvmref ∧ validrefs(str, refs1, st[refs1 .first -- _type] .type, st) ∧ validrefs(str, refs2, st[refs2 .first -- _type] .type, st))

• Proof step 13:

  path∃(str, r, r1, st), ∀ refs1, refs2. ¬ ( refs1 ≠ [] ∧ refs2 ≠ [] ∧ refs1 .first ∈ r ' + r0 ' ∧ refs2 .first ∈ r ' + r0 ' ∧ refs1 .first ≠ refs2 .first ∧ refs1 .last = refs2 .last ∧ refs1 .last ≠ jvmref ∧ validrefs(str, refs1, st[refs1 .first -- _type] .type, st) ∧ validrefs(str, refs2, st[refs2 .first -- _type] .type, st)), path∃(str, r0, r1, st) ⊦ r = r0, r1 = jvmref

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, r ' + r0 ', str)]]