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, (!(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 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), h0 ⊥ h, r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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, h0 ⊥ h, r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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), h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP0(h4), r.=>_(h0), 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: 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), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ ((!(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), h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h0 ∪ h3 ∪ h4, hO2, h2), ¬ ((!(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), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h0 ∪ h3 ∪ h4, hO2, h2), ¬ (!(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), h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h0 ∪ h3 ∪ h4, hO2, h2), ¬ (!(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), h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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), h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(me, hO2, r.=>_ * hP) * hP0)(h1 ++ r), ¬ (!(me, hO2, hP) * hP0)(h3 ∪ h4), ¬ !(me, hO2, hP)(h3), ¬ 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), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP0(h4), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(me, hO2, r.=>_ * hP) * hP0)(h1 ++ r), ¬ (!(me, hO2, hP) * hP0)(h3 ∪ h4), ¬ !(me, hO2, hP)(h3), ¬ 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, h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(me, hO2, r.=>_ * hP) * hP0)(h1 ++ r), ¬ (!(me, hO2, hP) * hP0)(h3 ∪ h4), ¬ !(me, hO2, hP)(h3), ¬ 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, h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP(h3), hP0(h4), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(me, hO2, r.=>_ * hP) * hP0)(h1 ++ r), ¬ (!(me, hO2, hP) * hP0)(h3 ∪ h4), ¬ !(me, hO2, hP)(h3), ¬ 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, h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(me, hO2, r.=>_ * hP) * hP0)(h1 ++ r), ¬ (!(me, hO2, hP) * hP0)(h3 ∪ h4), ¬ r ∈ h1, ¬ hP(h3) ∨ (∃ r. ¬(r ∈ h3 → hO2(r) = me)), ∀ r. r ∈ h3 → hO1(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, h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP(h3), hP0(h4), r0 ∈ h3, rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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, h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), r0 ∈ h3, rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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, h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), r0 ∈ h3, rely(hO1(r0), hO1(r := hO1(r0)), h1 ++ r, hO2, h2), ¬ (!(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, h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP(h3), hP0(h4), r0 ∈ h3, ¬ (!(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: h2, hO1(r := hO1(r0)), h1 ++ r, hO1(r0), hO2

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, h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), r0 ∈ h3, ¬ (!(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), h0 ⊥ h, rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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, hP) * hP0)(h), !(me, hO2, r.=>_)(h0), h0 ⊥ h, rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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), h0 ⊥ h, rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(me, hO1, hP) * hP0)(h1), ¬ (r.=>_ * !(me, hO1, hP) * hP0)(h1 ++ r), ¬ 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, hP) * hP0)(h), !(me, hO2, r.=>_)(h0), h0 ⊥ h, rely(me, hO1(r := me), h0 ∪ h, hO2, h2), ¬ (!(me, hO1, hP) * hP0)(h1), ¬ (r.=>_ * !(me, hO1, hP) * hP0)(h0 ∪ h), ¬ 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), h0 ⊥ h, rely(me, hO1(r := me), h0 ∪ h, hO2, h2), ¬ (!(me, hO1, hP) * hP0)(h1), ¬ (r.=>_ * !(me, hO1, hP) * hP0)(h0 ∪ h), ¬ 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), h0 ⊥ h, r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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), h0 ⊥ h, r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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), h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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), h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(me, hO1, hP) * hP0)(h1), ¬ (!(me, hO1, hP) * hP0)(h3 ∪ h4), ¬ !(me, hO1, hP)(h3), ¬ 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), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP0(h4), r.=>_(h0), rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP(h3), hP0(h4), r.=>_(h0), r0 ∈ h3, rely(me, hO1(r := me), h1 ++ r, hO2, h2), ¬ (!(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), h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), r.=>_(h0), r0 ∈ h3, ¬ (!(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: h2, hO1(r := me), h1 ++ r, me, hO2

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), h0 ⊥ h4, h0 ⊥ h3, h3 ⊥ h4, hP(h3), hP0(h4), r.=>_(h0), r0 ∈ h3, ¬ (!(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:

  (r = r0 ⊃ me;hO1(r0)) = me ↔ hO2(r0) = me, h1 ++ r = h0 ∪ h3 ∪ h4, hO1(r0) ≠ me, r ≠ null, !(me, hO2, r.=>_)(h0), !(me, hO2, hP)(h3), h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), r.=>_(h0), r0 ∈ h3, ¬ (!(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)(r) = h2(r), h1 ++ r = h0 ∪ h3 ∪ h4, hO1(r) ≠ hO2(r), !(hO2(r), hO2, r.=>_)(h0), !(hO2(r), hO2, hP)(h3), h0 ⊥ h3, h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), r ∈ h2, r.=>_(h0), r ∈ h3, ¬ (!(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), h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), r ∈ h3, r.=>_(h0), r ∈ h2, ¬ (!(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))) ⊦

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)(r) = h2(r), h1 ++ r = h0 ∪ h3 ∪ h4, hO1(r) ≠ hO2(r), !(hO2(r), hO2, r.=>_)(h0), !(hO2(r), hO2, hP)(h3), h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), r ∈ h2, r.=>_(h0), r ∈ h3, ¬ (!(hO2(r), hO1, hP) * hP0)(h1), ¬ (!(hO2(r), hO1, hP) * hP0)(h3 ∪ h4), ¬ r ∈ h1, ¬ r ∈ h0 ∨ ¬ r ∈ h3, ∀ 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))) ⊦

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), h0 ⊥ h4, h3 ⊥ h4, hP(h3), hP0(h4), r ∈ h3, r.=>_(h0), r ∈ h2, ¬ (!(hO2(r), hO1, hP) * hP0)(h1), ¬ (!(hO2(r), hO1, hP) * hP0)(h3 ∪ h4), ¬ r ∈ h1, ¬ r ∈ h0, ∀ 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))) ⊦

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: ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s) precise(hP1) ⊦ hP1(h1) ∧ h0 ⊥ h1 → ((hP0 * hP1)(h0 ∪ h1) ↔ hP0(h0)); (s) sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep ⊦ (r => o)(h) → r ∈ h; (s) Used terms: r

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

A spec-lemma