Proof step 1 from proof union-left-singleton (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  r ≠ null, (∅ ++ r)[r, h[r]] ∪ (h -- r) ≠ h, r ∈ h ⊦

Rule argument

Additional information

Proof step 2 from proof union-left-singleton (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

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

• Proof step 4:

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

Rule argument

Additional information

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

Proof step 3 from proof union-left-singleton (previous step) (back to tree)

Lemma ext

Proof step 4 from proof union-left-singleton (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  r ∈ h ⊦ (r0 ∈ (∅ ++ r)[r, h[r]] ∪ (h -- r) ↔ r0 ∈ h) ∧ (r0 ∈ (∅ ++ r)[r, h[r]] ∪ (h -- r) → ((∅ ++ r)[r, h[r]] ∪ (h -- r))[r0] = h[r0])

Rule argument

Additional information

Used simplifier rules: nonnull: ⊦ r ∈ h → r ≠ null;

Proof step 5 from proof union-left-singleton (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  r ∈ h, (∅ ++ r)[r, h[r]] ⊥ h -- r ⊦ (r0 ∈ (∅ ++ r)[r, h[r]] ∨ r0 ∈ h -- r ↔ r0 ∈ h) ∧ (r0 ∈ (∅ ++ r)[r, h[r]] ∨ r0 ∈ h -- r → ((∅ ++ r)[r, h[r]] ∪ (h -- r))[r0] = h[r0])

Rule argument

Additional information

Used simplifier rules: nonnull: ⊦ r ∈ h → r ≠ null; disj-singleton-write: r ≠ null ⊦ (∅ ++ r)[r, o] ⊥ h ↔ ¬ r ∈ h; in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; Used terms: h -- r, (∅ ++ r)[r, h[r]], r0

Proof step 6 from proof union-left-singleton (previous step) (back to tree)

Lemma in-uni

Proof step 7 from proof union-left-singleton (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ((∅ ++ r)[r, h[r]] ∪ (h -- r))[r0] ≠ h[r0], r ∈ h, r0 ∈ h ⊦

Rule argument

Additional information

Used simplifier rules: disj-singleton-write: r ≠ null ⊦ (∅ ++ r)[r, o] ⊥ h ↔ ¬ r ∈ h; in-write: ⊦ r ∈ h[r0, o] ↔ r ∈ h; nonnull: ⊦ r ∈ h → r ≠ null; in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; in-emp: ⊦ ¬ r ∈ ∅; in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h;

Proof step 8 from proof union-left-singleton (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  (r0 ∈ (∅ ++ r)[r, h[r]] ⊃ (∅ ++ r)[r, h[r]][r0];(h -- r)[r0]) ≠ h[r0], r0 ∈ h, r ∈ h, r0 ∈ (∅ ++ r)[r, h[r]] ∪ (h -- r), (∅ ++ r)[r, h[r]] ⊥ h -- r ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1); in-write: ⊦ r ∈ h[r0, o] ↔ r ∈ h; in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; in-emp: ⊦ ¬ r ∈ ∅; nonnull: ⊦ r ∈ h → r ≠ null; disj-singleton-write: r ≠ null ⊦ (∅ ++ r)[r, o] ⊥ h ↔ ¬ r ∈ h; in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; Used terms: r0, h -- r, (∅ ++ r)[r, h[r]]

Proof step 9 from proof union-left-singleton (previous step) (back to tree)

Lemma at-uni

Proof step 10 from proof union-left-singleton (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (r0 = r ⊃ h[r];h[r0]) ≠ h[r0], r0 ∈ (∅ ++ r)[r, h[r]] ∪ (h -- r), r ∈ h, r0 ∈ h ⊦

Rule argument

Additional information

Used simplifier rules: in-write: ⊦ r ∈ h[r0, o] ↔ r ∈ h; at-write: ⊦ h[r0, o][r] = (r = r0 ∧ r0 ∈ h ⊃ o;h[r]); in-emp: ⊦ ¬ r ∈ ∅; in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; at-del: r ∈ h ⊦ r ≠ r0 → (h -- r0)[r] = h[r]; nonnull: ⊦ r ∈ h → r ≠ null; disj-singleton-write: r ≠ null ⊦ (∅ ++ r)[r, o] ⊥ h ↔ ¬ r ∈ h; in-del: ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h;

Proof step 11 from proof union-left-singleton (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used formulas: r0 = r