Proof step 1 from proof mapex-new (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(hP(h) ↔ (r.=>_ * hP)(h ++ r)), r ≠ null, ¬ r ∈ h ⊦

Rule argument

Additional information

Proof step 2 from proof mapex-new (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  r ≠ null, ¬ r ∈ h ⊦ hP(h) ↔ (∃ b. (r => b * hP)(h ++ r))

Rule argument

Additional information

Used simplifier rules: mapex: ⊦ r.=>_ = _∃(λ o. r => o); sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep ⊦ (_∃ bP * hP)(h) ↔ (∃ b. (bP(b) * hP)(h)); (s)

Proof step 3 from proof mapex-new (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  r ≠ null, hP(h), ¬ r ∈ h ⊦ ∃ b. (r => b * hP)(h ++ r)

• Proof step 9:

  r ≠ null, ¬ hP(h), ¬ r ∈ h, ∃ b. (r => b * hP)(h ++ r) ⊦

Rule argument

Additional information

Proof step 4 from proof mapex-new (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 5:

  r ≠ null, hP(h), ¬ (r => (h ++ r)(r) * hP)(h ++ r), ¬ r ∈ h ⊦

Rule argument

Additional information

Used terms: (h ++ r)(r)

Proof step 5 from proof mapex-new (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:

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

Rule argument

Additional information

Used terms: r => (h ++ r)(r), h ++ r, hP

Proof step 6 from proof mapex-new (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof mapex-new (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  r ≠ null, hP(h), ¬ r ∈ h, ∀ h0, h1. ¬ h0 ⊥ h1 ∨ h ++ r ≠ h0 ∪ h1 ∨ ¬ (r => (h ++ r)(r))(h0) ∨ ¬ hP(h1) ⊦

Rule argument

Additional information

Proof step 8 from proof mapex-new (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) r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) r ∈ h ⊦ h(r) = o → h(r := o) = h; (s) ⊦ (r => o)(h) ↔ h = (∅ ++ r)(r := o) ∧ r ≠ null; (ss) Used terms: (∅ ++ r)(r := (h ++ r)(r)), h

Proof step 9 from proof mapex-new (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  r ≠ null, (r => o * hP)(h ++ r), ¬ hP(h), ¬ r ∈ h ⊦

Rule argument

Additional information

Proof step 10 from proof mapex-new (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

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

• Proof step 12:

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

Rule argument

Additional information

Used terms: h ++ r, hP, r => o

Proof step 11 from proof mapex-new (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof mapex-new (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Proof step 13 from proof mapex-new (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used formulas: h = h1

Proof step 14 from proof mapex-new (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ h0 = h1 ↔ (∀ r. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 16:

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

Rule argument

Additional information

Used terms: h, h1

Proof step 15 from proof mapex-new (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof mapex-new (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) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 18:

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

Rule argument

Additional information

Used terms: h ++ r, h0 ∪ h1

Proof step 17 from proof mapex-new (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof mapex-new (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  r ≠ null, h0 ⊥ h1, hP(h1), (r => o)(h0), ¬ hP(h), ¬ r ∈ h, ∀ r1. (r1 = r ∨ r1 ∈ h ↔ r1 ∈ h0 ∨ r1 ∈ h1) ∧ (r1 = r ∨ r1 ∈ h → (h ++ r)(r1) = (h0 ∪ h1)(r1)) ⊦ (r0 ∈ h1 ↔ r0 ∈ h) ∧ (r0 ∈ h1 → h1(r0) = h(r0))

Rule argument

Additional information

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

Proof step 19 from proof mapex-new (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

  r0 = r ∨ r0 ∈ h ↔ r0 ∈ h0 ∨ r0 ∈ h1, r ≠ null, h0 ⊥ h1, hP(h1), (r => o)(h0), ¬ hP(h), ¬ r ∈ h, r0 = r ∨ r0 ∈ h → (h ++ r)(r0) = (h0 ∪ h1)(r0) ⊦ (r0 ∈ h1 ↔ r0 ∈ h) ∧ (r0 ∈ h1 → h1(r0) = h(r0))

Rule argument

Additional information

Used terms: r0

Proof step 20 from proof mapex-new (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  r0 = r ∨ r0 ∈ h ↔ r0 ∈ h0 ∨ r0 ∈ h1, r ≠ null, h0 ⊥ h1, hP(h1), (r => o)(h0), ¬ hP(h), ¬ r ∈ h, r0 ∈ h0 ∨ r0 ∈ h1 → (h ++ r)(r0) = (r0 ∈ h0 ⊃ h0(r0);h1(r0)) ⊦ (r0 ∈ h1 ↔ r0 ∈ h) ∧ (r0 ∈ h1 → h1(r0) = h(r0))

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 21 from proof mapex-new (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 22:

  (h ++ r)(r0) = (r0 ∈ h0 ⊃ h0(r0);h1(r0)), r0 = r ∨ r0 ∈ h ↔ r0 ∈ h0 ∨ r0 ∈ h1, r ≠ null, h0 ⊥ h1, hP(h1), (r => o)(h0), ¬ hP(h), ¬ r ∈ h ⊦ (r0 ∈ h1 ↔ r0 ∈ h) ∧ (r0 ∈ h1 → h1(r0) = h(r0))

Rule argument

Additional information

Proof step 22 from proof mapex-new (previous step) (back to tree)

User applied rule unfold

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  (h ++ r)(r0) = (r0 ∈ h0 ⊃ h0(r0);h1(r0)), h2 = (∅ ++ r1)(r1 := o0), h2 = h0, o0 = o, r0 = r ∨ r0 ∈ h ↔ r0 ∈ h0 ∨ r0 ∈ h1, r1 = r, r ≠ null, r1 ≠ null, h0 ⊥ h1, hP(h1), ¬ hP(h), ¬ r ∈ h ⊦ (r0 ∈ h1 ↔ r0 ∈ h) ∧ (r0 ∈ h1 → h1(r0) = h(r0))

Rule argument

Additional information

Proof step 23 from proof mapex-new (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof mapex-new (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  (h ++ r)(r0) = (r0 = r ⊃ o0;h1(r0)), r ≠ null, hP(h1), ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1, r0 ≠ r → (r0 ∈ h ↔ r0 ∈ h1) ⊦ (r0 ∈ h1 ↔ r0 ∈ h) ∧ (r0 ∈ h1 → h1(r0) = h(r0))

Rule argument

Additional information

Used simplifier rules: r ≠ null ⊦ (∅ ++ r)(r := o) ⊥ h ↔ ¬ r ∈ h; (s) r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) ⊦ ¬ r ∈ ∅; (s) ⊦ h(r0 := o)(r) = (r = r0 ∧ r0 ∈ h ⊃ o;h(r)); (s) ⊦ r ∈ h(r0 := o) ↔ r ∈ h; (s)

Proof step 25 from proof mapex-new (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ (h ++ r0)(r) = h(r); (s)