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) ↔ (∃ o. ((r => o * hP))(h ++ r))

Rule argument

Additional information

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

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 ⊦ ∃ o. ((r => o * hP))(h ++ r)

• Proof step 21:

  r ≠ null, ¬ hP(h), ¬ r ∈ h, ∃ o. ((r => o * 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: h ++ r, hP, r => (h ++ r)[r]

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, ∀ h1. r ∈ h1 ∨ h ++ r ≠ (∅ ++ r)[r, (h ++ r)[r]] ∪ h1 ∨ ¬ hP(h1) ⊦

Rule argument

Additional information

Used simplifier rules: maplet: ⊦ ((r => o))(h) ↔ h = (∅ ++ r)[r, o] ∧ r ≠ null; r ≠ null ⊦ (∅ ++ r)[r, o] ⊥ h ↔ ¬ r ∈ h; (s)

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

User applied rule all left

And obtained the following new goals

• Proof step 9:

  r ≠ null, hP(h), ¬ r ∈ h, r ∈ h ∨ h ++ r ≠ (∅ ++ r)[r, (h ++ r)[r]] ∪ h ∨ ¬ hP(h) ⊦

Rule argument

Additional information

Used terms: 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:

  h ++ r ≠ (∅ ++ r)[r, (h ++ r)[r]] ∪ h, r ≠ null, 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:

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

• Proof step 12:

  r ≠ null, hP(h), ¬ r ∈ h, ∃ r0. ¬((r0 ∈ h ++ r ↔ r0 ∈ (∅ ++ r)[r, (h ++ r)[r]] ∪ h) ∧ (r0 ∈ h ++ r → (h ++ r)[r0] = ((∅ ++ r)[r, (h ++ r)[r]] ∪ h)[r0])) ⊦

Rule argument

Additional information

Used terms: (∅ ++ r)[r, (h ++ r)[r]] ∪ h, h ++ r

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:

  r ≠ null, hP(h), ¬ r ∈ h ⊦ (r0 = r ∨ r0 ∈ h ↔ r0 ∈ (∅ ++ r)[r, (h ++ r)[r]] ∪ h) ∧ (r0 = r ∨ r0 ∈ h → (h ++ r)[r0] = ((∅ ++ r)[r, (h ++ r)[r]] ∪ h)[r0])

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  r ≠ null, hP(h), ¬ r ∈ h ⊦ (r0 = r ∨ r0 ∈ h ↔ r0 ∈ (∅ ++ r)[r, (h ++ r)[r]] ∪ h) ∧ (r0 = r ∨ r0 ∈ h → (h ++ r)[r0] = ((∅ ++ r)[r, (h ++ r)[r]] ∪ h)[r0]), r0 ∈ (∅ ++ r)[r, (h ++ r)[r]] ∪ h ∧ (∅ ++ r)[r, (h ++ r)[r]] ⊥ h

• Proof step 18:

  r ≠ null, hP(h), r0 ∈ (∅ ++ r)[r, (h ++ r)[r]] ∪ h, (∅ ++ r)[r, (h ++ r)[r]] ⊥ h, ¬ r ∈ h ⊦ (r0 = r ∨ r0 ∈ h ↔ r0 ∈ (∅ ++ r)[r, (h ++ r)[r]] ∪ h) ∧ (r0 = r ∨ r0 ∈ h → (h ++ r)[r0] = (r0 ∈ (∅ ++ r)[r, (h ++ r)[r]] ⊃ (∅ ++ r)[r, (h ++ r)[r]][r0];h[r0]))

Rule argument

Additional information

Used terms: r0, h, (∅ ++ r)[r, (h ++ r)[r]]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  r ≠ null, r0 ≠ r, hP(h), r0 ∈ (∅ ++ r)[r, (h ++ r)[r]] ∪ h, ¬ r ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

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

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 ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

Rule argument

Additional information

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

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, hP(h), r0 ∈ (∅ ++ r)[r, (h ++ r)[r]] ∪ h, ¬ r ∈ h ⊦ (r0 = r ∨ r0 ∈ h) ∧ (h ++ r)[r0] = (r0 = r ⊃ (h ++ r)[r];h[r0])

Rule argument

Additional information

Used simplifier rules: 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) r ≠ null ⊦ (∅ ++ r)[r, o] ⊥ h ↔ ¬ r ∈ h; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

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

• Proof step 24:

  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 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 = (∅ ++ r)[r, o] ∪ h1, r ≠ null, hP(h1), ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used simplifier rules: maplet: ⊦ ((r => o))(h) ↔ h = (∅ ++ r)[r, o] ∧ r ≠ null; r ≠ null ⊦ (∅ ++ r)[r, o] ⊥ h ↔ ¬ r ∈ h; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 26:

  h ++ r = (∅ ++ r)[r, o] ∪ h1, h ≠ h1, r ≠ null, hP(h1), ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1 ⊦

Rule argument

Additional information

Used formulas: h = h1

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

  h ++ r = (∅ ++ r)[r, o] ∪ h1, r ≠ null, hP(h1), ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1, ∃ r. ¬((r ∈ h1 ↔ r ∈ h) ∧ (r ∈ h1 → h1[r] = h[r])) ⊦

Rule argument

Additional information

Used terms: h, h1

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

  r ≠ null, hP(h1), ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1, ∀ r0. (r0 ∈ h ++ r ↔ r0 ∈ (∅ ++ r)[r, o] ∪ h1) ∧ (r0 ∈ h ++ r → (h ++ r)[r0] = ((∅ ++ r)[r, o] ∪ h1)[r0]), ∃ r. ¬((r ∈ h1 ↔ r ∈ h) ∧ (r ∈ h1 → h1[r] = h[r])) ⊦

Rule argument

Additional information

Used terms: (∅ ++ r)[r, o] ∪ h1, h ++ r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  r ≠ null, hP(h1), ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1, ∀ r1. (r1 = r ∨ r1 ∈ h ↔ r1 ∈ (∅ ++ r)[r, o] ∪ h1) ∧ (r1 = r ∨ r1 ∈ h → (h ++ r)[r1] = ((∅ ++ r)[r, o] ∪ 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)

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

User applied rule all left

And obtained the following new goals

• Proof step 32:

  r0 = r ∨ r0 ∈ h ↔ r0 ∈ (∅ ++ r)[r, o] ∪ h1, r ≠ null, hP(h1), ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1, r0 = r ∨ r0 ∈ h → (h ++ r)[r0] = ((∅ ++ r)[r, o] ∪ h1)[r0] ⊦ (r0 ∈ h1 ↔ r0 ∈ h) ∧ (r0 ∈ h1 → h1[r0] = h[r0])

Rule argument

Additional information

Used terms: r0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  r0 = r ∨ r0 ∈ h ↔ r0 ∈ (∅ ++ r)[r, o] ∪ h1, r ≠ null, hP(h1), ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1, r0 = r ∨ r0 ∈ h → (h ++ r)[r0] = ((∅ ++ r)[r, o] ∪ h1)[r0] ⊦ (r0 ∈ h1 ↔ r0 ∈ h) ∧ (r0 ∈ h1 → h1[r0] = h[r0])

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

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

• Proof step 38:

  r0 = r ∨ r0 ∈ h ↔ r0 ∈ (∅ ++ r)[r, o] ∪ h1, r ≠ null, hP(h1), r0 ∈ (∅ ++ r)[r, o] ∪ h1, (∅ ++ r)[r, o] ⊥ h1, ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1, r0 = r ∨ r0 ∈ h → (h ++ r)[r0] = (r0 ∈ (∅ ++ r)[r, o] ⊃ (∅ ++ r)[r, o][r0];h1[r0]) ⊦ (r0 ∈ h1 ↔ r0 ∈ h) ∧ (r0 ∈ h1 → h1[r0] = h[r0])

Rule argument

Additional information

Used terms: r0, h1, (∅ ++ r)[r, o]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  h[r0] = ((∅ ++ r)[r, o] ∪ h1)[r0], r ≠ null, r0 ≠ r, hP(h1), r0 ∈ h, r0 ∈ (∅ ++ r)[r, o] ∪ h1, ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1, ¬ r0 ∈ h1 ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ 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) r ≠ null ⊦ (∅ ++ r)[r, o] ⊥ h ↔ ¬ r ∈ h; (s) ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s) r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) ⊦ ¬ r ∈ ∅; (s) Used terms: h1, (∅ ++ r)[r, o], r0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  r ≠ null, hP(h1), r0 ∈ (∅ ++ r)[r, o] ∪ h1, ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1, r0 ≠ r → (r0 ∈ h ↔ r0 ∈ h1), r0 = r ∨ r0 ∈ h → (h ++ r)[r0] = (r0 = r ⊃ o;h1[r0]) ⊦ (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) ⊦ ¬ r ∈ ∅; (s) ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]); (s) ⊦ r ∈ h[r0, o] ↔ r ∈ h; (s) r ≠ null ⊦ (∅ ++ r)[r, o] ⊥ h ↔ ¬ r ∈ h; (s) ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 40:

  (h ++ r)[r0] = (r0 = r ⊃ o;h1[r0]), r ≠ null, hP(h1), r0 ∈ (∅ ++ r)[r, o] ∪ 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

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

User applied rule case distinction

And obtained the following new goals

• Proof step 41:

  r0 ∈ h ↔ r0 ∈ h1, (h ++ r)[r0] = (r0 = r ⊃ o;h1[r0]), r ≠ null, hP(h1), r0 ∈ (∅ ++ r)[r, o] ∪ h1, ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1 ⊦ (r0 ∈ h1 ↔ r0 ∈ h) ∧ (r0 ∈ h1 → h1[r0] = h[r0])

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h → r ≠ null; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  (h ++ r)[r0] = h1[r0], h1[r0] ≠ h[r0], r ≠ null, hP(h1), r0 ∈ (∅ ++ r)[r, o] ∪ h1, r0 ∈ h1, r0 ∈ h, ¬ hP(h), ¬ r ∈ h, ¬ r ∈ h1 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  r ∈ h, r0 ≠ null, ¬ r0 ∈ h ⊦ r ≠ r0 → (h ++ r0)[r] = h[r]

Rule argument

Additional information

Used terms: r0, r, h

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

A spec-lemma