Proof step 1 from proof precise-mapornull (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬ precise(r =>?) ⊦

Rule argument

Additional information

Proof step 2 from proof precise-mapornull (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬ precise((r = null ⊃ emp;_∃(λ o. r => o))) ⊦

Rule argument

Additional information

Used simplifier rules: mapornull: ⊦ r =>? = (r = null ⊃ emp;r =>_); mapex: ⊦ r =>_ = _∃(λ o. r => o);

Proof step 3 from proof precise-mapornull (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  r ≠ null, ¬ precise(_∃(λ o. r => o)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ precise(emp); (s)

Proof step 4 from proof precise-mapornull (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ precise(hP) ↔ (∀ h, h0, h1, h2. hP(h) ∧ hP(h0) ∧ h ⊥ h1 ∧ h0 ⊥ h2 ∧ h ∪ h1 = h0 ∪ h2 → h = h0)

• Proof step 6:

  r ≠ null, ∃ h, h0, h1, h2. ¬((_∃(λ o. r => o))(h) ∧ (_∃(λ o. r => o))(h0) ∧ h ⊥ h1 ∧ h0 ⊥ h2 ∧ h ∪ h1 = h0 ∪ h2 → h = h0) ⊦

Rule argument

Additional information

Used terms: _∃(λ o. r => o)

Proof step 5 from proof precise-mapornull (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof precise-mapornull (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

Proof step 7 from proof precise-mapornull (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

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

Rule argument

Additional information

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

Proof step 8 from proof precise-mapornull (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof precise-mapornull (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Proof step 10 from proof precise-mapornull (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  r ∈ (∅ ++ r)[r, o] ∪ h1 ↔ r ∈ (∅ ++ r)[r, o0] ∪ h2, (∅ ++ r)[r, o] ≠ (∅ ++ r)[r, o0], r ≠ null, ¬ r ∈ h2, ¬ r ∈ h1, r ∈ (∅ ++ r)[r, o] ∪ h1 → ((∅ ++ r)[r, o] ∪ h1)[r] = ((∅ ++ r)[r, o0] ∪ h2)[r] ⊦

Rule argument

Additional information

Used terms: r

Proof step 11 from proof precise-mapornull (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  (∅ ++ r)[r, o] ≠ (∅ ++ r)[r, o0], r ≠ null, ¬ r ∈ h2, ¬ r ∈ h1, ¬ r ∈ (∅ ++ r)[r, o] ∪ h1, ¬ r ∈ (∅ ++ r)[r, o0] ∪ h2 ⊦

Rule argument

Additional information

Used simplifier rules: r ≠ null, ¬ r ∈ h ⊦ ((∅ ++ r)[r, o] ∪ h)[r] = o; (s)

Proof step 12 from proof precise-mapornull (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

Proof step 13 from proof precise-mapornull (previous step) (back to tree)

A spec-lemma