Proof step 1 from proof alloc-refset (conclusion) (back to tree)

Heuristic unfold applied rule call right

And obtained the following new goals

• Proof step 2:

  hP(h), dom h ⊆ rs ⊦ ⟪choose r0 with ¬ r0 ∈ rs ∧ r0 ≠ null in r := r0, h := h ++ r0⟫ (((r =>_ * hP))(h) ∧ ¬ r ∈ rs)

Rule argument

Additional information

Used simplifier rules: alloc#(rs; r, h){choose r0 with ¬ r0 ∈ rs ∧ r0 ≠ null in r := r0, h := h ++ r0};

Proof step 2 from proof alloc-refset (previous step) (back to tree)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 3:

  r0 ≠ null, hP(h), dom h ⊆ rs, ¬ r0 ∈ rs ⊦ ⟪r := r0, h := h ++ r0⟫ (((r =>_ * hP))(h) ∧ ¬ r ∈ rs)

• Proof step 9:

  hP(h), dom h ⊆ rs, ∀ r0. ¬(¬ r0 ∈ rs ∧ r0 ≠ null) ⊦ ⟪abort⟫ (((r =>_ * hP))(h) ∧ ¬ r ∈ rs)

Rule argument

Additional information

Proof step 3 from proof alloc-refset (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 4:

  r0 ≠ null, hP(h), dom h ⊆ rs, ¬ r0 ∈ rs ⊦ ((r0 =>_ * hP))(h ++ r0) ∧ ¬ r0 ∈ rs

Rule argument

Additional information

Proof step 4 from proof alloc-refset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  r0 ≠ null, hP(h), dom h ⊆ rs, ¬ ((r0 =>_ * hP))(h ++ r0), ¬ r0 ∈ rs ⊦

Rule argument

Additional information

Proof step 5 from proof alloc-refset (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2)

• Proof step 7:

  r0 ≠ null, hP(h), ¬ ((r0 =>_ * hP))(h ++ r0), ¬ r0 ∈ rs, ∀ a. a ∈ dom h → a ∈ rs ⊦

Rule argument

Additional information

Used terms: dom h, rs

Proof step 6 from proof alloc-refset (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof alloc-refset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  r0 ≠ null, hP(h), ¬ ((r0 =>_ * hP))(h ++ r0), ¬ r0 ∈ rs, ∀ a. a ∈ h → a ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ dom h ↔ r ∈ h; (s)

Proof step 8 from proof alloc-refset (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ¬ r ∈ h, r ≠ null ⊦ ((r =>_ * hP))(h ++ r) ↔ hP(h); (ss) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep Used terms: r0

Proof step 9 from proof alloc-refset (previous step) (back to tree)

Heuristic symbolic execution applied rule abort right

And obtained the following new goals

• Proof step 10:

  hP(h), dom h ⊆ rs, ∀ r0. ¬(¬ r0 ∈ rs ∧ r0 ≠ null) ⊦

Rule argument

Additional information

Proof step 10 from proof alloc-refset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  hP(h), dom h ⊆ rs, ∀ r0. r0 ∈ rs ∨ r0 = null ⊦

Rule argument

Additional information

Proof step 11 from proof alloc-refset (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 12:

  ⊦ ∃ r. ¬ r ∈ rs ∧ r ≠ null

• Proof step 13:

  hP(h), dom h ⊆ rs, ∀ r0. r0 ∈ rs ∨ r0 = null, ∃ r. ¬ r ∈ rs ∧ r ≠ null ⊦

Rule argument

Additional information

Used terms: rs

Proof step 12 from proof alloc-refset (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof alloc-refset (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  r ≠ null, hP(h), dom h ⊆ rs, ¬ r ∈ rs, ∀ r0. r0 ∈ rs ∨ r0 = null ⊦

Rule argument

Additional information

Proof step 14 from proof alloc-refset (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r