Proof step 1 from proof map-del-sharing (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬((r => o ⊗ hP)(h) ↔ (hP(h -- r) ∨ hP(h)) ∧ r ∈ h ∧ h(r) = o) ⊦

Rule argument

Additional information

Proof step 2 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

  ⊦ (∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ (r => o)(h0 ∪ h2) ∧ hP(h1 ∪ h2)) ↔ (hP(h -- r) ∨ hP(h)) ∧ r ∈ h ∧ h(r) = o

Rule argument

Additional information

Used simplifier rules: sharing-ass: ⊦ hP0 ⊗ hP1 ⊗ hP2 = (hP0 ⊗ hP1) ⊗ hP2; from specification map-sep sharing-com: ⊦ hP0 ⊗ hP1 = hP1 ⊗ hP0; from specification map-sep Used terms: h, r => o, hP

Proof step 3 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ⊦ (∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ h0 ∪ h2 = ∅(r := o) ∧ hP(h1 ∪ h2)) ↔ (hP(h -- r) ∨ hP(h)) ∧ r ∈ h ∧ h(r) = o

Rule argument

Additional information

Used simplifier rules: maplet: ⊦ (r => o)(h) ↔ h = ∅(r := o);

Proof step 5 from proof map-del-sharing (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  ∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ h0 ∪ h2 = ∅(r := o) ∧ hP(h1 ∪ h2) ⊦ (hP(h -- r) ∨ hP(h)) ∧ r ∈ h ∧ h(r) = o

• Proof step 71:

  h(r) = o, r ∈ h, hP(h -- r) ∨ hP(h) ⊦ ∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ h0 ∪ h2 = ∅(r := o) ∧ hP(h1 ∪ h2)

Rule argument

Additional information

Proof step 6 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Proof step 7 from proof map-del-sharing (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h2 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o

• Proof step 42:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), ¬ r ∈ h2 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used formulas: r ∈ h2

Proof step 8 from proof map-del-sharing (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  h0 ∪ h2 = ∅(r := o), h2 = ∅(r := o), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h2 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o

• Proof step 30:

  h0 ∪ h2 = ∅(r := o), h2 ≠ ∅(r := o), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h2 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used formulas: h2 = ∅(r := o)

Proof step 9 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  h0(r := o) = ∅(r := o), h0 ⊥ h1, hP(h1(r := o)), ¬ r ∈ h1, ¬ r ∈ h0 ⊦ (hP((h0 ∪ h1(r := o)) -- r) ∨ hP(h0 ∪ h1(r := o))) ∧ r ∈ h0 ∪ h1(r := o) ∧ (h0 ∪ h1(r := o))(r) = o

Rule argument

Additional information

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

Proof step 10 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

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

• Proof step 12:

  h0(r := o) = ∅(r := o), h0 ⊥ h1, h0 ⊥ h1(r := o), hP(h1(r := o)), ¬ r ∈ h1, ¬ r ∈ h0 ⊦ (hP((h0 ∪ h1(r := o)) -- r) ∨ hP(h0 ∪ h1(r := o))) ∧ (r ∈ h0 ∨ r ∈ h1(r := o)) ∧ (h0 ∪ h1(r := o))(r) = o

Rule argument

Additional information

Used simplifier rules: ¬ r ∈ h1 ⊦ h0 ⊥ h1(r := o) ↔ h0 ⊥ h1 ∧ ¬ r ∈ h0; (s) Used terms: r, h0, h1(r := o)

Proof step 11 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  h0(r := o) = ∅(r := o), h0 ⊥ h1, hP(h1(r := o)), ¬ r ∈ h1, ¬ r ∈ h0 ⊦ (hP((h0 ∪ h1(r := o)) -- r) ∨ hP(h0 ∪ h1(r := o))) ∧ (h0 ∪ h1(r := o))(r) = o

Rule argument

Additional information

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

Proof step 13 from proof map-del-sharing (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:

  h0(r := o) = ∅(r := o), h0 ⊥ h1, h0 ⊥ h1(r := o), hP(h1(r := o)), r ∈ h0 ∪ h1(r := o), ¬ r ∈ h1, ¬ r ∈ h0 ⊦ (hP((h0 ∪ h1(r := o)) -- r) ∨ hP(h0 ∪ h1(r := o))) ∧ (r ∈ h0 ⊃ h0(r);h1(r := o)(r)) = o

Rule argument

Additional information

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

Proof step 14 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

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

Proof step 16 from proof map-del-sharing (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)

• Proof step 18:

  h0(r := o) = ∅(r := o), h0 ⊥ h1, h0 ⊥ h1(r := o), hP(h1(r := o)), ¬ hP((h0 ∪ h1(r := o)) -- r), ¬ hP(h0 ∪ h1(r := o)), ¬ r ∈ h1, ¬ r ∈ h0, r ∈ h0 ∨ r ∈ h1(r := o) ⊦

Rule argument

Additional information

Used simplifier rules: ¬ r ∈ h1 ⊦ h0 ⊥ h1(r := o) ↔ h0 ⊥ h1 ∧ ¬ r ∈ h0; (s) Used terms: r, h0, h1(r := o)

Proof step 17 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

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

Rule argument

Additional information

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

Proof step 19 from proof map-del-sharing (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ∅ ⊥ h; (s) ⊦ st(a := d) -- a = st -- a; (s) ⊦ ¬ a ∈ st → st -- a = st; (s) ⊦ ∅ ∪ h = h; (s) ⊦ ¬ a ∈ ∅; (s) Used formulas: h0 = ∅

Proof step 20 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  h0(r := o) = ∅(r := o), h0 ⊥ h1, hP(h1(r := o)), ¬ hP((h0 ∪ h1(r := o)) -- r), ¬ hP(h0 ∪ h1(r := o)), ¬ r ∈ h1, ¬ r ∈ h0, ∃ a. ¬((a ∈ h0 ↔ a ∈ ∅) ∧ h0(a) = ∅(a)) ⊦

Rule argument

Additional information

Used terms: h0, ∅

Proof step 21 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 22 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  h0(r := o) = ∅(r := o), h0 ⊥ h1, hP(h1(r := o)), ¬ hP((h0 ∪ h1(r := o)) -- r), ¬ hP(h0 ∪ h1(r := o)), ¬ r ∈ h1, ¬ r ∈ h0 ⊦ ¬ r0 ∈ h0 ∧ h0(r0) = ∅(r0)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 23 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

  h0 ⊥ h1, hP(h1(r := o)), ¬ hP((h0 ∪ h1(r := o)) -- r), ¬ hP(h0 ∪ h1(r := o)), ¬ r ∈ h1, ¬ r ∈ h0, ∀ a. (a ∈ h0(r := o) ↔ a ∈ ∅(r := o)) ∧ h0(r := o)(a) = ∅(r := o)(a) ⊦ ¬ r0 ∈ h0 ∧ h0(r0) = ∅(r0)

Rule argument

Additional information

Used terms: h0(r := o), ∅(r := o)

Proof step 24 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  h0 ⊥ h1, hP(h1(r := o)), ¬ hP((h0 ∪ h1(r := o)) -- r), ¬ hP(h0 ∪ h1(r := o)), ¬ r ∈ h1, ¬ r ∈ h0, ∀ a. ¬ a ∈ h0 ∧ h0(r := o)(a) = ∅(r := o)(a) ⊦ ¬ r0 ∈ h0 ∧ h0(r0) = ∅(r0)

Rule argument

Additional information

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

Proof step 26 from proof map-del-sharing (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 27:

  h0(r := o)(r0) = ∅(r := o)(r0), h0 ⊥ h1, hP(h1(r := o)), ¬ hP((h0 ∪ h1(r := o)) -- r), ¬ hP(h0 ∪ h1(r := o)), ¬ r ∈ h1, ¬ r ∈ h0, ¬ r0 ∈ h0 ⊦ ¬ r0 ∈ h0 ∧ h0(r0) = ∅(r0)

Rule argument

Additional information

Used terms: r0

Proof step 27 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

Proof step 28 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Used terms: h0, r0

Proof step 29 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

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

• Proof step 32:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h2, ∃ a. ¬((a ∈ h2 ↔ a ∈ ∅(r := o)) ∧ h2(a) = ∅(r := o)(a)) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used terms: h2, ∅(r := o)

Proof step 31 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h2 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o, (r0 ∈ h2 → r0 = r) ∧ h2(r0) = ∅(r := o)(r0)

Rule argument

Additional information

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

Proof step 33 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

  h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h2, ∀ a. (a ∈ h0 ∪ h2 ↔ a ∈ ∅(r := o)) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o, (r0 ∈ h2 → r0 = r) ∧ h2(r0) = ∅(r := o)(r0)

Rule argument

Additional information

Used terms: h0 ∪ h2, ∅(r := o)

Proof step 34 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h2, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o, (r0 ∈ h2 → r0 = r) ∧ h2(r0) = ∅(r := o)(r0)

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); (s) ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); (s) ⊦ a ∈ ∅(b := d) ↔ a = b; (s)

Proof step 36 from proof map-del-sharing (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 37:

  (h0 ∪ h2)(r0) = ∅(r := o)(r0), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h2, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a), r0 ∈ h0 ∨ r0 ∈ h2 → r0 = r ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o, (r0 ∈ h2 → r0 = r) ∧ h2(r0) = ∅(r := o)(r0)

Rule argument

Additional information

Used terms: r0

Proof step 37 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

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

• Proof step 39:

  ∅(r0) = ∅(r := o)(r0), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h2, ¬ r0 ∈ h0 ∪ h2, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a), r0 ∈ h0 ∨ r0 ∈ h2 → r0 = r ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o, (r0 ∈ h2 → r0 = r) ∧ h2(r0) = ∅(r := o)(r0)

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 := d)(a) = d; (s) ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); (s) Used terms: h0 ∪ h2, r0

Proof step 38 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 39 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  ∅(r0) = ∅(r := o)(r0), h2(r0) ≠ ∅(r0), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h2, ¬ r0 ∈ h0, ¬ r0 ∈ h2, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h0 ∪ h1 ∪ h2 ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); (s)

