Proof step 1 from proof write-known (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬((a[r => o0] * hR)[rs, f, g] ↔ (a[r => o1] * hR)[rs, f(r; o1), g] ∧ f(r) = o0) ⊦

Rule argument

Additional information

Proof step 2 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬((a[r => o0] * hR)[rs, f, g] ↔ (a[r => o1] * hR)[rs, f(r; o1), g] ∧ f(r) = o0) ⊦

Rule argument

Additional information

Proof step 3 from proof write-known (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

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

• Proof step 78:

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

Rule argument

Additional information

Proof step 4 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

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

Rule argument

Additional information

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

Proof step 5 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  rs0 ∩ rs1 = ∅, a[r => o0][rs0, f, g], hR[rs1, f, g] ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

Rule argument

Additional information

Proof step 7 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ hR0[rs0, f, g] ∧ hR1[rs1, f, g] ∧ rs0 ∩ rs1 = ∅ → (hR0 * hR1)[rs0 ∪ rs1, f, g]

• Proof step 9:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r => o0][rs0, f, g] ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0, a[r => o1][rs0, f(r; o1), g] ∧ hR[rs1, f(r; o1), g] ∧ rs0 ∩ rs1 = ∅

• Proof step 65:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r => o0][rs0, f, g], a[r => o1][rs0, f(r; o1), g], hR[rs1, f(r; o1), g] ⊦ true ∧ f(r) = o0

Rule argument

Additional information

Used terms: rs0, hR, g, a[r => o1], f(r; o1), rs1

Proof step 8 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  rs0 ∩ rs1 = ∅, a[r => o0][rs0, f, g], hR[rs1, f, g] ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0, a[r => o1][rs0, f(r; o1), g] ∧ hR[rs1, f(r; o1), g]

Rule argument

Additional information

Proof step 10 from proof write-known (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r => o0][rs0, f, g], ¬ a[r => o1][rs0, f(r; o1), g] ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

• Proof step 50:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r => o0][rs0, f, g], ¬ hR[rs1, f(r; o1), g] ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

Rule argument

Additional information

Proof step 11 from proof write-known (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

  rs0 ∩ rs1 = ∅, a[r => o0][rs0, f, g], hR[rs1, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g], ¬ a[r => o1][rs0, f(r; o1), g] ⊦

• Proof step 38:

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

Rule argument

Additional information

Proof step 12 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

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

• Proof step 14:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r => o0][rs0, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g], ¬ a[r => o1](mk(rs0, f(r; o1), g)) ⊦

Rule argument

Additional information

Used terms: g, f(r; o1), rs0, a[r => o1]

Proof step 13 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  rs0 ∩ rs1 = ∅, a[r => o0][rs0, f, g], hR[rs1, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g], ¬ ((r => o1))(mk(rs0, f(r; o1))) ∨ (∃ r. ¬(r ∈ rs0 → g(r) = a)) ⊦

Rule argument

Additional information

Used terms: a, r => o1, rs0, g, f(r; o1)

Proof step 15 from proof write-known (previous step) (back to tree)

Lemma lift-aux

