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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  cf(r) = a × r0, ¬((o[r =>_] * hR)[rs, cf, af] ↔ (o[r => a × r0] * hR)[rs, cf, af]) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  cf(r) = a × r0, ¬((o[r =>_] * hR)[rs, cf, af] ↔ (o[r => a × r0] * hR)[rs, cf, af]) ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ r =>_ = _∃(λ o. r => o)

• Proof step 5:

  cf(r) = a × r0, ¬((o[_∃(λ o. r => o)] * hR)[rs, cf, af] ↔ (o[r => a × r0] * hR)[rs, cf, af]) ⊦

Rule argument

Additional information

Used terms: r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  cf(r) = a × r0 ⊦ (∃ _o. (o[r => _o] * hR)[rs, cf, af]) ↔ (o[r => a × r0] * hR)[rs, cf, af]

Rule argument

Additional information

Used simplifier rules: sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep[heap-aux-inst] sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep[heap-aux-inst] ⊦ (_∃ oaR * hR)[rs, f, g] ↔ (∃ o, a. (oaR(o, a) * hR)[rs, f, g]); (s) ⊦ a[_∃ ohP] = _∃(λ o, a0. a[ohP(o)]); (s)

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

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  cf(r) = a × r0, ¬ (o[r => a × r0] * hR)[rs, cf, af], ∃ _o. (o[r => _o] * hR)[rs, cf, af] ⊦

• Proof step 54:

  cf(r) = a × r0, (o[r => a × r0] * hR)[rs, cf, af] ⊦ ∃ _o. (o[r => _o] * hR)[rs, cf, af]

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  cf(r) = a × r0, (o[r => _o] * hR)[rs, cf, af], ¬ (o[r => a × r0] * hR)[rs, cf, af] ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  cf(r) = a × r0, ¬ (o[r => a × r0] * hR)[rs, cf, af], ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ o[r => _o][rs0, cf, af] ∧ hR[rs1, cf, af] ⊦

Rule argument

Additional information

Used terms: cf, rs, hR, af, o[r => _o]

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, o[r => _o][rs0, cf, af], hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af] ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, hR[rs1, cf, af], o[r => _o][rs0, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af] ⊦ o[r => a × r0][rs0, cf, af] ∧ hR[rs1, cf, af] ∧ rs0 ∩ rs1 = ∅

Rule argument

Additional information

