Proof step 1 from proof embed-split (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  a[hP0 * hP1] ≠ a[hP0] * a[hP1] ⊦

Rule argument

Additional information

Proof step 2 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ hR0 = hR1 ↔ (∀ rs, f, g. hR0[rs, f, g] ↔ hR1[rs, f, g])

• Proof step 4:

  ∃ rs, f, g. ¬(a[hP0 * hP1][rs, f, g] ↔ (a[hP0] * a[hP1])[rs, f, g]) ⊦

Rule argument

Additional information

Used terms: a[hP0] * a[hP1], a[hP0 * hP1]

Proof step 3 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(a[hP0 * hP1][rs, f, g] ↔ (a[hP0] * a[hP1])[rs, f, g]) ⊦

Rule argument

Additional information

Proof step 5 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  ¬(a[hP0 * hP1](mk(rs, f, g)) ↔ (a[hP0] * a[hP1])[rs, f, g]) ⊦

Rule argument

Additional information

Used terms: g, f, rs, a[hP0 * hP1]

Proof step 6 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

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

• Proof step 9:

  ¬(a[hP0 * hP1](mk(rs, f, g)) ↔ ((a[hP0] * a[hP1]))(mk(rs, f, g))) ⊦

Rule argument

Additional information

Used terms: g, f, rs, a[hP0] * a[hP1]

Proof step 8 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof embed-split (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  a[hP0 * hP1](mk(rs, f, g)), ¬ ((a[hP0] * a[hP1]))(mk(rs, f, g)) ⊦

• Proof step 39:

  ((a[hP0] * a[hP1]))(mk(rs, f, g)), ¬ a[hP0 * hP1](mk(rs, f, g)) ⊦

Rule argument

Additional information

Proof step 10 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

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

• Proof step 12:

  ((hP0 * hP1))(mk(rs, f)), ¬ ((a[hP0] * a[hP1]))(mk(rs, f, g)), ∀ r. r ∈ rs → g(r) = a ⊦

Rule argument

Additional information

Used terms: a, hP0 * hP1, rs, g, f

Proof step 11 from proof embed-split (previous step) (back to tree)

Lemma lift-aux

Proof step 12 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ((hP0 * hP1))(mk(rs, f)), ¬ ((a[hP0] * a[hP1]))(mk(rs, f, g)), ∀ r. r ∈ rs → g(r) = a ⊦

Rule argument

Additional information

Proof step 13 from proof embed-split (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 14:

  ⊦ hP[rs, f] ↔ hP(mk(rs, f))

• Proof step 15:

  (hP0 * hP1)[rs, f] ↔ ((hP0 * hP1))(mk(rs, f)), ((hP0 * hP1))(mk(rs, f)), ¬ ((a[hP0] * a[hP1]))(mk(rs, f, g)), ∀ r. r ∈ rs → g(r) = a ⊦

Rule argument

Additional information

Used terms: hP0 * hP1, rs, f

Proof step 14 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ((hP0 * hP1))(mk(rs, f)), (hP0 * hP1)[rs, f], ¬ ((a[hP0] * a[hP1]))(mk(rs, f, g)), ∀ r. r ∈ rs → g(r) = a ⊦

Rule argument

Additional information

Proof step 16 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ (hP0 * hP1)[rs, f] ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hP0[rs0, f] ∧ hP1[rs1, f])

• Proof step 18:

  ((hP0 * hP1))(mk(rs, f)), ¬ ((a[hP0] * a[hP1]))(mk(rs, f, g)), ∀ r. r ∈ rs → g(r) = a, ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ rs0 ∩ rs1 = ∅ ∧ hP0[rs0, f] ∧ hP1[rs1, f] ⊦

Rule argument

Additional information

Used terms: f, rs, hP1, hP0

Proof step 17 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  rs0 ∩ rs1 = ∅, ((hP0 * hP1))(mk(rs0 ∪ rs1, f)), hP0[rs0, f], hP1[rs1, f], ¬ ((a[hP0] * a[hP1]))(mk(rs0 ∪ rs1, f, g)), ∀ r. r ∈ rs0 ∪ rs1 → g(r) = a ⊦

Rule argument

Additional information

Proof step 19 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ rs0 ∩ rs1 = ∅ → mk(rs0 ∪ rs1, f, g) = mk(rs0, f, g) ∪ mk(rs1, f, g)

• Proof step 21:

  rs0 ∩ rs1 = ∅, ((hP0 * hP1))(mk(rs0 ∪ rs1, f)), hP1[rs1, f], hP0[rs0, f], ¬ ((a[hP0] * a[hP1]))(mk(rs0, f, g) ∪ mk(rs1, f, g)), ∀ r. r ∈ rs0 ∪ rs1 → g(r) = a ⊦

Rule argument

Additional information

Used terms: g, f, rs1, rs0

Proof step 20 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ hP0(h0) ∧ hP1(h1) ∧ h0 ⊥ h1 → ((hP0 * hP1))(h0 ∪ h1)

• Proof step 23:

  rs0 ∩ rs1 = ∅, ((hP0 * hP1))(mk(rs0 ∪ rs1, f)), hP0[rs0, f], hP1[rs1, f], ¬ ((a[hP0] * a[hP1]))(mk(rs0, f, g) ∪ mk(rs1, f, g)), ∀ r. r ∈ rs0 ∪ rs1 → g(r) = a ⊦ a[hP0](mk(rs0, f, g)) ∧ a[hP1](mk(rs1, f, g)) ∧ mk(rs0, f, g) ⊥ mk(rs1, f, g)

Rule argument

Additional information

Used terms: a[hP0], a[hP1], mk(rs0, f, g), mk(rs1, f, g)

Proof step 22 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

Used simplifier rules: ⊦ mk(rs0, f, g) ⊥ mk(rs1, f0, g0) ↔ rs0 ∩ rs1 = ∅; (s)

Proof step 24 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ hP[rs, f] ↔ hP(mk(rs, f))

• Proof step 26:

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

Rule argument

Additional information

Used terms: f, rs0, hP0

Proof step 25 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ hP[rs, f] ↔ hP(mk(rs, f))

• Proof step 28:

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

Rule argument

Additional information

Used terms: f, rs1, hP1

Proof step 27 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

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

Rule argument

Additional information

Used terms: a, hP0, rs0, g, f

Proof step 29 from proof embed-split (previous step) (back to tree)

Lemma lift-aux

Proof step 30 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

Proof step 31 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

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

• Proof step 33:

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

Rule argument

Additional information

Used terms: a, hP1, rs1, g, f

Proof step 32 from proof embed-split (previous step) (back to tree)

Lemma lift-aux

Proof step 33 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  rs0 ∩ rs1 = ∅, ((hP0 * hP1))(mk(rs0 ∪ rs1, f)), hP0(mk(rs0, f)), hP1(mk(rs1, f)), ¬ ((a[hP0] * a[hP1]))(mk(rs0, f, g) ∪ mk(rs1, f, g)), ∀ r. r ∈ rs0 ∪ rs1 → g(r) = a ⊦ (r ∈ rs0 → g(r) = a) ∧ (r0 ∈ rs1 → g(r0) = a)

Rule argument

Additional information

Proof step 34 from proof embed-split (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 35:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, ((hP0 * hP1))(mk(rs0 ∪ rs1, f)), hP0(mk(rs0, f)), hP1(mk(rs1, f)), r ∈ rs0, ¬ ((a[hP0] * a[hP1]))(mk(rs0, f, g) ∪ mk(rs1, f, g)), ∀ r. r ∈ rs0 ∪ rs1 → g(r) = a ⊦

• Proof step 37:

  rs0 ∩ rs1 = ∅, g(r0) ≠ a, ((hP0 * hP1))(mk(rs0 ∪ rs1, f)), hP0(mk(rs0, f)), hP1(mk(rs1, f)), r0 ∈ rs1, ¬ ((a[hP0] * a[hP1]))(mk(rs0, f, g) ∪ mk(rs1, f, g)), ∀ r. r ∈ rs0 ∪ rs1 → g(r) = a ⊦

Rule argument

Additional information

Proof step 35 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, ((hP0 * hP1))(mk(rs0 ∪ rs1, f)), hP0(mk(rs0, f)), hP1(mk(rs1, f)), r ∈ rs0, ¬ ((a[hP0] * a[hP1]))(mk(rs0, f, g) ∪ mk(rs1, f, g)), ∀ r. r ∈ rs0 ∪ rs1 → g(r) = a ⊦

Rule argument

Additional information

Proof step 36 from proof embed-split (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s ∪ s0 ↔ ¬(¬ a ∈ s ∧ ¬ a ∈ s0); (ss) una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] Used terms: r

Proof step 37 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  rs0 ∩ rs1 = ∅, g(r0) ≠ a, ((hP0 * hP1))(mk(rs0 ∪ rs1, f)), hP0(mk(rs0, f)), hP1(mk(rs1, f)), r0 ∈ rs1, ¬ ((a[hP0] * a[hP1]))(mk(rs0, f, g) ∪ mk(rs1, f, g)), ∀ r. r ∈ rs0 ∪ rs1 → g(r) = a ⊦

Rule argument

Additional information

Proof step 38 from proof embed-split (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s ∪ s0 ↔ ¬(¬ a ∈ s ∧ ¬ a ∈ s0); (ss) una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] Used terms: r0

Proof step 39 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ ((hP0 * hP1))(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 41:

  ¬ a[hP0 * hP1](mk(rs, f, g)), ∃ h0, h1. h0 ⊥ h1 ∧ mk(rs, f, g) = h0 ∪ h1 ∧ a[hP0](h0) ∧ a[hP1](h1) ⊦

Rule argument

Additional information

Used terms: a[hP0], a[hP1], mk(rs, f, g)

Proof step 40 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 41 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  mk(rs, f, g) = h0 ∪ h1, a[hP0](h0), a[hP1](h1), h0 ⊥ h1, ¬ a[hP0 * hP1](mk(rs, f, g)) ⊦

Rule argument

Additional information

Proof step 42 from proof embed-split (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 43:

  ⊦ ∃ rs, f, g. ha = mk(rs, f, g)

• Proof step 44:

  mk(rs, f, g) = h0 ∪ h1, a[hP1](h1), a[hP0](h0), h0 ⊥ h1, ¬ a[hP0 * hP1](mk(rs, f, g)), ∃ rs, f, g. h0 = mk(rs, f, g) ⊦

Rule argument

Additional information

Used terms: h0

Proof step 43 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 44 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ h1, a[hP0](mk(rs0, f0, g0)), a[hP1](h1), mk(rs0, f0, g0) ⊥ h1, ¬ a[hP0 * hP1](mk(rs, f, g)) ⊦

Rule argument

Additional information

Proof step 45 from proof embed-split (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 46:

  ⊦ ∃ rs, f, g. ha = mk(rs, f, g)

• Proof step 47:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ h1, a[hP1](h1), a[hP0](mk(rs0, f0, g0)), mk(rs0, f0, g0) ⊥ h1, ¬ a[hP0 * hP1](mk(rs, f, g)), ∃ rs, f, g. h1 = mk(rs, f, g) ⊦

Rule argument

Additional information

Used terms: h1

Proof step 46 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 47 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), a[hP0](mk(rs0, f0, g0)), a[hP1](mk(rs1, f1, g1)), mk(rs0, f0, g0) ⊥ mk(rs1, f1, g1), ¬ a[hP0 * hP1](mk(rs, f, g)) ⊦

Rule argument

Additional information

Proof step 48 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), a[hP1](mk(rs1, f1, g1)), a[hP0](mk(rs0, f0, g0)), mk(rs0, f0, g0) ⊥ mk(rs1, f1, g1), ¬ ((hP0 * hP1))(mk(rs, f)) ∨ (∃ r. ¬(r ∈ rs → g(r) = a)) ⊦

Rule argument

Additional information

Used terms: a, hP0 * hP1, rs, g, f

Proof step 49 from proof embed-split (previous step) (back to tree)

Lemma lift-aux

Proof step 50 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, a[hP0](mk(rs0, f0, g0)), a[hP1](mk(rs1, f1, g1)), ¬ ((hP0 * hP1))(mk(rs, f)) ∨ ¬(r ∈ rs → g(r) = a) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ mk(rs0, f, g) ⊥ mk(rs1, f0, g0) ↔ rs0 ∩ rs1 = ∅; (s)

Proof step 51 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ ((hP0 * hP1))(h) ↔ (∃ h0, h1. h0 ⊥ h1 ∧ h = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1))

• Proof step 53:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, a[hP1](mk(rs1, f1, g1)), a[hP0](mk(rs0, f0, g0)), ¬(∃ h0, h1. h0 ⊥ h1 ∧ mk(rs, f) = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1)) ∨ ¬(r ∈ rs → g(r) = a) ⊦

Rule argument

Additional information

Used terms: mk(rs, f), hP1, hP0

Proof step 52 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof embed-split (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 54:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, a[hP0](mk(rs0, f0, g0)), a[hP1](mk(rs1, f1, g1)) ⊦ ∃ h0, h1. h0 ⊥ h1 ∧ mk(rs, f) = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1)

• Proof step 75:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, g(r) ≠ a, a[hP0](mk(rs0, f0, g0)), a[hP1](mk(rs1, f1, g1)), r ∈ rs ⊦

Rule argument

Additional information

Proof step 54 from proof embed-split (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 55:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, a[hP1](mk(rs1, f1, g1)), a[hP0](mk(rs0, f0, g0)) ⊦ mk(rs0, f0) ⊥ mk(rs1, f1) ∧ mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1) ∧ hP0(mk(rs0, f0)) ∧ hP1(mk(rs1, f1))

Rule argument

Additional information

Used terms: mk(rs0, f0), mk(rs1, f1)

Proof step 55 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 56:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, a[hP0](mk(rs0, f0, g0)), a[hP1](mk(rs1, f1, g1)) ⊦ mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1) ∧ hP0(mk(rs0, f0)) ∧ hP1(mk(rs1, f1))

Rule argument

Additional information

Used simplifier rules: ⊦ mk(rs0, f0) ⊥ mk(rs1, f1) ↔ rs0 ∩ rs1 = ∅; (s)

Proof step 56 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 57:

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

• Proof step 58:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, a[hP1](mk(rs1, f1, g1)), hP0(mk(rs0, f0)), ∀ r. r ∈ rs0 → g0(r) = a ⊦ mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1) ∧ hP0(mk(rs0, f0)) ∧ hP1(mk(rs1, f1))

