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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(((!(me, hO2, r => o0 * hP) * hP0))(h1) ↔ ((!(me, hO2, r => o1 * hP) * hP0))(h1[r, o1]) ∧ h1[r] = o0 ∧ r ∈ h1), rely(me, hO1, h1[r, o1], hO2, h2) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(((!(me, hO2, r => o0 * hP) * hP0))(h1) ↔ ((!(me, hO2, r => o1 * hP) * hP0))(h1[r, o1]) ∧ h1[r] = o0 ∧ r ∈ h1), rely(me, hO1, h1[r, o1], hO2, h2) ⊦

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  ((!(me, hO2, r => o0 * hP) * hP0))(h1), rely(me, hO1, h1[r, o1], hO2, h2) ⊦ ((!(me, hO2, r => o1 * hP) * hP0))(h1[r, o1]) ∧ h1[r] = o0 ∧ r ∈ h1

• Proof step 26:

  h1[r] = o0, ((!(me, hO2, r => o1 * hP) * hP0))(h1[r, o1]), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, ¬ ((!(me, hO2, r => o0 * hP) * hP0))(h1) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  rely(me, hO1, h1[r, o1], hO2, h2), ∃ h0, h2. h0 ⊥ h2 ∧ h1 = h0 ∪ h2 ∧ !(me, hO2, r => o0 * hP)(h0) ∧ hP0(h2) ⊦ ((!(me, hO2, r => o1 * hP) * hP0))(h1[r, o1]) ∧ h1[r] = o0 ∧ r ∈ h1

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  !(me, hO2, r => o0 * hP)(h0), hP0(h), rely(me, hO1, (h0 ∪ h)[r, o1], hO2, h2), h0 ⊥ h ⊦ ((!(me, hO2, r => o1 * hP) * hP0))((h0 ∪ h)[r, o1]) ∧ (r ∈ h0 ⊃ h0[r];h[r]) = o0 ∧ (r ∈ h0 ∨ r ∈ h)

Rule argument

Additional information

Used simplifier rules: r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)[r] = (r ∈ h0 ⊃ h0[r];h1[r]); (s) ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, (h0 ∪ h)[r, o1], hO2, h2), h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me ⊦ ((!(me, hO2, r => o1 * hP) * hP0))((h0 ∪ h)[r, o1]) ∧ (r ∈ h0 ⊃ h0[r];h[r]) = o0 ∧ (r ∈ h0 ∨ r ∈ h)

Rule argument

Additional information

Used terms: h0, r => o0 * hP, hO2, me

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

Lemma owned

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, (h0 ∪ h)[r, o1], hO2, h2), h0 ⊥ h, ¬ ((!(me, hO2, r => o1 * hP) * hP0))((h0 ∪ h)[r, o1]), ∀ r. r ∈ h0 → hO2(r) = me ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ((r => o * hP))(h) → r ∈ h; (s) ⊦ ((r => o0 * hP))(h) → (h[r] = o1 ↔ o0 = o1); (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ r ∈ h0 ∧ h0 ⊥ h1 → (h0 ∪ h1)[r, o] = h0[r, o] ∪ h1

• Proof step 12:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, h0[r, o1] ∪ h, hO2, h2), r ∈ h0, h0 ⊥ h, ¬ ((!(me, hO2, r => o1 * hP) * hP0))(h0[r, o1] ∪ h), ∀ r. r ∈ h0 → hO2(r) = me ⊦

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 => o * hP))(h) → r ∈ h; (s) Used terms: o1, r, h, h0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, h0[r, o1] ∪ h, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO2, r => o1 * hP) * hP0))(h0[r, o1] ∪ h), ∀ r. r ∈ h0 → hO2(r) = me ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, h0[r, o1] ∪ h, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO2, r => o1 * hP) * hP0))(h0[r, o1] ∪ h), ∀ r. r ∈ h0 → hO2(r) = me ⊦ !(me, hO2, r => o1 * hP)(h0[r, o1]) ∧ hP0(h) ∧ h0[r, o1] ⊥ h

Rule argument

Additional information