Used terms: cf, rs0, hR, af, o[r => a × r0], rs1

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, o[r => _o][rs0, cf, af], hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ¬ o[r => a × r0][rs0, cf, af] ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, hR[rs1, cf, af], o[r => _o][rs0, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ¬ o[r => a × r0](mk(rs0, cf, af)) ⊦

Rule argument

Additional information

Used terms: o[r => a × r0], rs0, cf, af

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

A spec-lemma

Proof step 16 from proof cf-map-unknown (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:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, o[r => _o][rs0, cf, af], hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ¬ ((r => a × r0))(mk(rs0, cf)) ∨ (∃ r. ¬(r ∈ rs0 → af(r) = o)) ⊦

Rule argument

Additional information

Used terms: cf, o, r => a × r0, rs0, af

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

A spec-lemma

Proof step 18 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, hR[rs1, cf, af], o[r => _o][rs0, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ¬ ((r => a × r0))(mk(rs0, cf)) ∨ ¬(r1 ∈ rs0 → af(r1) = o) ⊦

Rule argument

Additional information

Proof step 19 from proof cf-map-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

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

• Proof step 21:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, o[r => _o](mk(rs0, cf, af)), hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ¬ ((r => a × r0))(mk(rs0, cf)) ∨ ¬(r1 ∈ rs0 → af(r1) = o) ⊦

Rule argument

Additional information

Used terms: o[r => _o], rs0, cf, af

Proof step 20 from proof cf-map-unknown (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof cf-map-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, ((r => _o))(mk(rs0, cf)), hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ¬ ((r => a × r0))(mk(rs0, cf)) ∨ ¬(r1 ∈ rs0 → af(r1) = o) ⊦

Rule argument

Additional information

Used terms: cf, o, r => _o, rs0, af

Proof step 22 from proof cf-map-unknown (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, ((r => _o))(mk(rs0, cf)), hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ¬ ((r => a × r0))(mk(rs0, cf)) ∨ ¬(r1 ∈ rs0 → af(r1) = o) ⊦

Rule argument

Additional information

Proof step 24 from proof cf-map-unknown (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 25:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, ((r => _o))(mk(rs0, cf)), hR[rs1, cf, af], ¬ ((r => a × r0))(mk(rs0, cf)), ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

• Proof step 51:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, af(r1) ≠ o, ((r => _o))(mk(rs0, cf)), hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 25 from proof cf-map-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, ((r => _o))(mk(rs0, cf)), hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, mk(rs0, cf) ≠ (∅ ++ r)[r, a × r0] ∨ r = null ⊦

Rule argument

Additional information

Used terms: mk(rs0, cf), a × r0, r

Proof step 26 from proof cf-map-unknown (previous step) (back to tree)

A spec-lemma

Proof step 27 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, mk(rs0, cf) ≠ (∅ ++ r)[r, a × r0], r ≠ null, ((r => _o))(mk(rs0, cf)), hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

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

Proof step 28 from proof cf-map-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, r ≠ null, ((r => _o))(mk(rs0, cf)), hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ∃ r1. ¬((r1 ∈ mk(rs0, cf) ↔ r1 ∈ (∅ ++ r)[r, a × r0]) ∧ (r1 ∈ mk(rs0, cf) → mk(rs0, cf)[r1] = (∅ ++ r)[r, a × r0][r1])) ⊦

Rule argument

Additional information

Used terms: (∅ ++ r)[r, a × r0], mk(rs0, cf)

Proof step 29 from proof cf-map-unknown (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, r ≠ null, ((r => _o))(mk(rs0, cf)), hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦ (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → cf(r1) = (r1 = r ⊃ a × r0;(∅ ++ 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 31 from proof cf-map-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

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

• Proof step 33:

  cf(r) = a × r0, mk(rs0, cf) = (∅ ++ r)[r, _o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦ (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → cf(r1) = (r1 = r ⊃ a × r0;(∅ ++ r)[r1]))

Rule argument

Additional information

Used terms: mk(rs0, cf), _o, r

Proof step 32 from proof cf-map-unknown (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  cf(r) = a × r0, mk(rs0, cf) = (∅ ++ r)[r, _o], rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦ (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → cf(r1) = (r1 = r ⊃ a × r0;(∅ ++ r)[r1]))

Rule argument

Additional information

Proof step 34 from proof cf-map-unknown (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

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

• Proof step 36:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ∀ r0. (r0 ∈ mk(rs0, cf) ↔ r0 ∈ (∅ ++ r)[r, _o]) ∧ (r0 ∈ mk(rs0, cf) → mk(rs0, cf)[r0] = (∅ ++ r)[r, _o][r0]) ⊦ (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → cf(r1) = (r1 = r ⊃ a × r0;(∅ ++ r)[r1]))

Rule argument

Additional information

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

Proof step 35 from proof cf-map-unknown (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])) ⊦ (r1 ∈ rs0 ↔ r1 = r) ∧ (r1 ∈ rs0 → cf(r1) = (r1 = r ⊃ a × r0;(∅ ++ 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 37 from proof cf-map-unknown (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 38:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, ¬(r1 ∈ rs0 ↔ r1 = r), r ≠ null, hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])), ∀ r. r ∈ rs0 → af(r) = o ⊦

• Proof step 45:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, cf(r1) ≠ (r1 = r ⊃ a × r0;(∅ ++ r)[r1]), r ≠ null, hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])), ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 38 from proof cf-map-unknown (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 39:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, r ≠ null, r1 ≠ r, hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])) ⊦

• Proof step 43:

  cf(r) = a × r0, r1 = r, rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ¬ r1 ∈ rs0, ∀ r. r ∈ rs0 → af(r) = o, ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])) ⊦

Rule argument

Additional information

Proof step 39 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 40:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, r ≠ null, r1 ≠ r, hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])), ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 40 from proof cf-map-unknown (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 41:

  r0 ∈ rs0 ↔ r0 = r, cf(r) = a × r0, rs0 ∩ rs1 = ∅, r ≠ null, r1 ≠ r, hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], r0 ∈ rs0 → cf(r0) = (r0 = r ⊃ _o;(∅ ++ r)[r0]), ∀ r. r ∈ rs0 → af(r) = o, ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])) ⊦