Proof step 16 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r => o0][rs0, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g], ¬ ((r => o1))(mk(rs0, f(r; o1))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

Rule argument

Additional information

Proof step 17 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  rs0 ∩ rs1 = ∅, a[r => o0](mk(rs0, f, g)), hR[rs1, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g], ¬ ((r => o1))(mk(rs0, f(r; o1))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

Rule argument

Additional information

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

Proof step 18 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 19 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  rs0 ∩ rs1 = ∅, ((r => o0))(mk(rs0, f)), hR[rs1, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g], ∀ r. r ∈ rs0 → g(r) = a, ¬ ((r => o1))(mk(rs0, f(r; o1))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

Rule argument

Additional information

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

Proof step 20 from proof write-known (previous step) (back to tree)

Lemma lift-aux

Proof step 21 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  rs0 ∩ rs1 = ∅, ((r => o0))(mk(rs0, f)), hR[rs1, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g], ∀ r. r ∈ rs0 → g(r) = a, ¬ ((r => o1))(mk(rs0, f(r; o1))) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

Rule argument

Additional information

Proof step 22 from proof write-known (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 23:

  rs0 ∩ rs1 = ∅, ((r => o0))(mk(rs0, f)), hR[rs1, f, g], ¬ ((r => o1))(mk(rs0, f(r; o1))), ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g], ∀ r. r ∈ rs0 → g(r) = a ⊦

• Proof step 36:

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

Rule argument

Additional information

Proof step 23 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

  rs0 ∩ rs1 = ∅, ((r => o0))(mk(rs0, f)), hR[rs1, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g], ∀ r. r ∈ rs0 → g(r) = a, mk(rs0, f(r; o1)) ≠ (∅ ++ r)[r, o1] ∨ r = null ⊦

Rule argument

Additional information

Used terms: mk(rs0, f(r; o1)), o1, r

Proof step 24 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ false(h); (s) ⊦ ⌜false⌝ = false; (s) ⊦ null => o = ⌜false⌝ ; (s)

Proof step 26 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

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

Rule argument

Additional information

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

Proof step 27 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Proof step 29 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

• Proof step 31:

  rs0 ∩ rs1 = ∅, mk(rs0, f(r; o1)) ≠ (∅ ++ r)[r, o1], r ≠ null, hR[rs1, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), 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 30 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 31 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  rs0 ∩ rs1 = ∅, mk(rs0, f(r; o1)) ≠ (∅ ++ r)[r, o1], r ≠ null, hR[rs1, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), 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 32 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 33:

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

• Proof step 34:

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

Rule argument

Additional information

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

Proof step 33 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 34 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g], ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o0;(∅ ++ r)[r0])) ⊦ (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → (r = r0 ⊃ o1;f(r0)) = (r0 = r ⊃ o1;(∅ ++ 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 35 from proof write-known (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0

Proof step 36 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

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

Rule argument

Additional information

Proof step 37 from proof write-known (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0

Proof step 38 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

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

• Proof step 40:

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

Rule argument

Additional information

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

Proof step 39 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 40 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

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

• Proof step 42:

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

Rule argument

Additional information

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

Proof step 41 from proof write-known (previous step) (back to tree)

Lemma lift-aux

Proof step 42 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

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

Rule argument

Additional information

Proof step 43 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

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

• Proof step 45:

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

Rule argument

Additional information

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

Proof step 44 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

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

Rule argument

Additional information

Proof step 46 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 47:

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

• Proof step 48:

  rs0 ∩ rs1 = ∅, f(r) ≠ o0, r ≠ null, hR[rs1, f, g], ¬ a[r => o1][rs0, f(r; o1), 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 47 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 48 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 49:

  rs0 ∩ rs1 = ∅, f(r) ≠ o0, r ≠ null, hR[rs1, f, g], ¬ a[r => o1][rs0, f(r; o1), 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 49 from proof write-known (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 50 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 51:

  ⊦ ¬ r ∈ rs → (hR[rs, f(r; o), g] ↔ hR[rs, f, g])

• Proof step 52:

  rs0 ∩ rs1 = ∅, a[r => o0][rs0, f, g], hR[rs1, f, g], r ∈ rs1, ¬ hR[rs1, f(r; o1), g] ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

Rule argument

Additional information

Used terms: hR, r, rs1, g, f, o1

Proof step 51 from proof write-known (previous step) (back to tree)

Lemma switch-obj

Proof step 52 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r => o0][rs0, f, g], r ∈ rs1, ¬ hR[rs1, f(r; o1), g] ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

Rule argument

Additional information

Proof step 53 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 54:

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

• Proof step 55:

  rs0 ∩ rs1 = ∅, a[r => o0](mk(rs0, f, g)), hR[rs1, f, g], r ∈ rs1, ¬ hR[rs1, f(r; o1), g] ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

Rule argument

Additional information

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

Proof step 54 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 55 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

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

• Proof step 57:

  rs0 ∩ rs1 = ∅, ((r => o0))(mk(rs0, f)), hR[rs1, f, g], r ∈ rs1, ¬ hR[rs1, f(r; o1), g], ∀ r. r ∈ rs0 → g(r) = a ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

Rule argument

Additional information

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

Proof step 56 from proof write-known (previous step) (back to tree)

Lemma lift-aux

Proof step 57 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  rs0 ∩ rs1 = ∅, ((r => o0))(mk(rs0, f)), hR[rs1, f, g], r ∈ rs1, ¬ hR[rs1, f(r; o1), g], ∀ r. r ∈ rs0 → g(r) = a ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

Rule argument

Additional information

Proof step 58 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 59:

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

• Proof step 60:

  mk(rs0, f) = (∅ ++ r)[r, o0], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], r ∈ rs1, ¬ hR[rs1, f(r; o1), g], ∀ r. r ∈ rs0 → g(r) = a ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

Rule argument

Additional information

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

Proof step 59 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 60 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  mk(rs0, f) = (∅ ++ r)[r, o0], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], r ∈ rs1, ¬ hR[rs1, f(r; o1), g], ∀ r. r ∈ rs0 → g(r) = a ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

Rule argument

Additional information

Proof step 61 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 62:

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

• Proof step 63:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], r ∈ rs1, ¬ hR[rs1, f(r; o1), 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]) ⊦ (a[r => o1] * hR)[rs0 ∪ rs1, f(r; o1), g] ∧ f(r) = o0

Rule argument

Additional information

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

Proof step 62 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 63 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

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

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 64 from proof write-known (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: int-a: ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1; from specification set-union[refset] int-c: ⊦ s ∩ s0 = s0 ∩ s; from specification set-union[refset] ⊦ s ∩ s0 = ∅ ∧ a ∈ s → (a ∈ s0 ↔ false); (as) Used terms: r

Proof step 65 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

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

Rule argument

Additional information

Proof step 66 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 67:

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

• Proof step 68:

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

Rule argument

Additional information

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

Proof step 67 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 68 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

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

• Proof step 70:

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

Rule argument

Additional information

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

Proof step 69 from proof write-known (previous step) (back to tree)

Lemma lift-aux

Proof step 70 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

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

Rule argument

Additional information

Proof step 71 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

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

• Proof step 73:

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

Rule argument

Additional information

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

Proof step 72 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 73 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

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

Rule argument

Additional information

Proof step 74 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

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

• Proof step 76:

  rs0 ∩ rs1 = ∅, f(r) ≠ o0, r ≠ null, hR[rs1, f(r; o1), g], a[r => o1][rs0, f(r; o1), g], 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 75 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 76 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  rs0 ∩ rs1 = ∅, f(r) ≠ o0, r ≠ null, hR[rs1, f, g], a[r => o1][rs0, f(r; o1), g], hR[rs1, f(r; o1), 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: map-in0: ⊦ a[r => o][rs, f, g] → r ∈ rs; 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 77 from proof write-known (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: map-in0: ⊦ a[r => o][rs, f, g] → r ∈ rs; Used terms: r

Proof step 78 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  (a[r => o1] * hR)[rs, f(r; o1), g], ¬ (a[r => f(r)] * hR)[rs, f, g] ⊦

Rule argument

Additional information

Proof step 79 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 80:

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

• Proof step 81:

  ¬ (a[r => f(r)] * hR)[rs, f, g], ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ a[r => o1][rs0, f(r; o1), g] ∧ hR[rs1, f(r; o1), g] ⊦

Rule argument

Additional information

Used terms: rs, hR, g, a[r => o1], f(r; o1)

Proof step 80 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 81 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 82:

  rs0 ∩ rs1 = ∅, a[r => o1][rs0, f(r; o1), g], hR[rs1, f(r; o1), g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g] ⊦

Rule argument

Additional information

Proof step 82 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 83:

  ⊦ hR0[rs0, f, g] ∧ hR1[rs1, f, g] ∧ rs0 ∩ rs1 = ∅ → (hR0 * hR1)[rs0 ∪ rs1, f, g]

• Proof step 84:

  rs0 ∩ rs1 = ∅, hR[rs1, f(r; o1), g], a[r => o1][rs0, f(r; o1), g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g] ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g] ∧ rs0 ∩ rs1 = ∅

Rule argument

Additional information

Used terms: rs0, hR, g, a[r => f(r)], f, rs1

Proof step 83 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 84 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 85:

  rs0 ∩ rs1 = ∅, a[r => o1][rs0, f(r; o1), g], hR[rs1, f(r; o1), g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g] ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g]

Rule argument

Additional information

Proof step 85 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 86:

  ⊦ ¬ r ∈ rs → (hR[rs, f(r; o), g] ↔ hR[rs, f, g])

• Proof step 87:

  rs0 ∩ rs1 = ∅, hR[rs1, f(r; o1), g], a[r => o1][rs0, f(r; o1), g], r ∈ rs1, ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g] ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g]

• Proof step 100:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r => o1][rs0, f(r; o1), g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1 ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g]

Rule argument

Additional information

Used terms: hR, r, rs1, g, f, o1

Proof step 86 from proof write-known (previous step) (back to tree)

Lemma switch-obj

Proof step 87 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 88:

  rs0 ∩ rs1 = ∅, a[r => o1][rs0, f(r; o1), g], hR[rs1, f(r; o1), g], r ∈ rs1, ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g] ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g]