Proof step 40 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

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

Rule argument

Additional information

Used terms: h2, r0

Proof step 41 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 42 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

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

• Proof step 44:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h2, h0 ⊥ h1, h0 ⊥ h1 ∪ h2, h1 ⊥ h2, hP(h1 ∪ h2), ¬ r ∈ h2 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (r ∈ h0 ∨ r ∈ h1 ∪ h2) ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used simplifier rules: h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws) Used terms: r, h0, h1 ∪ h2

Proof step 43 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), ¬ r ∈ h2 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (r ∈ h0 ∨ r ∈ h1) ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); (s) h1 ⊥ h ⊦ h0 ⊥ h1 ∪ h ↔ h0 ⊥ h1 ∧ h0 ⊥ h; (ws)

Proof step 45 from proof map-del-sharing (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 46:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, ¬ r ∈ h2 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (r ∈ h0 ∨ r ∈ h1) ∧ (h0 ∪ h1 ∪ h2)(r) = o

• Proof step 66:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), ¬ r ∈ h0, ¬ r ∈ h2 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (r ∈ h0 ∨ r ∈ h1) ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used formulas: r ∈ h0

Proof step 46 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → (r ∈ h1 ↔ false); (s)

Proof step 47 from proof map-del-sharing (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 48:

  h0 ∪ h2 = ∅(r := o), h2 ≠ ∅, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used simplifier rules: ⊦ h ⊥ ∅; (s) ⊦ h0 ⊥ h1 → (h0 ∪ h1) -- r = (h0 -- r) ∪ (h1 -- r); (s) ⊦ h0 ∪ ∅ = h0; (s) ⊦ 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 := d) ↔ a = b; (s) ⊦ ∅(r := o) ⊥ h ↔ ¬ r ∈ h; (s) ⊦ st(a := d) -- a = st -- a; (s) ⊦ ∅ -- a = ∅; (s) ⊦ ¬ a ∈ st → st -- a = st; (s) ⊦ ∅ ∪ h = h; (s) ⊦ a = b → st(b := d)(a) = d; (s) Used formulas: h2 = ∅

