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[rs, f] ↔ (r.=>_ * hP)[rs ++ r, f]), r ≠ null, ¬ r ∈ rs ⊦

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:

  ¬(hP(mk(rs, f)) ↔ (r.=>_ * hP)(mk(rs ++ r, f))), r ≠ null, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: apply: ⊦ hP[rs, f] ↔ hP(mk(rs, f));

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ¬ r ∈ h, r ≠ null ⊦ hP(h) ↔ (r.=>_ * hP)(h ++ r)

• Proof step 5:

  hP(mk(rs, f)) ↔ (r.=>_ * hP)(mk(rs, f) ++ r), ¬(hP(mk(rs, f)) ↔ (r.=>_ * hP)(mk(rs ++ r, f))), r ≠ null, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; ⊦ r ∈ h → r ≠ null; (s) ⊦ a ∈ s → s ++ a = s; (s) Used terms: r, mk(rs, f), hP

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

A spec-lemma

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

User applied rule subst equation

And obtained the following new goals

• Proof step 6:

  ¬((r.=>_ * hP)(mk(rs, f) ++ r) ↔ (r.=>_ * hP)(mk(rs ++ r, f))), r ≠ null, ¬ r ∈ rs ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ (r.=>_ * hP)(h) ↔ (r => o1 * hP)(h(r := o1)) ∧ r ∈ h

• Proof step 8:

  ¬((r.=>_ * hP)(mk(rs, f) ++ r) ↔ (r => f(r) * hP)(mk(rs ++ r, f)(r := f(r))) ∧ r ∈ mk(rs ++ r, f)), r ≠ null, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used terms: f(r), mk(rs ++ r, f), hP, r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  r ≠ null, ¬((r.=>_ * hP)(mk(rs, f) ++ r) ↔ (r => f(r) * hP)(mk(rs ++ r, f)(r := f(r)))), ¬ r ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; ⊦ ¬ a ∈ s → (a ∈ s ++ b ↔ a = b); (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ (r.=>_ * hP)(h) ↔ (r => o1 * hP)(h(r := o1)) ∧ r ∈ h

• Proof step 11:

  r ≠ null, ¬((r => f(r) * hP)((mk(rs, f) ++ r)(r := f(r))) ∧ r ∈ mk(rs, f) ++ r ↔ (r => f(r) * hP)(mk(rs ++ r, f)(r := f(r)))), ¬ r ∈ rs ⊦

Rule argument

Additional information

Used terms: f(r), mk(rs, f) ++ r, hP, r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  r ≠ null, ¬((r => f(r) * hP)((mk(rs, f) ++ r)(r := f(r))) ↔ (r => f(r) * hP)(mk(rs ++ r, f)(r := f(r)))), ¬ r ∈ rs ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ (r => o * hP)(h) ↔ hP(h -- r) ∧ r ∈ h ∧ h(r) = o

• Proof step 14:

  ¬ ( hP((mk(rs, f) ++ r)(r := f(r)) -- r) ∧ r ∈ (mk(rs, f) ++ r)(r := f(r)) ∧ (mk(rs, f) ++ r)(r := f(r))(r) = f(r) ↔ (r => f(r) * hP)(mk(rs ++ r, f)(r := f(r)))), r ≠ null, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used terms: (mk(rs, f) ++ r)(r := f(r)), hP, f(r), r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ¬(hP(mk(rs, f)) ↔ (r => f(r) * hP)(mk(rs ++ r, f)(r := f(r)))), r ≠ null, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; r0 ≠ null, ¬ r0 ∈ h ⊦ r ∈ h ++ r0 ↔ r = r0 ∨ r ∈ h; (s) ⊦ h(r0 := o)(r) = (r = r0 ∧ r0 ∈ h ⊃ o;h(r)); (s) ⊦ r ∈ h(r0 := o) ↔ r ∈ h; (s) ¬ r ∈ h, r ≠ null ⊦ (h ++ r) -- r = h; (s) r ∈ h ⊦ h(r := o) -- r = h -- r; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ (r => o * hP)(h) ↔ hP(h -- r) ∧ r ∈ h ∧ h(r) = o

• Proof step 17:

  ¬(hP(mk(rs, f)) ↔ hP(mk(rs ++ r, f)(r := f(r)) -- r) ∧ r ∈ mk(rs ++ r, f)(r := f(r)) ∧ mk(rs ++ r, f)(r := f(r))(r) = f(r)), r ≠ null, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used terms: mk(rs ++ r, f)(r := f(r)), hP, f(r), r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  ¬(hP(mk(rs, f)) ↔ hP(mk(rs ++ r, f) -- r)), r ≠ null, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; ⊦ ¬ a ∈ s → (a ∈ s ++ b ↔ a = b); (s) ⊦ h(r0 := o)(r) = (r = r0 ∧ r0 ∈ h ⊃ o;h(r)); (s) ⊦ r ∈ h(r0 := o) ↔ r ∈ h; (s) r ∈ h ⊦ h(r := o) -- r = h -- r; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 19:

  ¬(hP(mk(rs, f)) ↔ hP(mk(rs ++ r, f) -- r)), mk(rs ++ r, f) -- r ≠ mk(rs, f), r ≠ null, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used formulas: mk(rs ++ r, f) -- r = mk(rs, f)

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. (r ∈ h0 ↔ r ∈ h1) ∧ (r ∈ h0 → h0(r) = h1(r)))

