Proof step 1 from proof assign-wp (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(hP(h1) ↔ ((r => o -* hP) * r.=>_)(h0)), h1 ≡ h0(r := o), r ∈ h0 ⊦

Rule argument

Additional information

Proof step 2 from proof assign-wp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(hP(h0(r := o)) ↔ ((r => o -* hP) * r.=>_)(h0)), r ∈ h0 ⊦

Rule argument

Additional information

Used simplifier rules: eq: ⊦ h0 ≡ h1 ↔ h0 = h1;

Proof step 3 from proof assign-wp (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  hP(h0(r := o)), r ∈ h0, ¬ ((r => o -* hP) * r.=>_)(h0) ⊦

• Proof step 22:

  r ∈ h0, ((r => o -* hP) * r.=>_)(h0), ¬ hP(h0(r := o)) ⊦

Rule argument

Additional information

Proof step 4 from proof assign-wp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  hP(h0(r := o)), r ∈ h0, ¬ ((r => o -* hP) * r.=>_)(h0) ⊦

Rule argument

Additional information

Proof step 5 from proof assign-wp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  hP(h0(r := o)), r ∈ h0, ∀ h1, h2. ¬(h1 ⊥ h2 ∧ h0 = h1 ∪ h2 ∧ (r => o -* hP)(h1) ∧ r.=>_(h2)) ⊦

Rule argument

Additional information

Used terms: h0, r.=>_, r => o -* hP

Proof step 6 from proof assign-wp (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof assign-wp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ r ≠ null → (r ∈ h ↔ (∃ h0, o. h = (h0 ++ r)(r := o) ∧ ¬ r ∈ h0))

• Proof step 9:

  r ≠ null, hP(h0(r := o)), ∀ h1, h2. ¬(h1 ⊥ h2 ∧ h0 = h1 ∪ h2 ∧ (r => o -* hP)(h1) ∧ r.=>_(h2)), ∃ h1, o. h0 = (h1 ++ r)(r := o) ∧ ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ null ∈ h; (s) Used terms: h0, r

Proof step 8 from proof assign-wp (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof assign-wp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  r ≠ null, hP((h1 ++ r)(r := o)), ¬ r ∈ h1, ∀ h, h2. ¬ h ⊥ h2 ∨ (h1 ++ r)(r := o0) ≠ h ∪ h2 ∨ ¬ (r => o -* hP)(h) ∨ ¬ r.=>_(h2) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h(r := o0)(r := o1) = h(r := o1); (s)

Proof step 10 from proof assign-wp (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  r ≠ null, hP((h1 ++ r)(r := o)), ¬ r ∈ h1, ¬ h1 ⊥ (∅ ++ r)(r := o0) ∨ (h1 ++ r)(r := o0) ≠ h1 ∪ (∅ ++ r)(r := o0) ∨ ¬ (r => o -* hP)(h1) ∨ ¬ r.=>_((∅ ++ r)(r := o0)) ⊦

Rule argument

Additional information

Used terms: h1, (∅ ++ r)(r := o0)

Proof step 11 from proof assign-wp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  r ≠ null, hP((h1 ++ r)(r := o)), ¬ r ∈ h1, ¬ (r => o -* hP)(h1) ∨ ¬ r.=>_((∅ ++ r)(r := o0)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ≠ null ∧ ¬ r ∈ h → h ∪ (∅ ++ r)(r := o) = (h ++ r)(r := o); (s) ⊦ h ⊥ ∅; (s) r ≠ null, ¬ r ∈ h1 ⊦ h0 ⊥ (h1 ++ r)(r := o) ↔ h0 ⊥ h1 ∧ ¬ r ∈ h0; (s) ⊦ ¬ r ∈ ∅; (s)

Proof step 12 from proof assign-wp (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  r ≠ null, hP((h1 ++ r)(r := o)), ¬ (r => o -* hP)(h1), ¬ r ∈ h1 ⊦

• Proof step 18:

  r ≠ null, hP((h1 ++ r)(r := o)), ¬ r.=>_((∅ ++ r)(r := o0)), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Proof step 13 from proof assign-wp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ (hP0 -* hP1)(h) ↔ (∀ h1. h1 ⊥ h ∧ hP0(h1) → hP1(h1 ∪ h))

• Proof step 15:

  r ≠ null, hP((h1 ++ r)(r := o)), ¬ r ∈ h1, ∃ h0. ¬(h0 ⊥ h1 ∧ (r => o)(h0) → hP(h0 ∪ h1)) ⊦

Rule argument

Additional information

Used terms: h1, hP, r => o

Proof step 14 from proof assign-wp (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof assign-wp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  r ≠ null, h0 ⊥ h1, hP((h1 ++ r)(r := o)), (r => o)(h0), ¬ hP(h0 ∪ h1), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Proof step 16 from proof assign-wp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ (r => o)(h) ↔ h = (∅ ++ r)(r := o) ∧ r ≠ null

Rule argument

Additional information

Used simplifier rules: r ≠ null ⊦ (∅ ++ r)(r := o) ⊥ h ↔ ¬ r ∈ h; (s) ⊦ r ≠ null ∧ ¬ r ∈ h → (∅ ++ r)(r := o) ∪ h = (h ++ r)(r := o); (s) Used terms: h0, o, r

Proof step 17 from proof assign-wp (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof assign-wp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

  r ≠ null, hP((h1 ++ r)(r := o)), ¬ (_∃(λ o. r => o))((∅ ++ r)(r := o0)), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used terms: r

Proof step 19 from proof assign-wp (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof assign-wp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  r ≠ null, hP((h1 ++ r)(r := o)), ¬ r ∈ h1 ⊦ ∃ o. (r => o)((∅ ++ r)(r := o0))

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s)

Proof step 21 from proof assign-wp (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (r => o)(h) ↔ h = (∅ ++ r)(r := o) ∧ r ≠ null; (ss) Used terms: o0

Proof step 22 from proof assign-wp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  ((r => o -* hP) * r.=>_)(h0), ¬ hP(h0(r := o)) ⊦

Rule argument

Additional information

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

Proof step 23 from proof assign-wp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

  ¬ hP(h0(r := o)), ∃ h1, h2. h1 ⊥ h2 ∧ h0 = h1 ∪ h2 ∧ (r => o -* hP)(h1) ∧ r.=>_(h2) ⊦

Rule argument

Additional information

Used terms: h0, r.=>_, r => o -* hP

Proof step 24 from proof assign-wp (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof assign-wp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  h1 ⊥ h2, (r => o -* hP)(h1), r.=>_(h2), ¬ hP((h1 ∪ h2)(r := o)) ⊦

Rule argument

Additional information

Proof step 26 from proof assign-wp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

  (_∃(λ o. r => o))(h2), h1 ⊥ h2, (r => o -* hP)(h1), ¬ hP((h1 ∪ h2)(r := o)) ⊦

Rule argument

Additional information

Used terms: r

Proof step 27 from proof assign-wp (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof assign-wp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  h1 ⊥ h2, (r => o -* hP)(h1), (r => o0)(h2), ¬ hP((h1 ∪ h2)(r := o)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ bP)(h) ↔ (∃ b. bP(b)(h)); (s)

Proof step 29 from proof assign-wp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ (r => o)(h) ↔ h = (∅ ++ r)(r := o) ∧ r ≠ null

• Proof step 31:

  h2 = (∅ ++ r)(r := o0), r ≠ null, h1 ⊥ h2, (r => o -* hP)(h1), ¬ hP((h1 ∪ h2)(r := o)) ⊦

Rule argument

Additional information

Used terms: h2, o0, r

Proof step 30 from proof assign-wp (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof assign-wp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  r ≠ null, (r => o -* hP)(h1), ¬ hP((h1 ++ r)(r := o)), ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ h(r := o0)(r := o1) = h(r := o1); (s) ⊦ r ≠ null ∧ ¬ r ∈ h → h ∪ (∅ ++ r)(r := o) = (h ++ r)(r := o); (s) ⊦ h ⊥ ∅; (s) r ≠ null, ¬ r ∈ h1 ⊦ h0 ⊥ (h1 ++ r)(r := o) ↔ h0 ⊥ h1 ∧ ¬ r ∈ h0; (s) ⊦ ¬ r ∈ ∅; (s)

Proof step 32 from proof assign-wp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ (hP0 -* hP1)(h) ↔ (∀ h1. h1 ⊥ h ∧ hP0(h1) → hP1(h1 ∪ h))

• Proof step 34:

  r ≠ null, ¬ hP((h1 ++ r)(r := o)), ¬ r ∈ h1, ∀ h0. h0 ⊥ h1 ∧ (r => o)(h0) → hP(h0 ∪ h1) ⊦

Rule argument

Additional information

Used terms: h1, hP, r => o

Proof step 33 from proof assign-wp (previous step) (back to tree)

A spec-lemma

Proof step 34 from proof assign-wp (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: r ≠ null ⊦ (∅ ++ r)(r := o) ⊥ h ↔ ¬ r ∈ h; (s) ⊦ r ≠ null ∧ ¬ r ∈ h → (∅ ++ r)(r := o) ∪ h = (h ++ r)(r := o); (s) ⊦ (r => o)(h) ↔ h = (∅ ++ r)(r := o) ∧ r ≠ null; (ss) Used terms: (∅ ++ r)(r := o)