Proof step 1 from proof exin-uni (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  r ≠ null ⊦ r ∈ h ↔ (∃ h0, o. h = h0 ∪ (∅ ++ r)(r := o) ∧ ¬ r ∈ h0)

Rule argument

Additional information

Proof step 2 from proof exin-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  r ≠ null ⊦ r ∈ h ↔ (∃ h0, o. h = h0 ∪ (∅ ++ r)(r := o) ∧ ¬ r ∈ h0)

Rule argument

Additional information

Proof step 3 from proof exin-uni (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  r ≠ null, r ∈ h ⊦ ∃ h0, o. h = h0 ∪ (∅ ++ r)(r := o) ∧ ¬ r ∈ h0

• Proof step 15:

  r ≠ null, ¬ r ∈ h, ∃ h0, o. h = h0 ∪ (∅ ++ r)(r := o) ∧ ¬ r ∈ h0 ⊦

Rule argument

Additional information

Proof step 4 from proof exin-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  r ≠ null, r ∈ h ⊦ ∃ h0, o. h = h0 ∪ (∅ ++ r)(r := o) ∧ ¬ r ∈ h0

Rule argument

Additional information

Proof step 5 from proof exin-uni (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ r ≠ null → (r ∈ h ↔ (∃ h0, o. h = (h0 ++ r)(r := o) ∧ ¬ r ∈ h0))

• Proof step 7:

  r ≠ null, ∃ h0, o. h = (h0 ++ r)(r := o) ∧ ¬ r ∈ h0 ⊦ ∃ h0, o. h = h0 ∪ (∅ ++ r)(r := o) ∧ ¬ r ∈ h0

Rule argument

Additional information

Used terms: h, r

Proof step 6 from proof exin-uni (previous step) (back to tree)

Lemma exin

Proof step 7 from proof exin-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  r ≠ null, ¬ r ∈ h0 ⊦ ∃ h1, o0. (h0 ++ r)(r := o) = h1 ∪ (∅ ++ r)(r := o0) ∧ ¬ r ∈ h1

Rule argument

Additional information

Proof step 8 from proof exin-uni (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 9:

  r ≠ null, ¬ r ∈ h0 ⊦ (h0 ++ r)(r := o) = h0 ∪ (∅ ++ r)(r := o) ∧ ¬ r ∈ h0

Rule argument

Additional information

Used terms: h0, o

Proof step 9 from proof exin-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  (h0 ++ r)(r := o) ≠ h0 ∪ (∅ ++ r)(r := o), r ≠ null, ¬ r ∈ h0 ⊦

Rule argument

Additional information

Proof step 10 from proof exin-uni (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  r ≠ null, r ∈ h1, h0 ⊥ h1 ⊦ h0 ∪ h1(r := o) = (h0 ∪ h1)(r := o)

• Proof step 12:

  (h0 ++ r)(r := o) ≠ h0 ∪ (∅ ++ r)(r := o), r ≠ null, ¬ r ∈ h0 ⊦ r ≠ null ∧ r ∈ ∅ ++ r ∧ h0 ⊥ ∅ ++ r

Rule argument

Additional information

Used simplifier rules: in-emp: ⊦ ¬ r ∈ ∅; disj-r: ⊦ r ∈ h1 ∧ h0 ⊥ h1 → (r ∈ h0 ↔ false); disj-emp-r: ⊦ h ⊥ ∅; uni-alloc: r ≠ null, ¬ r ∈ h1, ¬ r ∈ h0, h0 ⊥ h1 ⊦ h0 ∪ (h1 ++ r) = (h0 ∪ h1) ++ r; uni-emp: ⊦ h0 ∪ ∅ = h0; Used terms: o, r, ∅ ++ r, h0

Proof step 11 from proof exin-uni (previous step) (back to tree)

Lemma uni-write

Proof step 12 from proof exin-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (h0 ++ r)(r := o) ≠ h0 ∪ (∅ ++ r)(r := o), r ≠ null, ¬ h0 ⊥ ∅ ++ r, ¬ r ∈ h0 ⊦

Rule argument

Additional information

Used simplifier rules: in-emp: ⊦ ¬ r ∈ ∅; in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h;

Proof step 13 from proof exin-uni (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ h0 ⊥ h1 ↔ (∀ r. ¬ r ∈ h0 ∨ ¬ r ∈ h1)

Rule argument

Additional information

Used simplifier rules: in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; in-emp: ⊦ ¬ r ∈ ∅; Used terms: ∅ ++ r, h0

Proof step 14 from proof exin-uni (previous step) (back to tree)

Lemma disj

Proof step 15 from proof exin-uni (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  r ≠ null, ¬ r ∈ h0 ∪ (∅ ++ r)(r := o), ¬ r ∈ h0 ⊦

Rule argument

Additional information

Proof step 16 from proof exin-uni (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: in-emp: ⊦ ¬ r ∈ ∅; disj-write: r ≠ null, ¬ r ∈ h1 ⊦ h0 ⊥ (h1 ++ r)(r := o) ↔ h0 ⊥ h1 ∧ ¬ r ∈ h0; disj-emp-r: ⊦ h ⊥ ∅; disj-write: r ≠ null, ¬ r ∈ h1 ⊦ h0 ⊥ (h1 ++ r)(r := o) ↔ h0 ⊥ h1 ∧ ¬ r ∈ h0; disj-emp-r: ⊦ h ⊥ ∅; in-write: ⊦ r ∈ h(r0 := o) ↔ r ∈ h; in-emp: ⊦ ¬ r ∈ ∅; in-alloc: r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; Used terms: (∅ ++ r)(r := o), h0, r

Proof step 17 from proof exin-uni (previous step) (back to tree)

Lemma in-uni