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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬((a0[r => o] * hR)[rs, f, g] ↔ (a1[r => o] * hR)[rs, f, g(r; a1)] ∧ g(r) = a0) ⊦

Rule argument

Additional information

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

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  (a0[r => o] * hR)[rs, f, g] ⊦ (a1[r => o] * hR)[rs, f, g(r; a1)] ∧ g(r) = a0

• Proof step 47:

  g(r) = a0, (a1[r => o] * hR)[rs, f, g(r; a1)], ¬ (a0[r => o] * hR)[rs, f, g] ⊦

Rule argument

Additional information

Proof step 3 from proof aux-known (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:

  ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ a0[r => o][rs0, f, g] ∧ hR[rs1, f, g] ⊦ (a1[r => o] * hR)[rs, f, g(r; a1)] ∧ g(r) = a0

Rule argument

Additional information

Used terms: rs, hR, g, a0[r => o], f

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  rs0 ∩ rs1 = ∅, a0[r => o][rs0, f, g], hR[rs1, f, g] ⊦ (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a0[r => o][rs0, f, g] ⊦ (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0, a1[r => o][rs0, f, g(r; a1)] ∧ hR[rs1, f, g(r; a1)] ∧ rs0 ∩ rs1 = ∅

• Proof step 32:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a0[r => o][rs0, f, g], a1[r => o][rs0, f, g(r; a1)], hR[rs1, f, g(r; a1)] ⊦ true ∧ g(r) = a0

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  rs0 ∩ rs1 = ∅, a0[r => o][rs0, f, g], hR[rs1, f, g] ⊦ (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0, a1[r => o][rs0, f, g(r; a1)] ∧ hR[rs1, f, g(r; a1)]

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a0[r => o](mk(rs0, f, g)) ⊦ a1[r => o][rs0, f, g(r; a1)] ∧ hR[rs1, f, g(r; a1)], (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0

Rule argument

Additional information

Used terms: g, f, rs0, a0[r => o]

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  rs0 ∩ rs1 = ∅, a0[r => o](mk(rs0, f, g)), hR[rs1, f, g] ⊦ (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0, a1[r => o](mk(rs0, f, g(r; a1))) ∧ hR[rs1, f, g(r; a1)]

Rule argument

Additional information

Used terms: g(r; a1), f, rs0, a1[r => o]

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

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

• Proof step 15:

  rs0 ∩ rs1 = ∅, hR[rs1, f, g], a0[r => o](mk(rs0, f, g)) ⊦ (((r => o))(mk(rs0, f)) ∧ (∀ r0. r0 ∈ rs0 → g(r; a1)(r0) = a1)) ∧ hR[rs1, f, g(r; a1)], (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0

Rule argument

Additional information

Used terms: a1, r => o, rs0, g(r; a1), f

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  rs0 ∩ rs1 = ∅, a0[r => o](mk(rs0, f, g)), hR[rs1, f, g] ⊦ (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0, ((r => o))(mk(rs0, f)) ∧ (r0 ∈ rs0 → (r = r0 ⊃ a1;g(r0)) = a1) ∧ hR[rs1, f, g(r; a1)]

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

• Proof step 18:

  rs0 ∩ rs1 = ∅, ((r => o))(mk(rs0, f)), hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a0 ⊦ ((r => o))(mk(rs0, f)) ∧ (r0 ∈ rs0 → (r = r0 ⊃ a1;g(r0)) = a1) ∧ hR[rs1, f, g(r; a1)], (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0

Rule argument

Additional information

Used terms: a0, r => o, rs0, g, f

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  rs0 ∩ rs1 = ∅, ((r => o))(mk(rs0, f)), hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a0 ⊦ (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0, (r0 ∈ rs0 → (r = r0 ⊃ a1;g(r0)) = a1) ∧ hR[rs1, f, g(r; a1)]

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 20:

  rs0 ∩ rs1 = ∅, ((r => o))(mk(rs0, f)), hR[rs1, f, g], r0 ∈ rs0 → g(r0) = a0, ∀ r. r ∈ rs0 → g(r) = a0 ⊦ (r0 ∈ rs0 → (r = r0 ⊃ a1;g(r0)) = a1) ∧ hR[rs1, f, g(r; a1)], (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0

Rule argument

Additional information

Used terms: r0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], r0 ∈ rs0 → g(r0) = a0, ∀ r. r ∈ rs0 → g(r) = a0 ⊦ (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0, (r0 ∈ rs0 → (r = r0 ⊃ a1;g(r0)) = a1) ∧ hR[rs1, f, g(r; a1)]

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  mk(rs0, f) = (∅ ++ r)[r, o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, f, g], r0 ∈ rs0 → g(r0) = a0, ∀ r. r ∈ rs0 → g(r) = a0 ⊦ (r0 ∈ rs0 → (r = r0 ⊃ a1;g(r0)) = a1) ∧ hR[rs1, f, g(r; a1)], (a1[r => o] * hR)[rs0 ∪ rs1, f, g(r; a1)] ∧ g(r) = a0

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

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

User applied rule all left

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

Used terms: r0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

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

Rule argument

Additional information

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

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

Lemma switch-aux

Proof step 30 from proof aux-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

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

Proof step 31 from proof aux-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 32 from proof aux-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  rs0 ∩ rs1 = ∅, g(r) ≠ a0, hR[rs1, f, g(r; a1)], a1[r => o][rs0, f, g(r; a1)], a0[r => o][rs0, f, g], hR[rs1, f, g] ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

• Proof step 35:

  rs0 ∩ rs1 = ∅, g(r) ≠ a0, hR[rs1, f, g], a0[r => o](mk(rs0, f, g)), a1[r => o][rs0, f, g(r; a1)], hR[rs1, f, g(r; a1)] ⊦

Rule argument

Additional information

Used terms: g, f, rs0, a0[r => o]

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

A spec-lemma

Proof step 35 from proof aux-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

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

• Proof step 37:

  rs0 ∩ rs1 = ∅, g(r) ≠ a0, ((r => o))(mk(rs0, f)), hR[rs1, f, g(r; a1)], a1[r => o][rs0, f, g(r; a1)], hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a0 ⊦

Rule argument

Additional information

Used terms: a0, r => o, rs0, g, f

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  rs0 ∩ rs1 = ∅, g(r) ≠ a0, ((r => o))(mk(rs0, f)), hR[rs1, f, g], a1[r => o][rs0, f, g(r; a1)], hR[rs1, f, g(r; a1)], ∀ r. r ∈ rs0 → g(r) = a0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

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

• Proof step 40:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

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

• Proof step 43:

  rs0 ∩ rs1 = ∅, g(r) ≠ a0, r ≠ null, hR[rs1, f, g(r; a1)], a1[r => o][rs0, f, g(r; a1)], hR[rs1, f, g], ∀ r. r ∈ rs0 → g(r) = a0, ∀ r0. (r0 ∈ mk(rs0, f) ↔ r0 ∈ (∅ ++ r)[r, o]) ∧ (r0 ∈ mk(rs0, f) → mk(rs0, f)[r0] = (∅ ++ r)[r, o][r0]) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  rs0 ∩ rs1 = ∅, g(r) ≠ a0, r ≠ null, hR[rs1, f, g], a1[r => o][rs0, f, g(r; a1)], hR[rs1, f, g(r; a1)], ∀ r. r ∈ rs0 → g(r) = a0, ∀ r0. (r0 ∈ rs0 → r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ 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 44 from proof aux-known (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 45:

  rs0 ∩ rs1 = ∅, g(r) ≠ a0, r ≠ null, hR[rs1, f, g(r; a1)], a1[r => o][rs0, f, g(r; a1)], hR[rs1, f, g], r ∈ rs0 → r = r, r ∈ rs0 → f(r) = (r = r ⊃ o;(∅ ++ r)[r]), ∀ r0. (r0 ∈ rs0 → r0 = r) ∧ (r0 ∈ rs0 → f(r0) = (r0 = r ⊃ o;(∅ ++ r)[r0])), ∀ r. r ∈ rs0 → g(r) = a0 ⊦

Rule argument

Additional information

Used terms: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

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

Rule argument

Additional information

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

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

Heuristic quantifier closing 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 47 from proof aux-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

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

Rule argument

Additional information

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

Proof step 49 from proof aux-known (previous step) (back to tree)

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

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

• Proof step 53:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

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

• Proof step 56:

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

• Proof step 69:

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

Rule argument

Additional information

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

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

Lemma switch-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

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

• Proof step 59:

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

Rule argument

Additional information

Used terms: g(r; a1), f, rs0, a1[r => o]

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 60:

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

• Proof step 61:

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

Rule argument

Additional information

Used terms: a1, r => o, rs0, g(r; a1), f

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

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

• Proof step 64:

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

Rule argument

Additional information

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

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

A spec-lemma

Proof step 64 from proof aux-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

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

• Proof step 67:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 71:

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

• Proof step 72:

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

Rule argument

Additional information

Used terms: g(r; a1), f, rs0, a1[r => o]

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 73:

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

• Proof step 74:

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

Rule argument

Additional information

Used terms: a1, r => o, rs0, g(r; a1), f

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

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

Rule argument

Additional information

Proof step 75 from proof aux-known (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

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

• Proof step 77:

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

Rule argument

Additional information

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

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

A spec-lemma

Proof step 77 from proof aux-known (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 79:

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

• Proof step 80:

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

Rule argument

Additional information

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

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 81:

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

• Proof step 82:

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

Rule argument

Additional information

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

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

Lemma lift-aux

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 84:

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

• Proof step 85:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

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

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

User applied rule all left

And obtained the following new goals

• Proof step 87:

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

Rule argument

Additional information

Used terms: r

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 88:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 89:

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

• Proof step 90:

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 91:

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

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r0