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 23:

  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)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ a ∈ st ↔ (∃ d, st0. st = st0(a := d) ∧ ¬ a ∈ st0)

• Proof step 10:

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

Rule argument

Additional information

Used terms: r, h0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: ⊦ a = b → st(a := d)(b := d0) = st(b := d0); (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used terms: h, ∅(r := o0)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  hP(h(r := o)), ¬ r ∈ h, ¬ (r => o -* hP)(h) ∨ ¬ r.=>_(∅(r := o0)) ⊦

Rule argument

Additional information

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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  hP(h(r := o)), ¬ (r => o -* hP)(h), ¬ r ∈ h ⊦

• Proof step 19:

  hP(h(r := o)), ¬ r.=>_(∅(r := o0)), ¬ r ∈ h ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  hP(h(r := o)), ¬ r ∈ h, ∃ h1. ¬(h1 ⊥ h ∧ (r => o)(h1) → hP(h1 ∪ h)) ⊦

Rule argument

Additional information

Used terms: r => o, hP, h

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  h1 ⊥ h, hP(h(r := o)), (r => o)(h1), ¬ hP(h1 ∪ h), ¬ r ∈ h ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ (r => o)(h) ↔ h = ∅(r := o)

Rule argument

Additional information

Used simplifier rules: ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; (s) ⊦ ¬ r ∈ h → ∅(r := o) ∪ h = h(r := o); (s) Used terms: r, o, h1

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  hP(h(r := o)), ¬ (_∃(λ o. r => o))(∅(r := o0)), ¬ r ∈ h ⊦

Rule argument

Additional information

Used terms: r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  hP(h(r := o)), ¬ r ∈ h ⊦ ∃ c. (r => c)(∅(r := o0))

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ cP)(h) ↔ (∃ c. cP(c)(h)); (s)

Proof step 22 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 := o); (ss) Used terms: o0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  ((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 map-sep sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification map-sep

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  ¬ 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 25 from proof assign-wp (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

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

• Proof step 29:

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

Rule argument

Additional information

Used terms: r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

Used simplifier rules: ⊦ (_∃ cP)(h) ↔ (∃ c. cP(c)(h)); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ (r => o)(h) ↔ h = ∅(r := o)

• Proof step 32:

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

Rule argument

Additional information

Used terms: r, o0, h2

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

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

Rule argument

Additional information

Used terms: r => o, hP, h1

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

A spec-lemma

Proof step 35 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 := o) ⊥ h ↔ ¬ r ∈ h; (s) ⊦ ¬ r ∈ h → ∅(r := o) ∪ h = h(r := o); (s) ⊦ (r => o)(h) ↔ h = ∅(r := o); (ss) Used terms: ∅(r := o)