Rule argument

Additional information

Used terms: a, hP0, rs0, g0, f0

Proof step 57 from proof embed-split (previous step) (back to tree)

Lemma lift-aux

Proof step 58 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, a[hP1](mk(rs1, f1, g1)), hP0(mk(rs0, f0)), ∀ r. r ∈ rs0 → g0(r) = a ⊦ mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1) ∧ hP1(mk(rs1, f1))

Rule argument

Additional information

Proof step 59 from proof embed-split (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:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ∀ r. r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs1 → g1(r) = a ⊦ mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1) ∧ hP1(mk(rs1, f1))

Rule argument

Additional information

Used terms: a, hP1, rs1, g1, f1

Proof step 60 from proof embed-split (previous step) (back to tree)

Lemma lift-aux

Proof step 61 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, mk(rs, f) ≠ mk(rs0, f0) ∪ mk(rs1, f1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs0 → g0(r) = a ⊦

Rule argument

Additional information

Proof step 62 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

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

• Proof step 64:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ∀ r. r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs1 → g1(r) = a, ∃ r. ¬((r ∈ mk(rs, f) ↔ r ∈ mk(rs0, f0) ∪ mk(rs1, f1)) ∧ (r ∈ mk(rs, f) → mk(rs, f)[r] = (mk(rs0, f0) ∪ mk(rs1, f1))[r])) ⊦

Rule argument

Additional information

Used terms: mk(rs0, f0) ∪ mk(rs1, f1), mk(rs, f)

Proof step 63 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 64 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs0 → g0(r) = a ⊦ (r ∈ rs ↔ r ∈ mk(rs0, f0) ∪ mk(rs1, f1)) ∧ (r ∈ rs → f(r) = (mk(rs0, f0) ∪ mk(rs1, f1))[r])

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ rs → mk(rs, f)[r] = f(r); (s) ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; (s)

Proof step 65 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

  ⊦ ha0 = ha1 ↔ (∀ r. (r ∈ ha0 ↔ r ∈ ha1) ∧ (r ∈ ha0 → ha0[r]o = ha1[r]o ∧ ha0[r]a = ha1[r]a))

• Proof step 67:

  rs0 ∩ rs1 = ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ∀ r. r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. (r ∈ mk(rs, f, g) ↔ r ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r ∈ mk(rs, f, g) → mk(rs, f, g)[r]o = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]o ∧ mk(rs, f, g)[r]a = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]a) ⊦ (r ∈ rs ↔ r ∈ mk(rs0, f0) ∪ mk(rs1, f1)) ∧ (r ∈ rs → f(r) = (mk(rs0, f0) ∪ mk(rs1, f1))[r])

