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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(((!(me, hO1, hP) * hP0))(h1) ↔ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r)), r ≠ null, rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ r ∈ h1 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(((!(me, hO1, hP) * hP0))(h1) ↔ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r)), r ≠ null, rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ r ∈ h1 ⊦

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  r ≠ null, ((!(me, hO1, hP) * hP0))(h1), rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1 ⊦

• Proof step 41:

  r ≠ null, ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1 ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 5:

  ¬ r ∈ h, r ≠ null ⊦ ((r =>_ * hP))(h ++ r) ↔ hP(h)

• Proof step 6:

  ((r =>_ * !(me, hO1, hP) * hP0))(h1 ++ r) ↔ ((!(me, hO1, hP) * hP0))(h1), r ≠ null, ((!(me, hO1, hP) * hP0))(h1), rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used terms: r, h1, !(me, hO1, hP) * hP0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  r ≠ null, ((!(me, hO1, hP) * hP0))(h1), ((r =>_ * !(me, hO1, hP) * hP0))(h1 ++ r), rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1 ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 8:

  ⊦ r =>_ = !(me, hO(r; me), r =>_)

• Proof step 9:

  r =>_ = !(me, hO1(r; me), r =>_), r ≠ null, ((r =>_ * !(me, hO1, hP) * hP0))(h1 ++ r), ((!(me, hO1, hP) * hP0))(h1), rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used terms: r, me, hO1

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

Lemma lift-mapex

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  r =>_ = !(me, hO2, r =>_), r ≠ null, ((!(me, hO1, hP) * hP0))(h1), ((r =>_ * !(me, hO1, hP) * hP0))(h1 ++ r), rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used simplifier rules: switch-ownership: ⊦ rely(me, hO1, h1, hO2, h2) → !(me, hO1, hP) = !(me, hO2, hP);

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

User applied rule weakening

And obtained the following new goals

• Proof step 11:

  r =>_ = !(me, hO2, r =>_), r ≠ null, ((r =>_ * !(me, hO1, hP) * hP0))(h1 ++ r), rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ ((hP0 * hP1))(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 13:

  r =>_ = !(me, hO2, r =>_), r ≠ null, rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1, ∃ h0, h2. h0 ⊥ h2 ∧ h1 ++ r = h0 ∪ h2 ∧ r =>_(h0) ∧ ((!(me, hO1, hP) * hP0))(h2) ⊦

Rule argument

Additional information

Used terms: h1 ++ r, !(me, hO1, hP) * hP0, r =>_

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  h1 ++ r = h0 ∪ h, r =>_ = !(me, hO2, r =>_), r ≠ null, ((!(me, hO1, hP) * hP0))(h), r =>_(h0), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ ((hP0 * hP1))(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 16:

  h1 ++ r = h0 ∪ h, r =>_ = !(me, hO2, r =>_), r ≠ null, r =>_(h0), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1, ∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ !(me, hO1, hP)(h0) ∧ hP0(h1) ⊦

Rule argument

Additional information

Used terms: h, hP0, !(me, hO1, hP)

Proof step 15 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  h1 ++ r = h0 ∪ h3 ∪ h4, r =>_ = !(me, hO2, r =>_), r ≠ null, !(me, hO1, hP)(h3), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h1 ⊥ h → (h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h); (ws)

Proof step 17 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ !(me, hO, hP0) * !(me, hO, hP1) = !(me, hO, hP0 * hP1)

• Proof step 19:

  h1 ++ r = h0 ∪ h3 ∪ h4, r =>_ = !(me, hO2, r =>_), r ≠ null, !(me, hO1, hP)(h3), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ (((!(me, hO2, r =>_) * !(me, hO2, hP)) * hP0))(h1 ++ r), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used terms: hP, r =>_, hO2, me

Proof step 18 from proof alloc-p (previous step) (back to tree)

Lemma compact-local

Proof step 19 from proof alloc-p (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 20:

  h1 ++ r = h0 ∪ h3 ∪ h4, r =>_ = !(me, hO2, r =>_), r ≠ null, !(me, hO1, hP)(h3), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h0 ∪ h3 ∪ h4, hO2, h2), h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ (((!(me, hO2, r =>_) * !(me, hO2, hP)) * hP0))(h0 ∪ h3 ∪ h4), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Proof step 20 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2

• Proof step 22:

  h1 ++ r = h0 ∪ h3 ∪ h4, r =>_ = !(me, hO2, r =>_), r ≠ null, !(me, hO1, hP)(h3), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h0 ∪ h3 ∪ h4, hO2, h2), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ ((!(me, hO2, r =>_) * !(me, hO2, hP) * hP0))(h0 ∪ h3 ∪ h4), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used terms: hP0, !(me, hO2, hP), !(me, hO2, r =>_)

Proof step 21 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → ((hP0 * hP1))(h0 ∪ h1)

• Proof step 24:

  h1 ++ r = h0 ∪ h3 ∪ h4, r =>_ = !(me, hO2, r =>_), r ≠ null, !(me, hO1, hP)(h3), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h0 ∪ h3 ∪ h4, hO2, h2), h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(me, hO2, r =>_) * !(me, hO2, hP) * hP0))(h0 ∪ h3 ∪ h4), ¬ r ∈ h1 ⊦ !(me, hO2, r =>_)(h0) ∧ ((!(me, hO2, hP) * hP0))(h3 ∪ h4) ∧ h0 ⊥ h3 ∪ h4