Rule argument

Additional information

Proof step 88 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 89:

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

• Proof step 90:

  rs0 ∩ rs1 = ∅, hR[rs1, f(r; o1), g], a[r => o1](mk(rs0, f(r; o1), g)), r ∈ rs1, ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g] ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g]

Rule argument

Additional information

Used terms: g, f(r; o1), rs0, a[r => o1]

Proof step 89 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 90 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 91:

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

• Proof step 92:

  rs0 ∩ rs1 = ∅, ((r => o1))(mk(rs0, f(r; o1))), hR[rs1, f(r; o1), g], r ∈ rs1, ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g]

Rule argument

Additional information

Used terms: a, r => o1, rs0, g, f(r; o1)

Proof step 91 from proof write-known (previous step) (back to tree)

Lemma lift-aux

Proof step 92 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 93:

  rs0 ∩ rs1 = ∅, ((r => o1))(mk(rs0, f(r; o1))), hR[rs1, f(r; o1), g], r ∈ rs1, ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g]

Rule argument

Additional information

Proof step 93 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 94:

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

• Proof step 95:

  mk(rs0, f(r; o1)) = (∅ ++ r)[r, o1], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f(r; o1), g], r ∈ rs1, ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g]

Rule argument

Additional information

Used terms: mk(rs0, f(r; o1)), o1, r

