Proof step 5 from proof junkrefs-put-nopathexplus-equiv (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ ¬ path∃(str, r, r0, st) ∧ ¬ junkrefs(str, refs, ty, st) ∧ sk ≠ _type ∧ refs ≠ [] ∧ refs .first = r → ¬ junkrefs(str, refs, ty, st[r0 -- sk, val])

• Proof step 4:

  ¬ ( ¬ path∃(str, (r ' + refs0) .first, r0, st) ∧ ¬ junkrefs(str, r ' + refs0, ty, st) ∧ sk ≠ _type ∧ r ' + refs0 ≠ [] ∧ (r ' + refs0) .first = (r ' + refs0) .first), junkrefs(str, r ' + refs0, ty, st[r0 -- sk, val]) ⊦ junkrefs(str, r ' + refs0, ty, st), sk = _type, path∃+(str, r, r0, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (str, (r ' + refs0) .first, r0, st, r ' + refs0, ty, sk, val)]]