Proof step 1 from proof map-unique (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  f(r) = o, o ≠ o0, (a[r => o0] * hR)[rs, f, g] ⊦

Rule argument

Additional information

Proof step 2 from proof map-unique (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  f(r) ≠ o0, (a[r => o0] * hR)[rs, f, g] ⊦

Rule argument

Additional information

Proof step 3 from proof map-unique (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ (hR0 * hR1)[rs, f, g] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hR0[rs0, f, g] ∧ hR1[rs1, f, g])

• Proof step 5:

  f(r) ≠ o0, ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ a[r => o0][rs0, f, g] ∧ hR[rs1, f, g] ⊦

Rule argument

Additional information

Used terms: rs, hR, g, a[r => o0], f

Proof step 4 from proof map-unique (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof map-unique (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  rs0 ∩ rs1 = ∅, f(r) ≠ o0, a[r => o0][rs0, f, g], hR[rs1, f, g] ⊦

Rule argument

Additional information

Proof step 6 from proof map-unique (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ hR[rs, f, g] ↔ hR(mk(rs, f, g))

• Proof step 8:

  rs0 ∩ rs1 = ∅, f(r) ≠ o0, hR[rs1, f, g], a[r => o0](mk(rs0, f, g)) ⊦

Rule argument

Additional information

Used terms: g, f, rs0, a[r => o0]

Proof step 7 from proof map-unique (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof map-unique (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ a[hP](mk(rs, f, g)) ↔ hP(mk(rs, f)) ∧ (∀ r. r ∈ rs → g(r) = a)

• Proof step 10:

  rs0 ∩ rs1 = ∅, f(r) ≠ o0, ((r => o0))(mk(rs0, f)), hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: a, r => o0, rs0, g, f

Proof step 9 from proof map-unique (previous step) (back to tree)

Lemma lift-aux

Proof step 10 from proof map-unique (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  rs0 ∩ rs1 = ∅, f(r) ≠ o0, ((r => o0))(mk(rs0, f)), hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Proof step 11 from proof map-unique (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ ((r => o))(h) ↔ h = (∅ ++ r)[r, o] ∧ r ≠ null

• Proof step 13:

  mk(rs0, f) = (∅ ++ r)[r, o0], rs0 ∩ rs1 = ∅, f(r) ≠ o0, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: mk(rs0, f), o0, r

Proof step 12 from proof map-unique (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof map-unique (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  mk(rs0, f) = (∅ ++ r)[r, o0], rs0 ∩ rs1 = ∅, f(r) ≠ o0, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Proof step 14 from proof map-unique (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  rs0 ∩ rs1 = ∅, f(r) ≠ o0, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ mk(rs0, f) ↔ r0 ∈ (∅ ++ r)[r, o0]) ∧ (r0 ∈ mk(rs0, f) → mk(rs0, f)[r0] = (∅ ++ r)[r, o0][r0]) ⊦

Rule argument

Additional information

Used terms: (∅ ++ r)[r, o0], mk(rs0, f)

Proof step 15 from proof map-unique (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof map-unique (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  rs0 ∩ rs1 = ∅, f(r) ≠ o0, r ≠ null, hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o0;(∅ ++ r)[r0])) ⊦

Rule argument

Additional information

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

Proof step 17 from proof map-unique (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r