Proof step 94 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 95 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 96:

  mk(rs0, f(r; o1)) = (∅ ++ r)[r, o1], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f(r; o1), g], r ∈ rs1, ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g]

Rule argument

Additional information

Proof step 96 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 97:

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

• Proof step 98:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f(r; o1), g], r ∈ rs1, ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ mk(rs0, f(r; o1)) ↔ r0 ∈ (∅ ++ r)[r, o1]) ∧ (r0 ∈ mk(rs0, f(r; o1)) → mk(rs0, f(r; o1))[r0] = (∅ ++ r)[r, o1][r0]) ⊦ a[r => f(r)][rs0, f, g] ∧ hR[rs1, f, g]

Rule argument

Additional information

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

Proof step 97 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 98 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 99:

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

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 99 from proof write-known (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: int-a: ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1; from specification set-union[refset] int-c: ⊦ s ∩ s0 = s0 ∩ s; from specification set-union[refset] ⊦ s ∩ s0 = ∅ ∧ a ∈ s → (a ∈ s0 ↔ false); (as) Used terms: r

Proof step 100 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 101:

  rs0 ∩ rs1 = ∅, a[r => o1][rs0, f(r; o1), g], hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ a[r => f(r)][rs0, f, g], ¬ r ∈ rs1 ⊦

Rule argument

Additional information

Proof step 101 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 102:

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

• Proof step 103:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a[r => o1][rs0, f(r; o1), g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ a[r => f(r)](mk(rs0, f, g)), ¬ r ∈ rs1 ⊦

Rule argument

Additional information

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

Proof step 102 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 103 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 104:

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

• Proof step 105:

  rs0 ∩ rs1 = ∅, a[r => o1](mk(rs0, f(r; o1), g)), hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ a[r => f(r)](mk(rs0, f, g)), ¬ r ∈ rs1 ⊦

Rule argument

Additional information

Used terms: g, f(r; o1), rs0, a[r => o1]

Proof step 104 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 105 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 106:

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

• Proof step 107:

  rs0 ∩ rs1 = ∅, ((r => o1))(mk(rs0, f(r; o1))), hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ a[r => f(r)](mk(rs0, f, g)), ¬ r ∈ rs1, ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used terms: a, r => o1, rs0, g, f(r; o1)

Proof step 106 from proof write-known (previous step) (back to tree)

Lemma lift-aux

Proof step 107 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 108:

  rs0 ∩ rs1 = ∅, ((r => o1))(mk(rs0, f(r; o1))), hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ a[r => f(r)](mk(rs0, f, g)), ¬ r ∈ rs1, ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Proof step 108 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 109:

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

• Proof step 110:

  rs0 ∩ rs1 = ∅, ((r => o1))(mk(rs0, f(r; o1))), hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r. r ∈ rs0 → g(r) = a, ¬ ((r => f(r)))(mk(rs0, f)) ∨ (∃ r. ¬(r ∈ rs0 → g(r) = a)) ⊦

Rule argument

Additional information

Used terms: a, r => f(r), rs0, g, f

Proof step 109 from proof write-known (previous step) (back to tree)

Lemma lift-aux

Proof step 110 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 111:

  rs0 ∩ rs1 = ∅, ((r => o1))(mk(rs0, f(r; o1))), hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r. r ∈ rs0 → g(r) = a, ¬ ((r => f(r)))(mk(rs0, f)) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

Rule argument

Additional information

Proof step 111 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 112:

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

• Proof step 113:

  mk(rs0, f(r; o1)) = (∅ ++ r)[r, o1], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r. r ∈ rs0 → g(r) = a, ¬ ((r => f(r)))(mk(rs0, f)) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

Rule argument

Additional information

Used terms: mk(rs0, f(r; o1)), o1, r

Proof step 112 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 113 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 114:

  mk(rs0, f(r; o1)) = (∅ ++ r)[r, o1], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r. r ∈ rs0 → g(r) = a, ¬ ((r => f(r)))(mk(rs0, f)) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

Rule argument

Additional information

Proof step 114 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 115:

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

• Proof step 116:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r. r ∈ rs0 → g(r) = a, ∀ r0. (r0 ∈ mk(rs0, f(r; o1)) ↔ r0 ∈ (∅ ++ r)[r, o1]) ∧ (r0 ∈ mk(rs0, f(r; o1)) → mk(rs0, f(r; o1))[r0] = (∅ ++ r)[r, o1][r0]), ¬ ((r => f(r)))(mk(rs0, f)) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

Rule argument

Additional information

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

Proof step 115 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 116 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 117:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r. r ∈ rs0 → g(r) = a, ∀ r1. (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → (r = r1 ⊃ o1;f(r1)) = (r1 = r ⊃ o1;(∅ ++ r)[r1])), ¬ ((r => f(r)))(mk(rs0, f)) ∨ ¬(r0 ∈ rs0 → g(r0) = a) ⊦

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 117 from proof write-known (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 118:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ ((r => f(r)))(mk(rs0, f)), ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r1. (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → (r = r1 ⊃ o1;f(r1)) = (r1 = r ⊃ o1;(∅ ++ r)[r1])), ∀ r. r ∈ rs0 → g(r) = a ⊦

• Proof step 123:

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

Rule argument

Additional information

Proof step 118 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 119:

  rs0 ∩ rs1 = ∅, mk(rs0, f) ≠ (∅ ++ r)[r, f(r)], r ≠ null, hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r. r ∈ rs0 → g(r) = a, ∀ r1. (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → (r = r1 ⊃ o1;f(r1)) = (r1 = r ⊃ o1;(∅ ++ r)[r1])) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ((r => o))(h) ↔ r ≠ null ∧ h = (∅ ++ r)[r, o]; (ss)

Proof step 119 from proof write-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 120:

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

• Proof step 121:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r1. (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → (r = r1 ⊃ o1;f(r1)) = (r1 = r ⊃ o1;(∅ ++ r)[r1])), ∀ r. r ∈ rs0 → g(r) = a, ∃ r0. ¬((r0 ∈ mk(rs0, f) ↔ r0 ∈ (∅ ++ r)[r, f(r)]) ∧ (r0 ∈ mk(rs0, f) → mk(rs0, f)[r0] = (∅ ++ r)[r, f(r)][r0])) ⊦

Rule argument

Additional information

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

Proof step 120 from proof write-known (previous step) (back to tree)

A spec-lemma

Proof step 121 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 122:

  rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r. r ∈ rs0 → g(r) = a, ∀ r1. (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → (r = r1 ⊃ o1;f(r1)) = (r1 = r ⊃ o1;(∅ ++ r)[r1])) ⊦ (r0 ∈ rs0 ↔ r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ f(r);(∅ ++ 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 122 from proof write-known (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0

Proof step 123 from proof write-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 124:

  rs0 ∩ rs1 = ∅, # rs0 ≠ 0, g(r0) ≠ a, r ≠ null, rs0 ≠ ∅, hR[rs1, f, g], r0 ∈ rs0, ¬ (a[r => f(r)] * hR)[rs0 ∪ rs1, f, g], ¬ r ∈ rs1, ∀ r1. (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → (r = r1 ⊃ o1;f(r1)) = (r1 = r ⊃ o1;(∅ ++ r)[r1])), ∀ r. r ∈ rs0 → g(r) = a ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic[refset] ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic[refset]

Proof step 124 from proof write-known (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0