Used terms: h, h0[r, o1], hP0, !(me, hO2, r => o1 * hP)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, h0[r, o1] ∪ h, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO2, r => o1 * hP) * hP0))(h0[r, o1] ∪ h), ∀ r. r ∈ h0 → hO2(r) = me ⊦ !(me, hO2, r => o1 * hP)(h0[r, o1]) ∧ h0[r, o1] ⊥ h

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, h0[r, o1] ∪ h, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO2, r => o1 * hP) * hP0))(h0[r, o1] ∪ h), ∀ r. r ∈ h0 → hO2(r) = me ⊦ !(me, hO2, r => o1 * hP)(h0[r, o1]) ∧ (∀ r0. ¬ r0 ∈ h0[r, o1] ∨ ¬ r0 ∈ h)

Rule argument

Additional information

Used terms: h, h0[r, o1]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, h0[r, o1] ∪ h, hO2, h2), h0 ⊥ h, ¬ !(me, hO2, r => o1 * hP)(h0[r, o1]), ¬ ((!(me, hO2, r => o1 * hP) * hP0))(h0[r, o1] ∪ h), ∀ r. r ∈ h0 → hO2(r) = me ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); (s) ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, h0[r, o1] ∪ h, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO2, r => o1 * hP) * hP0))(h0[r, o1] ∪ h), ∀ r. r ∈ h0 → hO2(r) = me, ¬ ((r => o1 * hP))(h0[r, o1]) ∨ (∃ r0. ¬(r0 ∈ h0[r, o1] → hO2(r0) = me)) ⊦

Rule argument

Additional information

Used terms: h0[r, o1], r => o1 * hP, hO2, me

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

Lemma owned

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, h0[r, o1] ∪ h, hO2, h2), h0 ⊥ h, ¬ ((!(me, hO2, r => o1 * hP) * hP0))(h0[r, o1] ∪ h), ∀ r. r ∈ h0 → hO2(r) = me, ¬ ((r => o1 * hP))(h0[r, o1]) ∨ ¬(r0 ∈ h0 → hO2(r0) = me) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  r ∈ h ⊦ ((r => o0 * hP))(h[r, o1]) ↔ o0 = o1 ∧ ((r =>_ * hP))(h)

• Proof step 24:

  ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, h0[r, o1] ∪ h, hO2, h2), r ∈ h0, h0 ⊥ h, ¬ ((!(me, hO2, r => o1 * hP) * hP0))(h0[r, o1] ∪ h), ∀ r. r ∈ h0 → hO2(r) = me, ¬(o1 = o1 ∧ ((r =>_ * hP))(h0)) ∨ ¬(r0 ∈ h0 → hO2(r0) = me) ⊦

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 => o * hP))(h) → r ∈ h; (s) Used terms: r, h0, hP, o1, o1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  hO2(r0) ≠ me, ((r => o0 * hP))(h0), hP0(h), rely(me, hO1, h0[r, o1] ∪ h, hO2, h2), r0 ∈ h0, h0 ⊥ h, ¬ ((!(me, hO2, r => o1 * hP) * hP0))(h0[r, o1] ∪ h), ∀ r. r ∈ h0 → hO2(r) = me ⊦

Rule argument

Additional information

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

Proof step 25 from proof write-known-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 26 from proof write-known-p (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  ((!(me, hO2, r => o1 * hP) * hP0))(h1[r, o1]), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, ¬ ((!(me, hO2, r => h1[r] * hP) * hP0))(h1) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

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

• Proof step 29:

  rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, ¬ ((!(me, hO2, r => h1[r] * hP) * hP0))(h1), ∃ h0, h2. h0 ⊥ h2 ∧ h1[r, o1] = h0 ∪ h2 ∧ !(me, hO2, r => o1 * hP)(h0) ∧ hP0(h2) ⊦

Rule argument

Additional information

Used terms: h1[r, o1], hP0, !(me, hO2, r => o1 * hP)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  h1[r, o1] = h0 ∪ h, !(me, hO2, r => o1 * hP)(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ¬ ((!(me, hO2, r => h1[r] * hP) * hP0))(h1) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

• Proof step 32:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ¬ ((!(me, hO2, r => h1[r] * hP) * hP0))(h1), ∀ r. r ∈ h0 → hO2(r) = me ⊦

Rule argument

Additional information

Used terms: h0, r => o1 * hP, hO2, me

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

Lemma owned

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ¬ ((!(me, hO2, r => h1[r] * hP) * hP0))(h1), ∀ r. r ∈ h0 → hO2(r) = me ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me, ∀ h0, h2. ¬(h0 ⊥ h2 ∧ h1 = h0 ∪ h2 ∧ !(me, hO2, r => h1[r] * hP)(h0) ∧ hP0(h2)) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me, ∀ h3, h4. ¬ h3 ⊥ h4 ∨ h1 ≠ h3 ∪ h4 ∨ ¬ !(me, hO2, r => (h3 ∪ h4)[r] * hP)(h3) ∨ ¬ hP0(h4) ⊦

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 37:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me, ¬ h0[r, h1[r]] ⊥ h ∨ h1 ≠ h0[r, h1[r]] ∪ h ∨ ¬ !(me, hO2, r => (h0[r, h1[r]] ∪ h)[r] * hP)(h0[r, h1[r]]) ∨ ¬ hP0(h) ⊦

Rule argument

Additional information

Used terms: h0[r, h1[r]], h

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me, ¬ h0[r, h1[r]] ⊥ h ∨ h1 ≠ h0[r, h1[r]] ∪ h ∨ ¬ !(me, hO2, r => h1[r] * hP)(h0[r, h1[r]]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ((r => o * hP))(h) → r ∈ h; (s) ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]); (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s) r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)[r] = (r ∈ h0 ⊃ h0[r];h1[r]); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

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