Rule argument

Additional information

Used terms: mk(rs, f, g), mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)

Proof step 66 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 67 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  rs0 ∩ rs1 = ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs0 → g0(r) = a, ∀ r0. (r0 ∈ rs ↔ r0 ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]o ∧ g(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]a) ⊦ (r ∈ rs ↔ r ∈ mk(rs0, f0) ∪ mk(rs1, f1)) ∧ (r ∈ rs → f(r) = (mk(rs0, f0) ∪ mk(rs1, f1))[r])

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ rs → mk(rs, f, g)[r]a = g(r); (s) ⊦ r ∈ rs → mk(rs, f, g)[r]o = f(r); (s) ⊦ r ∈ mk(rs, f, g) ↔ r ∈ rs; (s)

Proof step 68 from proof embed-split (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 69:

  r ∈ rs ↔ r ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs → f(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]o ∧ g(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]a, ∀ r0. (r0 ∈ rs ↔ r0 ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]o ∧ g(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]a), ∀ r. r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs1 → g1(r) = a ⊦ (r ∈ rs ↔ r ∈ mk(rs0, f0) ∪ mk(rs1, f1)) ∧ (r ∈ rs → f(r) = (mk(rs0, f0) ∪ mk(rs1, f1))[r])

Rule argument

Additional information

