Proof step 1 from proof free-unknown (conclusion) (back to tree)

Heuristic weak unfold applied rule call right

And obtained the following new goals

• Proof step 2:

  ((r =>_ * hP))(h) ⊦ ⟪if ¬ r ∈ h then abort else h := h -- r⟫ hP(h)

Rule argument

Additional information

Used simplifier rules: free(r; h){if ¬ r ∈ h then abort else h := h -- r};

Proof step 2 from proof free-unknown (previous step) (back to tree)

Heuristic symbolic execution applied rule if negative right

And obtained the following new goals

• Proof step 3:

  ((r =>_ * hP))(h) ⊦ ⟪h := h -- r⟫ hP(h)

Rule argument

Additional information

Used simplifier rules: sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep ⊦ ((r =>_ * hP))(h) → r ∈ h; (s)

Proof step 3 from proof free-unknown (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 4:

  ((r =>_ * hP))(h), ¬ hP(h -- r) ⊦

Rule argument

Additional information

Proof step 4 from proof free-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ h1 ≡ h0 -- r → (((r =>_ * hP))(h0) ↔ hP(h1) ∧ r ∈ h0)

Rule argument

Additional information

Used simplifier rules: ⊦ h ≡ h; (s) Used terms: h -- r, h, hP, r

Proof step 5 from proof free-unknown (previous step) (back to tree)

A spec-lemma