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; 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 =>_ * hP))(mk(rs, f) ++ r) ↔ ((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; ⊦ ¬ 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 => 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 ≠ null, ¬ 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 => f(r) * hP))((mk(rs, 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 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:

  mk(rs ++ r, f) -- r ≠ mk(rs, f), ¬(hP(mk(rs, f)) ↔ hP(mk(rs ++ r, f) -- r)), 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:

  ¬(hP(mk(rs, f)) ↔ hP(mk(rs ++ r, f) -- r)), (mk(rs ++ r, f) -- r)[r0] ≠ f(r0), r ≠ null, 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); ⊦ 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:

  ¬(hP(mk(rs, f)) ↔ hP(mk(rs ++ r, f) -- r)), mk(rs ++ r, f)[r0] ≠ f(r0), r ≠ null, r0 ≠ r, 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:

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

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; ⊦ a ∈ s → a ∈ s ++ b; (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 ∈ s → a ∈ s ++ b; (s) Used formulas: r0 ∈ rs ++ r