Used terms: r

Proof step 69 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 70:

  r ∈ rs ↔ r ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs → f(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]o ∧ g(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]a, ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs0 → g0(r) = a, ∀ r0. (r0 ∈ rs ↔ r0 ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]o ∧ g(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]a) ⊦ (r ∈ rs ↔ r ∈ mk(rs0, f0) ∪ mk(rs1, f1)) ∧ (r ∈ rs → f(r) = (mk(rs0, f0) ∪ mk(rs1, f1))[r])

Rule argument

Additional information

Proof step 70 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 71:

  ⊦ h0 ⊥ h1 → (r ∈ h0 ∪ h1 ↔ r ∈ h0 ∨ r ∈ h1)

• Proof step 72:

  r ∈ rs ↔ r ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), mk(rs0, f0) ⊥ mk(rs1, f1), r ∈ rs → f(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]o ∧ g(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]a, ∀ r0. (r0 ∈ rs ↔ r0 ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]o ∧ g(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]a), ∀ r. r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs1 → g1(r) = a ⊦ (r ∈ rs ↔ r ∈ mk(rs0, f0) ∨ r ∈ mk(rs1, f1)) ∧ (r ∈ rs → f(r) = (mk(rs0, f0) ∪ mk(rs1, f1))[r])

Rule argument