• Proof step 21:

  ¬(hP(mk(rs, f)) ↔ hP(mk(rs ++ r, f) -- r)), r ≠ null, ¬ r ∈ rs, ∃ r0. ¬((r0 ∈ mk(rs ++ r, f) -- r ↔ r0 ∈ mk(rs, f)) ∧ (r0 ∈ mk(rs ++ r, f) -- r → (mk(rs ++ r, f) -- r)(r0) = mk(rs, f)(r0))) ⊦

Rule argument

Additional information

Used terms: mk(rs, f), mk(rs ++ r, f) -- r

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:

  # rs ≠ 0, ¬(hP(mk(rs, f)) ↔ hP(mk(rs ++ r, f) -- r)), (mk(rs ++ r, f) -- r)(r0) ≠ f(r0), r ≠ null, rs ≠ ∅, r0 ∈ rs, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; at-mk: ⊦ r ∈ rs → mk(rs, f)(r) = f(r); size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ a ≠ b → (a ∈ s ++ b ↔ a ∈ s); (s) ⊦ r ∈ h -- r0 ↔ r ≠ r0 ∧ r ∈ h; (s) ⊦ a ∈ s → a ∈ s ++ b; (s)

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:

  r ∈ h ⊦ r ≠ r0 → (h -- r0)(r) = h(r)

• Proof step 24:

  # rs ≠ 0, ¬(hP(mk(rs, f)) ↔ hP(mk(rs ++ r, f) -- r)), mk(rs ++ r, f)(r0) ≠ f(r0), r ≠ null, r0 ≠ r, rs ≠ ∅, r0 ∈ rs, r0 ∈ mk(rs ++ r, f), ¬ r ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; ⊦ a ≠ b → (a ∈ s ++ b ↔ a ∈ s); (s) Used terms: r0, r, mk(rs ++ r, f)

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:

  # rs ≠ 0, ¬(hP(mk(rs, f)) ↔ hP(mk(rs ++ r, f) -- r)), mk(rs ++ r, f)(r0) ≠ f(r0), r ≠ null, r0 ≠ r, rs ≠ ∅, r0 ∈ rs, ¬ r ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; ⊦ a ≠ b → (a ∈ s ++ b ↔ a ∈ s); (s)

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

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: at-mk: ⊦ r ∈ rs → mk(rs, f)(r) = f(r); ⊦ a ≠ b → (a ∈ s ++ b ↔ a ∈ s); (s) Used formulas: r0 ∈ rs ++ r