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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 31:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ h1 ≡ h0 -- r → ((r.=>_ * hP)(h0) ↔ hP(h1) ∧ r ∈ h0 ∧ r ≠ null ∧ ¬ r ∈ h1)

• Proof step 6:

  r ≠ null, h0 -- r ≡ h0 -- r, hP(h0(r := o1)), r ∈ h0, ¬ (r => o1 -* hP)(h0 -- r) ∨ ¬ r ∈ h0 ∨ r = null ∨ r ∈ h0 -- r ⊦

Rule argument

Additional information

Used simplifier rules: eq: ⊦ h0 ≡ h1 ↔ h0 = h1; sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification map-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification map-sep Used terms: h0, r, r => o1 -* hP, h0 -- r

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

Lemma free-unknown

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  r ≠ null, hP(h0(r := o1)), r ∈ h0, ¬ (r => o1 -* hP)(h0 -- r) ⊦

Rule argument

Additional information

Used simplifier rules: eq: ⊦ h0 ≡ h1 ↔ h0 = h1; ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

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

Rule argument

Additional information

Used terms: r => o1, hP, h0 -- r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

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

User applied rule cut formula

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used formulas: h1 ∪ (h0 -- r) = h0(r := o1)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  h1 = ∅(r := o1), h1 ∪ (h0 -- r) ≠ h0(r := o1), r ≠ null, h1 ⊥ h0 -- r, hP(h0(r := o1)), r ∈ h0, ¬ hP(h1 ∪ (h0 -- r)) ⊦

Rule argument

Additional information

Used terms: r, o1, h1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  r ≠ null, ∅(r := o1) ∪ (h0 -- r) ≠ h0(r := o1), hP(h0(r := o1)), r ∈ h0, ¬ hP(∅(r := o1) ∪ (h0 -- r)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1(a) = st2(a))

• Proof step 16:

  r ≠ null, hP(h0(r := o1)), r ∈ h0, ¬ hP(∅(r := o1) ∪ (h0 -- r)), ∃ a. ¬((a ∈ h0(r := o1) ↔ a ∈ ∅(r := o1) ∪ (h0 -- r)) ∧ h0(r := o1)(a) = (∅(r := o1) ∪ (h0 -- r))(a)) ⊦

Rule argument

Additional information

Used terms: ∅(r := o1) ∪ (h0 -- r), h0(r := o1)

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  r ≠ null, hP(h0(r := o1)), r ∈ h0, ¬ hP(∅(r := o1) ∪ (h0 -- r)) ⊦ (r0 ∈ h0 ↔ r0 ∈ ∅(r := o1) ∪ (h0 -- r)) ∧ h0(r := o1)(r0) = (∅(r := o1) ∪ (h0 -- r))(r0)

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

• Proof step 19:

  r ≠ null, hP(h0(r := o1)), r ∈ h0, ∅(r := o1) ⊥ h0 -- r, ¬ hP(∅(r := o1) ∪ (h0 -- r)) ⊦ (r0 ∈ h0 ↔ r0 ∈ ∅(r := o1) ∨ r0 ∈ h0 -- r) ∧ h0(r := o1)(r0) = (∅(r := o1) ∪ (h0 -- r))(r0)

Rule argument

Additional information

Used simplifier rules: ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; (s) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) Used terms: r0, ∅(r := o1), h0 -- r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  h0(r := o1)(r0) ≠ (∅(r := o1) ∪ (h0 -- r))(r0), r ≠ null, hP(h0(r := o1)), r ∈ h0, ¬ hP(∅(r := o1) ∪ (h0 -- r)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) ⊦ ¬ a ∈ ∅; (s) ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; (s) ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ a ≠ b → st(b := d)(a) = st(a)

• Proof step 22:

  h0(r0) ≠ (∅(r := o1) ∪ (h0 -- r))(r0), r ≠ null, r0 ≠ r, hP(h0(r := o1)), r ∈ h0, ¬ hP(∅(r := o1) ∪ (h0 -- r)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a = b → st(b := d)(a) = d; (s) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) ¬ r ∈ h ⊦ (∅(r := o) ∪ h)(r) = o; (s) Used terms: h0, r, o1, r0

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r))

• Proof step 24:

  h0(r0) ≠ (∅(r := o1) ∪ (h0 -- r))(r0), r ≠ null, r0 ≠ r, hP(h0(r := o1)), r ∈ h0, ¬ hP(∅(r := o1) ∪ (h0 -- r)) ⊦ r0 ∈ ∅(r := o1) ∪ (h0 -- r) ∧ ∅(r := o1) ⊥ h0 -- r

Rule argument

Additional information

Used simplifier rules: ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); (s) ⊦ ¬ a ∈ ∅; (s) ⊦ a ≠ b → (st -- b)(a) = st(a); (s) Used terms: ∅(r := o1), h0 -- r, r0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  h0(r0) ≠ (∅(r := o1) ∪ (h0 -- r))(r0), r ≠ null, r0 ≠ r, hP(h0(r := o1)), r ∈ h0, ¬ hP(∅(r := o1) ∪ (h0 -- r)), ¬ r0 ∈ h0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; (s) ⊦ ¬ a ∈ ∅; (s) ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); (s) ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

• Proof step 27:

  r ≠ null, r0 ≠ r, ∅(r0) ≠ (∅(r := o1) ∪ (h0 -- r))(r0), hP(h0(r := o1)), r ∈ h0, ¬ hP(∅(r := o1) ∪ (h0 -- r)), ¬ r0 ∈ h0 ⊦

Rule argument

Additional information

Used terms: h0, r0

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ ¬ a ∈ st → st(a) = ∅(a)

• Proof step 29:

  r ≠ null, r0 ≠ r, ∅(r0) ≠ (∅(r := o1) ∪ (h0 -- r))(r0), hP(h0(r := o1)), r ∈ h0, r0 ∈ ∅(r := o1) ∪ (h0 -- r), ¬ hP(∅(r := o1) ∪ (h0 -- r)), ¬ r0 ∈ h0 ⊦

Rule argument

Additional information

Used terms: ∅(r := o1) ∪ (h0 -- r), r0

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); (s) r ∈ h0 ∪ h1 ⊦ h0 ⊥ h1 → (h0 ∪ h1)(r) = (r ∈ h0 ⊃ h0(r);h1(r)); (s) ⊦ a ≠ b → (st -- b)(a) = st(a); (s) ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; (s) ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); (s) ⊦ ¬ a ∈ ∅; (s) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) Used terms: r0, ∅(r := o1), h0 -- r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  r ≠ null, (r.=>_ * (r => o1 -* hP))(h0), ¬ hP(h0(r := o1)) ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

  ⊦ (r.=>_ * hP)(h) ↔ (r => o1 * hP)(h(r := o1)) ∧ r ∈ h

• Proof step 34:

  r ≠ null, (r => o1 * (r => o1 -* hP))(h0(r := o1)), r ∈ h0, ¬ hP(h0(r := o1)) ⊦

Rule argument

Additional information

Used terms: r, r => o1 -* hP, h0, o1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  r ≠ null, r ∈ h0, (r => o1 * (r => o1 -* hP))(h0(r := o1)), ¬ hP(h0(r := o1)) ⊦

Rule argument

Additional information

Used simplifier rules: sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification map-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification map-sep map-write: r ∈ h ⊦ (r => o0 * hP)(h(r := o1)) → o0 = o1; (forward) from specification refmap-maplet

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 36:

  ⊦ (hP0 * (hP0 -* hP1))(h) → hP1(h)

Rule argument

Additional information

Used terms: r => o1, hP, h0(r := o1)

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

A spec-lemma