Additional information

Used simplifier rules: ⊦ mk(rs0, f0) ⊥ mk(rs1, f1) ↔ rs0 ∩ rs1 = ∅; (s) Used terms: r, mk(rs0, f0), mk(rs1, f1)

Proof step 71 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 72 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 73:

  r ∈ rs ↔ r ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs → f(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]o ∧ g(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]a, ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs0 → g0(r) = a, ∀ r0. (r0 ∈ rs ↔ r0 ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]o ∧ g(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]a) ⊦ (r ∈ rs ↔ r ∈ rs0 ∨ r ∈ rs1) ∧ (r ∈ rs → f(r) = (mk(rs0, f0) ∪ mk(rs1, f1))[r])

Rule argument

Additional information

Used simplifier rules: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; (s) ⊦ mk(rs0, f0) ⊥ mk(rs1, f1) ↔ rs0 ∩ rs1 = ∅; (s)

Proof step 73 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 74:

  ⊦ rs0 ∩ rs1 = ∅ → (r ∈ mk(rs0, f, g) ∪ mk(rs1, f0, g0) ↔ r ∈ rs0 ∨ r ∈ rs1)

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] ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs0 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]o = f(r); (s) ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs0 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]a = g(r); (s) ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs0 → (mk(rs0, f0) ∪ mk(rs1, f1))[r] = f0(r); (s) ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs1 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]o = f0(r); (s) ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs1 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]a = g0(r); (s) ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs1 → (mk(rs0, f0) ∪ mk(rs1, f1))[r] = f1(r); (s) Used terms: r, f1, rs0, g0, f0, rs1, g1