Proof step 48 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, ∃ a. ¬((a ∈ h2 ↔ a ∈ ∅) ∧ h2(a) = ∅(a)) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used terms: h2, ∅

Proof step 49 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o, ¬ r0 ∈ h2 ∧ h2(r0) = ∅(r0)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 51 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

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

• Proof step 53:

  h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, ∀ a. (a ∈ h0 ∪ h2 ↔ a ∈ ∅(r := o)) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o, ¬ r0 ∈ h2 ∧ h2(r0) = ∅(r0)

Rule argument

Additional information

Used terms: h0 ∪ h2, ∅(r := o)

Proof step 52 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o, ¬ r0 ∈ h2 ∧ h2(r0) = ∅(r0)

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); (s) ⊦ a ∈ ∅(b := d) ↔ a = b; (s)

Proof step 54 from proof map-del-sharing (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 55:

  (h0 ∪ h2)(r0) = ∅(r := o)(r0), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a), r0 ∈ h0 ∨ r0 ∈ h2 → r0 = r ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o, ¬ r0 ∈ h2 ∧ h2(r0) = ∅(r0)

Rule argument

Additional information

Used terms: r0

Proof step 55 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

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

• Proof step 57:

  (h0 ∪ h2)(r0) = ∅(r := o)(r0), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, r0 ∈ h0 ∪ h2, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a), r0 ∈ h0 ∨ r0 ∈ h2 → r0 = r ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o, ¬ r0 ∈ h2 ∧ h2(r0) = ∅(r0)