Rule argument

Additional information

Used terms: r0

Proof step 41 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  r0 ∈ rs0 ↔ r0 = r, cf(r) = a × r0, rs0 ∩ rs1 = ∅, r ≠ null, r1 ≠ r, hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], r0 = r → a × r = _o, ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])), ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 42 from proof cf-map-unknown (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r1

Proof step 43 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, r ≠ null, hR[rs1, cf, af], ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ¬ r ∈ rs0, ∀ r. r ∈ rs0 → af(r) = o, ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (∅ ++ r)[r2]) ⊦

Rule argument

Additional information

Proof step 44 from proof cf-map-unknown (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 45 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, cf(r1) ≠ (r1 = r ⊃ a × r0;(∅ ++ r)[r1]), r ≠ null, hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])) ⊦

Rule argument

Additional information

Proof step 46 from proof cf-map-unknown (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 47:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, cf(r1) ≠ (∅ ++ r)[r1], r ≠ null, r1 ≠ r, hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])), ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 47 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, cf(r1) ≠ (∅ ++ r)[r1], r ≠ null, r1 ≠ r, hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o, ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])) ⊦

Rule argument

Additional information

Proof step 48 from proof cf-map-unknown (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 49:

  r0 ∈ rs0 ↔ r0 = r, cf(r) = a × r0, rs0 ∩ rs1 = ∅, cf(r1) ≠ (∅ ++ r)[r1], r ≠ null, r1 ≠ r, hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], r0 ∈ rs0 → cf(r0) = (r0 = r ⊃ _o;(∅ ++ r)[r0]), ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])), ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Used terms: r0

Proof step 49 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  r0 ∈ rs0 ↔ r0 = r, cf(r) = a × r0, rs0 ∩ rs1 = ∅, cf(r1) ≠ (∅ ++ r)[r1], r ≠ null, r1 ≠ r, hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], r0 = r → a × r = _o, ∀ r. r ∈ rs0 → af(r) = o, ∀ r2. (r2 ∈ rs0 ↔ r2 = r) ∧ (r2 ∈ rs0 → cf(r2) = (r2 = r ⊃ _o;(∅ ++ r)[r2])) ⊦

Rule argument

Additional information

Proof step 50 from proof cf-map-unknown (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r1

Proof step 51 from proof cf-map-unknown (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, af(r1) ≠ o, ((r => _o))(mk(rs0, cf)), hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Proof step 52 from proof cf-map-unknown (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And obtained the following new goals

• Proof step 53:

  cf(r) = a × r0, rs0 ∩ rs1 = ∅, af(r1) ≠ o, ((r => _o))(mk(rs0, cf)), hR[rs1, cf, af], r1 ∈ rs0, ¬ (o[r => a × r0] * hR)[rs0 ∪ rs1, cf, af], r0 ∈ rs0 → af(r0) = o, ∀ r. r ∈ rs0 → af(r) = o ⊦

Rule argument

Additional information

Used terms: r0

Proof step 53 from proof cf-map-unknown (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r1

Proof step 54 from proof cf-map-unknown (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: cf(r)