Rule argument

Additional information

Used terms: h3 ∪ h4, h0, !(me, hO2, hP) * hP0, !(me, hO2, r =>_)

Proof step 23 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  h1 ++ r = h0 ∪ h3 ∪ h4, r =>_ = !(me, hO2, r =>_), r ≠ null, !(me, hO1, hP)(h3), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ ((!(me, hO2, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used simplifier rules: compact-local: ⊦ !(me, hO, hP0) * !(me, hO, hP1) = !(me, hO, hP0 * hP1); ⊦ h1 ⊥ h → (h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h); (ws) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep

Proof step 25 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → ((hP0 * hP1))(h0 ∪ h1)

• Proof step 27:

  h1 ++ r = h0 ∪ h3 ∪ h4, r =>_ = !(me, hO2, r =>_), r ≠ null, !(me, hO1, hP)(h3), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ ((!(me, hO2, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1 ⊦ !(me, hO2, hP)(h3) ∧ hP0(h4) ∧ h3 ⊥ h4

Rule argument

Additional information

Used terms: h4, h3, hP0, !(me, hO2, hP)

Proof step 26 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  h1 ++ r = h0 ∪ h3 ∪ h4, r =>_ = !(me, hO2, r =>_), r ≠ null, !(me, hO1, hP)(h3), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ !(me, hO2, hP)(h3), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ ((!(me, hO2, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Proof step 28 from proof alloc-p (previous step) (back to tree)

User applied rule weakening

And obtained the following new goals

• Proof step 29:

  h1 ++ r = h0 ∪ h3 ∪ h4, r ≠ null, !(me, hO1, hP)(h3), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ !(me, hO2, hP)(h3), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ ((!(me, hO2, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Proof step 29 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ !(id, of, hP)(h) ↔ hP(h) ∧ (∀ r. r ∈ h → of(r) = id)

• Proof step 31:

  h1 ++ r = h0 ∪ h3 ∪ h4, r ≠ null, hP(h3), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ !(me, hO2, hP)(h3), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ ((!(me, hO2, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1, ∀ r. r ∈ h3 → hO1(r) = me ⊦

Rule argument

Additional information

Used terms: h3, hP, hO1, me

Proof step 30 from proof alloc-p (previous step) (back to tree)

Lemma owned

Proof step 31 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  h1 ++ r = h0 ∪ h3 ∪ h4, r ≠ null, hP(h3), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ !(me, hO2, hP)(h3), ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ ((!(me, hO2, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1, ∀ r. r ∈ h3 → hO1(r) = me ⊦

Rule argument

Additional information

Proof step 32 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ !(id, of, hP)(h) ↔ hP(h) ∧ (∀ r. r ∈ h → of(r) = id)

• Proof step 34:

  h1 ++ r = h0 ∪ h3 ∪ h4, r ≠ null, hP(h3), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ ((!(me, hO2, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1, ∀ r. r ∈ h3 → hO1(r) = me, ¬ hP(h3) ∨ (∃ r. ¬(r ∈ h3 → hO2(r) = me)) ⊦

Rule argument

Additional information

Used terms: h3, hP, hO2, me

Proof step 33 from proof alloc-p (previous step) (back to tree)

Lemma owned

Proof step 34 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  h1 ++ r = h0 ∪ h3 ∪ h4, hO2(r0) ≠ me, r ≠ null, hP(h3), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), r0 ∈ h3, h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ ((!(me, hO2, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1, ∀ r. r ∈ h3 → hO1(r) = me ⊦

Rule argument

Additional information

Proof step 35 from proof alloc-p (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 36:

  h1 ++ r = h0 ∪ h3 ∪ h4, hO2(r0) ≠ me, r ≠ null, hP(h3), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), r0 ∈ h3, h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(me, hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ ((!(me, hO2, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1, r0 ∈ h3 → hO1(r0) = me ⊦

Rule argument

Additional information

Used terms: r0

Proof step 36 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  h1 ++ r = h0 ∪ h3 ∪ h4, hO2(r0) ≠ hO1(r0), r ≠ null, hP(h3), hP0(h4), rely(hO1(r0), hO1(r; hO1(r0)), h1 ++ r, hO2, h2), r0 ∈ h3, h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(hO1(r0), hO2, hP) * hP0))(h3 ∪ h4), ¬ ((!(hO1(r0), hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Proof step 37 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

  ⊦ rely(me, of1, h1, of2, h2) ↔ (∀ r. (of1(r) = me ↔ of2(r) = me) ∧ (of1(r) = me → (r ∈ h1 ↔ r ∈ h2) ∧ (r ∈ h1 → h1[r] = h2[r])))

• Proof step 39:

  h1 ++ r = h0 ∪ h3 ∪ h4, hO2(r0) ≠ hO1(r0), r ≠ null, hP(h3), hP0(h4), r0 ∈ h3, h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ ((!(hO1(r0), hO2, hP) * hP0))(h3 ∪ h4), ¬ ((!(hO1(r0), hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1, ∀ r1. (hO1(r; hO1(r0))(r1) = hO1(r0) ↔ hO2(r1) = hO1(r0)) ∧ (hO1(r; hO1(r0))(r1) = hO1(r0) → (r1 ∈ h1 ++ r ↔ r1 ∈ h2) ∧ (r1 ∈ h1 ++ r → (h1 ++ r)[r1] = h2[r1])) ⊦

Rule argument

Additional information

Used terms: hO2, hO1(r; hO1(r0)), hO1(r0), h1 ++ r, h2

Proof step 38 from proof alloc-p (previous step) (back to tree)

Lemma rely

Proof step 39 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  h1 ++ r = h0 ∪ h3 ∪ h4, hO2(r0) ≠ hO1(r0), r ≠ null, hP(h3), hP0(h4), r0 ∈ h3, h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(hO1(r0), hO2, hP) * hP0))(h3 ∪ h4), ¬ ((!(hO1(r0), hO2, r =>_ * hP) * hP0))(h1 ++ r), ¬ r ∈ h1, ∀ r1. ((r = r1 ⊃ hO1(r0);hO1(r1)) = hO1(r0) ↔ hO2(r1) = hO1(r0)) ∧ ((r = r1 ⊃ hO1(r0);hO1(r1)) = hO1(r0) → (r1 = r ∨ r1 ∈ h1 ↔ r1 ∈ h2) ∧ (r1 = r ∨ r1 ∈ h1 → (h1 ++ r)[r1] = h2[r1])) ⊦

Rule argument

Additional information

Used simplifier rules: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s)

Proof step 40 from proof alloc-p (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0

Proof step 41 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  ⊦ !(me, hO, hP0) * !(me, hO, hP1) = !(me, hO, hP0 * hP1)

• Proof step 43:

  r ≠ null, (((!(me, hO2, r =>_) * !(me, hO2, hP)) * hP0))(h1 ++ r), rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used terms: hP, r =>_, hO2, me

Proof step 42 from proof alloc-p (previous step) (back to tree)

Lemma compact-local

Proof step 43 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

  ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2

• Proof step 45:

  r ≠ null, ((!(me, hO2, r =>_) * !(me, hO2, hP) * hP0))(h1 ++ r), rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used terms: hP0, !(me, hO2, hP), !(me, hO2, r =>_)

Proof step 44 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

  ⊦ ((hP0 * hP1))(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 47:

  r ≠ null, rely(me, hO1(r; me), h1 ++ r, hO2, h2), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1, ∃ h0, h2. h0 ⊥ h2 ∧ h1 ++ r = h0 ∪ h2 ∧ !(me, hO2, r =>_)(h0) ∧ ((!(me, hO2, hP) * hP0))(h2) ⊦

Rule argument

Additional information

Used terms: h1 ++ r, !(me, hO2, hP) * hP0, !(me, hO2, r =>_)

Proof step 46 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 47 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  h1 ++ r = h0 ∪ h, r ≠ null, !(me, hO2, r =>_)(h0), ((!(me, hO2, hP) * hP0))(h), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Proof step 48 from proof alloc-p (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 49:

  ¬ r ∈ h, r ≠ null ⊦ ((r =>_ * hP))(h ++ r) ↔ hP(h)

• Proof step 50:

  h1 ++ r = h0 ∪ h, ((r =>_ * !(me, hO1, hP) * hP0))(h1 ++ r) ↔ ((!(me, hO1, hP) * hP0))(h1), r ≠ null, !(me, hO2, r =>_)(h0), ((!(me, hO2, hP) * hP0))(h), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used terms: r, h1, !(me, hO1, hP) * hP0

Proof step 49 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof alloc-p (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 51:

  h1 ++ r = h0 ∪ h, r ≠ null, !(me, hO2, r =>_)(h0), ((!(me, hO2, hP) * hP0))(h), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h, ¬ ((r =>_ * !(me, hO1, hP) * hP0))(h1 ++ r), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Proof step 51 from proof alloc-p (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 52:

  h1 ++ r = h0 ∪ h, r ≠ null, !(me, hO2, r =>_)(h0), ((!(me, hO2, hP) * hP0))(h), rely(me, hO1(r; me), h0 ∪ h, hO2, h2), h0 ⊥ h, ¬ ((r =>_ * !(me, hO1, hP) * hP0))(h0 ∪ h), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Proof step 52 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 53:

  ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → ((hP0 * hP1))(h0 ∪ h1)

• Proof step 54:

  h1 ++ r = h0 ∪ h, r ≠ null, !(me, hO2, r =>_)(h0), ((!(me, hO2, hP) * hP0))(h), rely(me, hO1(r; me), h0 ∪ h, hO2, h2), h0 ⊥ h, ¬ ((r =>_ * !(me, hO1, hP) * hP0))(h0 ∪ h), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1 ⊦ r =>_(h0) ∧ ((!(me, hO1, hP) * hP0))(h) ∧ h0 ⊥ h

Rule argument

Additional information

Used terms: h, h0, !(me, hO1, hP) * hP0, r =>_

Proof step 53 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 54 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  h1 ++ r = h0 ∪ h, r ≠ null, !(me, hO2, r =>_)(h0), ((!(me, hO2, hP) * hP0))(h), r =>_(h0), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ ((!(me, hO1, hP) * hP0))(h), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used simplifier rules: owned-P: ⊦ !(me, hO, hP)(h) ∧ ¬ hP(h) → false; sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ¬ r ∈ h, r ≠ null ⊦ ((r =>_ * hP))(h ++ r) ↔ hP(h); (ss)

Proof step 55 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

  ⊦ ((hP0 * hP1))(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 57:

  h1 ++ r = h0 ∪ h, r ≠ null, !(me, hO2, r =>_)(h0), r =>_(h0), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ ((!(me, hO1, hP) * hP0))(h), ¬ r ∈ h1, ∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ !(me, hO2, hP)(h0) ∧ hP0(h1) ⊦

Rule argument

Additional information

Used terms: h, hP0, !(me, hO2, hP)

Proof step 56 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 57 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  h1 ++ r = h0 ∪ h3 ∪ h4, r ≠ null, !(me, hO2, r =>_)(h0), !(me, hO2, hP)(h3), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ ((!(me, hO1, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h1 ⊥ h → (h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h); (ws)

Proof step 58 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 59:

  ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → ((hP0 * hP1))(h0 ∪ h1)

• Proof step 60:

  h1 ++ r = h0 ∪ h3 ∪ h4, r ≠ null, !(me, hO2, hP)(h3), !(me, hO2, r =>_)(h0), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ ((!(me, hO1, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1 ⊦ !(me, hO1, hP)(h3) ∧ hP0(h4) ∧ h3 ⊥ h4

Rule argument

Additional information

Used terms: h4, h3, hP0, !(me, hO1, hP)

Proof step 59 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 60 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  h1 ++ r = h0 ∪ h3 ∪ h4, r ≠ null, !(me, hO2, r =>_)(h0), !(me, hO2, hP)(h3), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ !(me, hO1, hP)(h3), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ ((!(me, hO1, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Proof step 61 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 62:

  ⊦ !(id, of, hP)(h) ↔ hP(h) ∧ (∀ r. r ∈ h → of(r) = id)

• Proof step 63:

  h1 ++ r = h0 ∪ h3 ∪ h4, r ≠ null, !(me, hO2, hP)(h3), !(me, hO2, r =>_)(h0), r =>_(h0), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ ((!(me, hO1, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1, ¬ hP(h3) ∨ (∃ r. ¬(r ∈ h3 → hO1(r) = me)) ⊦

Rule argument

Additional information

Used terms: h3, hP, hO1, me

Proof step 62 from proof alloc-p (previous step) (back to tree)

Lemma owned

Proof step 63 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  h1 ++ r = h0 ∪ h3 ∪ h4, hO1(r0) ≠ me, r ≠ null, !(me, hO2, hP)(h3), !(me, hO2, r =>_)(h0), r =>_(h0), hP(h3), hP0(h4), rely(me, hO1(r; me), h1 ++ r, hO2, h2), r0 ∈ h3, h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ ((!(me, hO1, hP) * hP0))(h3 ∪ h4), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used simplifier rules: owned-P: ⊦ !(me, hO, hP)(h) ∧ ¬ hP(h) → false;

Proof step 64 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 65:

  ⊦ rely(me, of1, h1, of2, h2) ↔ (∀ r. (of1(r) = me ↔ of2(r) = me) ∧ (of1(r) = me → (r ∈ h1 ↔ r ∈ h2) ∧ (r ∈ h1 → h1[r] = h2[r])))

• Proof step 66:

  h1 ++ r = h0 ∪ h3 ∪ h4, hO1(r0) ≠ me, r ≠ null, !(me, hO2, r =>_)(h0), !(me, hO2, hP)(h3), r =>_(h0), hP(h3), hP0(h4), r0 ∈ h3, h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(me, hO1, hP) * hP0))(h3 ∪ h4), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1, ∀ r0. (hO1(r; me)(r0) = me ↔ hO2(r0) = me) ∧ (hO1(r; me)(r0) = me → (r0 ∈ h1 ++ r ↔ r0 ∈ h2) ∧ (r0 ∈ h1 ++ r → (h1 ++ r)[r0] = h2[r0])) ⊦

Rule argument

Additional information

Used terms: hO2, hO1(r; me), me, h1 ++ r, h2

Proof step 65 from proof alloc-p (previous step) (back to tree)

Lemma rely

Proof step 66 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  h1 ++ r = h0 ∪ h3 ∪ h4, hO1(r0) ≠ me, r ≠ null, !(me, hO2, hP)(h3), !(me, hO2, r =>_)(h0), r =>_(h0), hP(h3), hP0(h4), r0 ∈ h3, h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, ¬ ((!(me, hO1, hP) * hP0))(h3 ∪ h4), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1, ∀ r1. ((r = r1 ⊃ me;hO1(r1)) = me ↔ hO2(r1) = me) ∧ ((r = r1 ⊃ me;hO1(r1)) = me → (r1 = r ∨ r1 ∈ h1 ↔ r1 ∈ h2) ∧ (r1 = r ∨ r1 ∈ h1 → (h1 ++ r)[r1] = h2[r1])) ⊦

Rule argument

Additional information

Used simplifier rules: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s)

Proof step 67 from proof alloc-p (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 68:

  h1 ++ r = h0 ∪ h3 ∪ h4, (r = r0 ⊃ me;hO1(r0)) = me ↔ hO2(r0) = me, hO1(r0) ≠ me, r ≠ null, !(me, hO2, r =>_)(h0), !(me, hO2, hP)(h3), r =>_(h0), hP(h3), hP0(h4), r0 ∈ h3, h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(me, hO1, hP) * hP0))(h3 ∪ h4), ¬ ((!(me, hO1, hP) * hP0))(h1), ¬ r ∈ h1, (r = r0 ⊃ me;hO1(r0)) = me → (r0 = r ∨ r0 ∈ h1 ↔ r0 ∈ h2) ∧ (r0 = r ∨ r0 ∈ h1 → (h1 ++ r)[r0] = h2[r0]), ∀ r1. ((r = r1 ⊃ me;hO1(r1)) = me ↔ hO2(r1) = me) ∧ ((r = r1 ⊃ me;hO1(r1)) = me → (r1 = r ∨ r1 ∈ h1 ↔ r1 ∈ h2) ∧ (r1 = r ∨ r1 ∈ h1 → (h1 ++ r)[r1] = h2[r1])) ⊦

Rule argument

Additional information

Used terms: r0

Proof step 68 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  h1 ++ r = h0 ∪ h3 ∪ h4, (h1 ++ r)[r] = h2[r], hO1(r) ≠ hO2(r), !(hO2(r), hO2, r =>_)(h0), !(hO2(r), hO2, hP)(h3), r =>_(h0), hP(h3), hP0(h4), r ∈ h2, r ∈ h3, h3 ⊥ h4, h0 ⊥ h3, h0 ⊥ h4, ¬ ((!(hO2(r), hO1, hP) * hP0))(h1), ¬ ((!(hO2(r), hO1, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1, ∀ r1. ((r = r1 ⊃ hO2(r1);hO1(r1)) = hO2(r) ↔ hO2(r1) = hO2(r)) ∧ ((r = r1 ⊃ hO2(r1);hO1(r1)) = hO2(r) → (r1 = r ∨ r1 ∈ h1 ↔ r1 ∈ h2) ∧ (r1 ∈ h1 → (h1 ++ r)[r1] = h2[r1])) ⊦

Rule argument

Additional information

Used simplifier rules: owned-r: ⊦ !(me, hO, hP)(h) ∧ hO(r) ≠ me → ¬ r ∈ h; ⊦ r ∈ h → r ≠ null; (s)

Proof step 69 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 70:

  ⊦ h0 ⊥ h1 ↔ (∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h1)

• Proof step 71:

  h1 ++ r = h0 ∪ h3 ∪ h4, (h1 ++ r)[r] = h2[r], hO1(r) ≠ hO2(r), !(hO2(r), hO2, hP)(h3), !(hO2(r), hO2, r =>_)(h0), r =>_(h0), hP(h3), hP0(h4), r ∈ h3, r ∈ h2, h0 ⊥ h4, h3 ⊥ h4, ¬ ((!(hO2(r), hO1, hP) * hP0))(h1), ¬ ((!(hO2(r), hO1, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1, ∀ r1. ((r = r1 ⊃ hO2(r1);hO1(r1)) = hO2(r) ↔ hO2(r1) = hO2(r)) ∧ ((r = r1 ⊃ hO2(r1);hO1(r1)) = hO2(r) → (r1 = r ∨ r1 ∈ h1 ↔ r1 ∈ h2) ∧ (r1 ∈ h1 → (h1 ++ r)[r1] = h2[r1])), ∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h3 ⊦

Rule argument

Additional information

Used terms: h3, h0

Proof step 70 from proof alloc-p (previous step) (back to tree)

A spec-lemma

Proof step 71 from proof alloc-p (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 72:

  h1 ++ r = h0 ∪ h3 ∪ h4, (h1 ++ r)[r] = h2[r], hO1(r) ≠ hO2(r), !(hO2(r), hO2, r =>_)(h0), !(hO2(r), hO2, hP)(h3), r =>_(h0), hP(h3), hP0(h4), r ∈ h2, r ∈ h3, h3 ⊥ h4, h0 ⊥ h4, ¬ ((!(hO2(r), hO1, hP) * hP0))(h1), ¬ ((!(hO2(r), hO1, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1, ∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h3, ∀ r1. ((r = r1 ⊃ hO2(r1);hO1(r1)) = hO2(r) ↔ hO2(r1) = hO2(r)) ∧ ((r = r1 ⊃ hO2(r1);hO1(r1)) = hO2(r) → (r1 = r ∨ r1 ∈ h1 ↔ r1 ∈ h2) ∧ (r1 ∈ h1 → (h1 ++ r)[r1] = h2[r1])), ¬ r ∈ h0 ∨ ¬ r ∈ h3 ⊦

Rule argument

Additional information

Used terms: r

Proof step 72 from proof alloc-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 73:

  h1 ++ r = h0 ∪ h3 ∪ h4, (h1 ++ r)[r] = h2[r], hO1(r) ≠ hO2(r), !(hO2(r), hO2, hP)(h3), !(hO2(r), hO2, r =>_)(h0), r =>_(h0), hP(h3), hP0(h4), r ∈ h3, r ∈ h2, h0 ⊥ h4, h3 ⊥ h4, ¬ ((!(hO2(r), hO1, hP) * hP0))(h1), ¬ ((!(hO2(r), hO1, hP) * hP0))(h3 ∪ h4), ¬ r ∈ h1, ¬ r ∈ h0, ∀ r1. ((r = r1 ⊃ hO2(r1);hO1(r1)) = hO2(r) ↔ hO2(r1) = hO2(r)) ∧ ((r = r1 ⊃ hO2(r1);hO1(r1)) = hO2(r) → (r1 = r ∨ r1 ∈ h1 ↔ r1 ∈ h2) ∧ (r1 ∈ h1 → (h1 ++ r)[r1] = h2[r1])), ∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h3 ⊦

Rule argument

Additional information

Proof step 73 from proof alloc-p (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 74:

  ⊦ r =>_ = _∃(λ o. r => o)

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ oP)(h) ↔ (∃ o. oP(o)(h)); (s) ⊦ ((r => o))(h) → r ∈ h; (s) Used terms: r

Proof step 74 from proof alloc-p (previous step) (back to tree)

A spec-lemma