• Proof step 60:

  ∅(r0) = ∅(r := o)(r0), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, ¬ r0 ∈ h0 ∪ h2, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a), r0 ∈ h0 ∨ r0 ∈ h2 → r0 = r ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o, ¬ r0 ∈ h2 ∧ h2(r0) = ∅(r0)

Rule argument

Additional information

Used terms: h0 ∪ h2, r0

Proof step 56 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 57 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  h2(r) ≠ ∅(r), h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := h0(r))(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = h0(r)

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h0 ∧ h0 ⊥ h1 → (r ∈ h1 ↔ false); (s) ⊦ a = b → st(b := d)(a) = d; (s) 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 58 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 59:

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

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); (s) Used terms: h2, r

Proof step 59 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 60 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  ∅(r0) = ∅(r := o)(r0), h2(r0) ≠ ∅(r0), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, ¬ r0 ∈ h0, ¬ r0 ∈ h2, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used simplifier rules: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); (s)

Proof step 61 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 62:

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

• Proof step 63:

  ∅(r0) = ∅(r0), h2(r0) ≠ ∅(r0), r0 ≠ r, h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, ¬ r0 ∈ h0, ¬ r0 ∈ h2, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used simplifier rules: ⊦ a = b → st(b := d)(a) = d; (s) Used terms: ∅, r, o, r0

Proof step 62 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 63 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  h2(r0) ≠ ∅(r0), r0 ≠ r, h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), r ∈ h0, ¬ r0 ∈ h0, ¬ r0 ∈ h2, ∀ a. (a ∈ h0 ∨ a ∈ h2 → a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Proof step 64 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 65:

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

Rule argument

Additional information

Used terms: h2, r0

Proof step 65 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 66 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 67:

  h0 ∪ h2 = ∅(r := o), h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), ¬ r ∈ h0, ¬ r ∈ h2 ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h1 ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Proof step 67 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 68:

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

• Proof step 69:

  h0 ⊥ h2, h0 ⊥ h1, h1 ⊥ h2, hP(h1 ∪ h2), ¬ r ∈ h0, ¬ r ∈ h2, ∀ a. (a ∈ h0 ∪ h2 ↔ a ∈ ∅(r := o)) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h1 ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used terms: h0 ∪ h2, ∅(r := o)

Proof step 68 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 69 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  h0 ⊥ h1, h0 ⊥ h2, h1 ⊥ h2, hP(h1 ∪ h2), ¬ r ∈ h0, ¬ r ∈ h2, ∀ a. (a ∈ h0 ∨ a ∈ h2 ↔ a = r) ∧ (h0 ∪ h2)(a) = ∅(r := o)(a) ⊦ (hP((h0 ∪ h1 ∪ h2) -- r) ∨ hP(h0 ∪ h1 ∪ h2)) ∧ r ∈ h1 ∧ (h0 ∪ h1 ∪ h2)(r) = o

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ ∅(b := d) ↔ a = b; (s) ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); (s)