Proof step 74 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 75 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 76:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, g(r) ≠ a, a[hP1](mk(rs1, f1, g1)), a[hP0](mk(rs0, f0, g0)), r ∈ rs ⊦

Rule argument

Additional information

Proof step 76 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 77:

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

• Proof step 78:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, g(r) ≠ a, a[hP0](mk(rs0, f0, g0)), hP1(mk(rs1, f1)), r ∈ rs, ∀ r. r ∈ rs1 → g1(r) = a ⊦

Rule argument

Additional information

Used terms: a, hP1, rs1, g1, f1

Proof step 77 from proof embed-split (previous step) (back to tree)

Lemma lift-aux

Proof step 78 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 79:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, g(r) ≠ a, a[hP0](mk(rs0, f0, g0)), hP1(mk(rs1, f1)), r ∈ rs, ∀ r. r ∈ rs1 → g1(r) = a ⊦

Rule argument

Additional information

Proof step 79 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 80:

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

• Proof step 81:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, g(r) ≠ a, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs, ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs0 → g0(r) = a ⊦

Rule argument

Additional information

Used terms: a, hP0, rs0, g0, f0

Proof step 80 from proof embed-split (previous step) (back to tree)

Lemma lift-aux

Proof step 81 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 82:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, g(r) ≠ a, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs, ∀ r. r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs1 → g1(r) = a ⊦

Rule argument

Additional information