• Proof step 40:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me, ¬(∀ r0. ¬ r0 ∈ h0[r, h1[r]] ∨ ¬ r0 ∈ h) ∨ h1 ≠ h0[r, h1[r]] ∪ h ∨ ¬ !(me, hO2, r => h1[r] * hP)(h0[r, h1[r]]) ⊦

Rule argument

Additional information

Used terms: h, h0[r, h1[r]]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me, h1 ≠ h0[r, h1[r]] ∪ h ∨ ¬ !(me, hO2, r => h1[r] * hP)(h0[r, h1[r]]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); (s) ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 42:

  h1[r, o1] = h0 ∪ h, h1 ≠ h0[r, h1[r]] ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me ⊦

• Proof step 48:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ¬ !(me, hO2, r => h1[r] * hP)(h0[r, h1[r]]), ∀ r. r ∈ h0 → hO2(r) = me ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ r ∈ h0 ∧ h0 ⊥ h1 → (h0 ∪ h1)[r, o] = h0[r, o] ∪ h1

• Proof step 44:

  h1[r, o1] = h0 ∪ h, h1 ≠ (h0 ∪ h)[r, h1[r]], ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, r ∈ h0, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me ⊦

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 => o * hP))(h) → r ∈ h; (s) Used terms: h, h1[r], r, h0

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

A spec-lemma

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

User applied rule subst equation

And obtained the following new goals

• Proof step 45:

  h1[r, o1] = h0 ∪ h, h1 ≠ h1[r, o1][r, h1[r]], ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h0, r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  h1[r, o1] = h0 ∪ h, h1 ≠ h1[r, h1[r]], ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ((r => o * hP))(h) → r ∈ h; (s) sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ h[r, o0][r, o1] = h[r, o1]; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

  r ∈ h ⊦ h[r] = o → h[r, o] = h

Rule argument

Additional information

Used terms: h1[r], r, h1

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me, ¬ ((r => h1[r] * hP))(h0[r, h1[r]]) ∨ (∃ r0. ¬(r0 ∈ h0[r, h1[r]] → hO2(r0) = me)) ⊦

Rule argument

Additional information

Used terms: h0[r, h1[r]], r => h1[r] * hP, hO2, me

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

Lemma owned

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me, ¬ ((r => h1[r] * hP))(h0[r, h1[r]]) ∨ ¬(r0 ∈ h0 → hO2(r0) = me) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  r ∈ h ⊦ ((r => o0 * hP))(h[r, o1]) ↔ o0 = o1 ∧ ((r =>_ * hP))(h)

• Proof step 53:

  h1[r, o1] = h0 ∪ h, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, r ∈ h0, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me, ¬(h1[r] = h1[r] ∧ ((r =>_ * hP))(h0)) ∨ ¬(r0 ∈ h0 → hO2(r0) = me) ⊦

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 => o * hP))(h) → r ∈ h; (s) Used terms: r, h0, hP, h1[r], h1[r]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  h1[r, o1] = h0 ∪ h, hO2(r0) ≠ me, ((r => o1 * hP))(h0), hP0(h), rely(me, hO1, h1[r, o1], hO2, h2), r ∈ h1, r0 ∈ h0, h0 ⊥ h, ∀ r. r ∈ h0 → hO2(r) = me ⊦

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0