Proof step 70 from proof map-del-sharing (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 71 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 72:

  r ∈ h, hP(h -- r) ∨ hP(h) ⊦ ∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ h0 ∪ h2 = ∅(r := (h0 ∪ h1 ∪ h2)(r)) ∧ hP(h1 ∪ h2)

Rule argument

Additional information

Proof step 72 from proof map-del-sharing (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 73:

  hP(h -- r), r ∈ h ⊦ ∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ h0 ∪ h2 = ∅(r := (h0 ∪ h1 ∪ h2)(r)) ∧ hP(h1 ∪ h2)

• Proof step 74:

  hP(h), r ∈ h ⊦ ∃ h0, h1, h2. h0 ⊥ h2 ∧ h0 ⊥ h1 ∧ h1 ⊥ h2 ∧ h = h0 ∪ h1 ∪ h2 ∧ h0 ∪ h2 = ∅(r := (h0 ∪ h1 ∪ h2)(r)) ∧ hP(h1 ∪ h2)

Rule argument

Additional information

Proof step 73 from proof map-del-sharing (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

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

Proof step 74 from proof map-del-sharing (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 75:

  hP(h), r ∈ h ⊦ ∅ ⊥ ∅(r := h(r)) ∧ ∅ ⊥ h -- r ∧ h -- r ⊥ ∅(r := h(r)) ∧ h = ∅ ∪ (h -- r) ∪ ∅(r := h(r)) ∧ ∅ ∪ ∅(r := h(r)) = ∅(r := (∅ ∪ (h -- r) ∪ ∅(r := h(r)))(r)) ∧ hP((h -- r) ∪ ∅(r := h(r)))

Rule argument

Additional information

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

Proof step 75 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  hP(h), r ∈ h ⊦ h = (h -- r) ∪ ∅(r := h(r)) ∧ h(r) = ((h -- r) ∪ ∅(r := h(r)))(r) ∧ hP((h -- r) ∪ ∅(r := h(r)))

Rule argument

Additional information

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

Proof step 76 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 77:

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

• Proof step 78:

  h -- r ⊥ ∅(r := h(r)), hP(h), r ∈ h, r ∈ (h -- r) ∪ ∅(r := h(r)) ⊦ h = (h -- r) ∪ ∅(r := h(r)) ∧ h(r) = (r ∈ h -- r ⊃ (h -- r)(r);∅(r := h(r))(r)) ∧ hP((h -- r) ∪ ∅(r := h(r)))

Rule argument

Additional information

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

Proof step 77 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 78 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  hP(h), r ∈ (h -- r) ∪ ∅(r := h(r)), r ∈ h ⊦ h = (h -- r) ∪ ∅(r := h(r)) ∧ hP((h -- r) ∪ ∅(r := h(r)))

Rule argument

Additional information

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

Proof step 79 from proof map-del-sharing (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 80:

  h ≠ (h -- r) ∪ ∅(r := h(r)), hP(h), r ∈ h, r ∈ (h -- r) ∪ ∅(r := h(r)) ⊦ h = (h -- r) ∪ ∅(r := h(r)) ∧ hP((h -- r) ∪ ∅(r := h(r)))

Rule argument

Additional information

Used formulas: h = (h -- r) ∪ ∅(r := h(r))

Proof step 80 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 81:

  h ≠ (h -- r) ∪ ∅(r := h(r)), hP(h), r ∈ (h -- r) ∪ ∅(r := h(r)), r ∈ h ⊦

Rule argument

Additional information

Proof step 81 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 82:

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

• Proof step 83:

  hP(h), r ∈ h, r ∈ (h -- r) ∪ ∅(r := h(r)), ∃ a. ¬((a ∈ (h -- r) ∪ ∅(r := h(r)) ↔ a ∈ h) ∧ ((h -- r) ∪ ∅(r := h(r)))(a) = h(a)) ⊦

Rule argument

Additional information

Used terms: h, (h -- r) ∪ ∅(r := h(r))

Proof step 82 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 83 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

  hP(h), r ∈ (h -- r) ∪ ∅(r := h(r)), r ∈ h ⊦ (r0 ∈ (h -- r) ∪ ∅(r := h(r)) ↔ r0 ∈ h) ∧ ((h -- r) ∪ ∅(r := h(r)))(r0) = h(r0)

Rule argument

Additional information

Proof step 84 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 85:

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

• Proof step 86:

  h -- r ⊥ ∅(r := h(r)), hP(h), r ∈ h, r ∈ (h -- r) ∪ ∅(r := h(r)) ⊦ (r0 ∈ h -- r ∨ r0 ∈ ∅(r := h(r)) ↔ r0 ∈ h) ∧ ((h -- r) ∪ ∅(r := h(r)))(r0) = h(r0)

Rule argument

Additional information

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

Proof step 85 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 86 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 87:

  ((h -- r) ∪ ∅(r := h(r)))(r0) ≠ h(r0), hP(h), r ∈ (h -- r) ∪ ∅(r := h(r)), r ∈ h ⊦

Rule argument

Additional information

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

Proof step 87 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 88:

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

• Proof step 89:

  ((h -- r) ∪ ∅(r := h(r)))(r0) ≠ h(r0), h -- r ⊥ ∅(r := h(r)), hP(h), r ∈ h, r ∈ h -- r ∨ r ∈ ∅(r := h(r)) ⊦

Rule argument

Additional information

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

Proof step 88 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 89 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 90:

  ((h -- r) ∪ ∅(r := h(r)))(r0) ≠ h(r0), hP(h), r ∈ h ⊦

Rule argument

Additional information

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

Proof step 90 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 91:

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

• Proof step 92:

  ((h -- r) ∪ ∅(r := h(r)))(r0) ≠ h(r0), hP(h), r ∈ h ⊦ r0 ∈ (h -- r) ∪ ∅(r := h(r)) ∧ h -- r ⊥ ∅(r := h(r))

• Proof step 102:

  (r0 ∈ h -- r ⊃ (h -- r)(r0);∅(r := h(r))(r0)) ≠ h(r0), h -- r ⊥ ∅(r := h(r)), hP(h), r ∈ h, r0 ∈ (h -- r) ∪ ∅(r := h(r)) ⊦

Rule argument

Additional information

Used terms: h -- r, ∅(r := h(r)), r0

Proof step 91 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 92 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 93:

  ((h -- r) ∪ ∅(r := h(r)))(r0) ≠ h(r0), hP(h), r ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

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

Proof step 93 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 94:

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

• Proof step 95:

  ((h -- r) ∪ ∅(r := h(r)))(r0) ≠ h(r0), hP(h), r ∈ h, r0 ∈ (h -- r) ∪ ∅(r := h(r)), ¬ r0 ∈ h ⊦

• Proof step 97:

  ∅(r0) ≠ h(r0), hP(h), r ∈ h, ¬ r0 ∈ (h -- r) ∪ ∅(r := h(r)), ¬ r0 ∈ h ⊦

Rule argument

Additional information

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

Proof step 94 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 95 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 96:

  ⊦ 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 ∈ ∅; (s) ¬ r ∈ h1 ⊦ h0 ⊥ h1(r := o) ↔ h0 ⊥ h1 ∧ ¬ r ∈ h0; (s) ⊦ h ⊥ ∅; (s) ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; (s) ⊦ a ∈ ∅(b := d) ↔ a = b; (s) Used terms: r0, h -- r, ∅(r := h(r))

Proof step 96 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 97 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 98:

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

• Proof step 99:

  ∅(r0) ≠ h(r0), h -- r ⊥ ∅(r := h(r)), hP(h), r ∈ h, ¬ r0 ∈ ∅(r := h(r)), ¬ r0 ∈ h -- r, ¬ r0 ∈ h ⊦

Rule argument

Additional information

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

Proof step 98 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 99 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 100:

  r0 ≠ r, ∅(r0) ≠ h(r0), hP(h), r ∈ h, ¬ r0 ∈ h ⊦

Rule argument

Additional information

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

Proof step 100 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 101:

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

Rule argument

Additional information

Used terms: h, r0

Proof step 101 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma

Proof step 102 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 103:

  (r0 ≠ r ∧ r0 ∈ h ⊃ h(r0);∅(r := h(r))(r0)) ≠ h(r0), hP(h), r ∈ h, r0 ∈ (h -- r) ∪ ∅(r := h(r)) ⊦

Rule argument

Additional information

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

Proof step 103 from proof map-del-sharing (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 104:

  ∅(r := h(r))(r0) ≠ h(r0), hP(h), r ∈ h, r0 ∈ (h -- r) ∪ ∅(r := h(r)), r0 = r ∨ ¬ r0 ∈ h ⊦

Rule argument

Additional information

Proof step 104 from proof map-del-sharing (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 105:

  r0 ≠ r, ∅(r0) ≠ h(r0), hP(h), r ∈ h, r0 ∈ (h -- r) ∪ ∅(r := h(r)), ¬ r0 ∈ h ⊦

Rule argument

Additional information

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

Proof step 105 from proof map-del-sharing (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 106:

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

Rule argument

Additional information

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

Proof step 106 from proof map-del-sharing (previous step) (back to tree)

A spec-lemma