Proof step 82 from proof embed-split (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 83:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, g(r) ≠ a, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs, r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs0 → g0(r) = a ⊦

Rule argument

Additional information

Used terms: r

Proof step 83 from proof embed-split (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 84:

  mk(rs, f, g) = mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, g(r) ≠ a, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs, r ∈ rs1 → g1(r) = a, r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs1 → g1(r) = a ⊦

Rule argument

Additional information

Used terms: r

Proof step 84 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 85:

  ⊦ ha0 = ha1 ↔ (∀ r. (r ∈ ha0 ↔ r ∈ ha1) ∧ (r ∈ ha0 → ha0[r]o = ha1[r]o ∧ ha0[r]a = ha1[r]a))

• Proof step 86:

  rs0 ∩ rs1 = ∅, g(r) ≠ a, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs, r ∈ rs0 → g0(r) = a, r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs0 → g0(r) = a, ∀ r. (r ∈ mk(rs, f, g) ↔ r ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r ∈ mk(rs, f, g) → mk(rs, f, g)[r]o = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]o ∧ mk(rs, f, g)[r]a = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]a) ⊦

Rule argument

Additional information

Used terms: mk(rs, f, g), mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)

Proof step 85 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 86 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 87:

  rs0 ∩ rs1 = ∅, # rs ≠ 0, g(r) ≠ a, rs ≠ ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs, r ∈ rs0 → g0(r) = a, r ∈ rs1 → g1(r) = a, ∀ r0. (r0 ∈ rs ↔ r0 ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]o ∧ g(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]a), ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs0 → g0(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] ⊦ r ∈ rs → mk(rs, f, g)[r]a = g(r); (s) ⊦ r ∈ rs → mk(rs, f, g)[r]o = f(r); (s) ⊦ r ∈ mk(rs, f, g) ↔ r ∈ rs; (s)

Proof step 87 from proof embed-split (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 88:

  r ∈ rs ↔ r ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), rs0 ∩ rs1 = ∅, # rs ≠ 0, g(r) ≠ a, rs ≠ ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs, r ∈ rs1 → g1(r) = a, r ∈ rs0 → g0(r) = a, r ∈ rs → f(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]o ∧ g(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]a, ∀ r. r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs1 → g1(r) = a, ∀ r0. (r0 ∈ rs ↔ r0 ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]o ∧ g(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]a) ⊦

Rule argument

Additional information

Used terms: r

Proof step 88 from proof embed-split (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  f(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]o, g(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]a, rs0 ∩ rs1 = ∅, # rs ≠ 0, g(r) ≠ a, rs ≠ ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs, r ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1), r ∈ rs0 → g0(r) = a, r ∈ rs1 → g1(r) = a, ∀ r0. (r0 ∈ rs ↔ r0 ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]o ∧ g(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]a), ∀ r. r ∈ rs1 → g1(r) = a, ∀ r. r ∈ rs0 → g0(r) = a ⊦

Rule argument

Additional information

Proof step 89 from proof embed-split (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 90:

  ⊦ rs0 ∩ rs1 = ∅ → (r ∈ mk(rs0, f, g) ∪ mk(rs1, f0, g0) ↔ r ∈ rs0 ∨ r ∈ rs1)

• Proof step 91:

  f(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]o, g(r) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r]a, rs0 ∩ rs1 = ∅, # rs ≠ 0, g(r) ≠ a, rs ≠ ∅, hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs, r ∈ rs1 → g1(r) = a, r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs0 → g0(r) = a, ∀ r. r ∈ rs1 → g1(r) = a, ∀ r0. (r0 ∈ rs ↔ r0 ∈ mk(rs0, f0, g0) ∪ mk(rs1, f1, g1)) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]o ∧ g(r0) = (mk(rs0, f0, g0) ∪ mk(rs1, f1, g1))[r0]a), r ∈ rs0 ∨ r ∈ rs1 ⊦

Rule argument

Additional information

Used terms: r, f1, rs0, g0, f0, rs1, g1

Proof step 90 from proof embed-split (previous step) (back to tree)

A spec-lemma

Proof step 91 from proof embed-split (previous step) (back to tree)

User applied rule case distinction

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] ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs1 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]a = g0(r); (s) ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs1 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]o = f0(r); (s) ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs0 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]a = g(r); (s) ⊦ rs0 ∩ rs1 = ∅ ∧ r ∈ rs0 → (mk(rs0, f, g) ∪ mk(rs1, f0, g0))[r]o = f(r); (s)