Proof step 1 from proof sep (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ (hP0 * hP1)(mk(rs, f)) ↔ (∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f)))

Rule argument

Additional information

Used simplifier rules: apply: ⊦ hP[rs, f] ↔ hP(mk(rs, f));

Proof step 2 from proof sep (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  (hP0 * hP1)(mk(rs, f)) ⊦ ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f))

• Proof step 38:

  ¬ (hP0 * hP1)(mk(rs, f)), ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f)) ⊦

Rule argument

Additional information

Proof step 3 from proof sep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  ∃ h0, h1. h0 ⊥ h1 ∧ mk(rs, f) = h0 ∪ h1 ∧ hP0(h0) ∧ hP1(h1) ⊦ ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f))

Rule argument

Additional information

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

Proof step 4 from proof sep (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  mk(rs, f) = h0 ∪ h1, h0 ⊥ h1, hP0(h0), hP1(h1) ⊦ ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f))

Rule argument

Additional information

Proof step 6 from proof sep (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ∃ rs, f. h = mk(rs, f)

• Proof step 8:

  mk(rs, f) = h0 ∪ h1, h0 ⊥ h1, hP0(h0), hP1(h1), ∃ rs, f. h0 = mk(rs, f) ⊦ ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f))

Rule argument

Additional information

Used terms: h0

Proof step 7 from proof sep (previous step) (back to tree)

Lemma mk-exists

Proof step 8 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  mk(rs, f) = mk(rs0, f0) ∪ h1, hP0(mk(rs0, f0)), hP1(h1), mk(rs0, f0) ⊥ h1 ⊦ ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f))

Rule argument

Additional information

Proof step 9 from proof sep (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ∃ rs, f. h = mk(rs, f)

• Proof step 11:

  mk(rs, f) = mk(rs0, f0) ∪ h1, hP0(mk(rs0, f0)), hP1(h1), mk(rs0, f0) ⊥ h1, ∃ rs, f. h1 = mk(rs, f) ⊦ ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f))

Rule argument

Additional information

Used terms: h1

Proof step 10 from proof sep (previous step) (back to tree)

Lemma mk-exists

Proof step 11 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)) ⊦ ∃ rs0, rs1. rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f))

Rule argument

Additional information

Used simplifier rules: disj: ⊦ mk(rs0, f0) ⊥ mk(rs1, f1) ↔ rs0 ∩ rs1 = ∅; int-c: ⊦ s ∩ s0 = s0 ∩ s; from specification set-union int-a: ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1; from specification set-union ⊦ s1 ∩ s2 = ∅ ↔ disjoint(s1, s2); (s)

Proof step 12 from proof sep (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 13:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)) ⊦ rs0 ∪ rs1 = rs ∧ disjoint(rs0, rs1) ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f))

Rule argument

Additional information

Used terms: rs0, rs1

Proof step 13 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)) ⊦ rs0 ∪ rs1 = rs ∧ hP0(mk(rs0, f)) ∧ hP1(mk(rs1, f))

Rule argument

Additional information

Proof step 14 from proof sep (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 15:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), rs0 ∪ rs1 ≠ rs, disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)) ⊦

• Proof step 22:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ¬ hP0(mk(rs0, f)) ⊦

• Proof step 30:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ¬ hP1(mk(rs1, f)) ⊦

Rule argument

Additional information

Proof step 15 from proof sep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

  rs0 ∪ rs1 ≠ rs, disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ∀ 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 16 from proof sep (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  rs0 ∪ rs1 ≠ rs, disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ∀ r. (r ∈ rs ↔ r ∈ rs0 ∨ r ∈ rs1) ∧ (r ∈ rs → f(r) = (mk(rs0, f0) ∪ mk(rs1, f1))(r)) ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ disjoint(rs0, rs1) → (r ∈ mk(rs0, f0) ∪ mk(rs1, f1) ↔ r ∈ rs0 ∨ r ∈ rs1); in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; at-mk: ⊦ r ∈ rs → mk(rs, f)(r) = f(r);

Proof step 18 from proof sep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2)

• Proof step 20:

  disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ∃ a. ¬(a ∈ rs0 ∪ rs1 ↔ a ∈ rs), ∀ r. (r ∈ rs ↔ r ∈ rs0 ∨ r ∈ rs1) ∧ (r ∈ rs → f(r) = (mk(rs0, f0) ∪ mk(rs1, f1))(r)) ⊦

Rule argument

Additional information

Used terms: rs0 ∪ rs1, rs

Proof step 19 from proof sep (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  ¬(r ∈ rs0 ∨ r ∈ rs1 ↔ r ∈ rs), disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ∀ r. (r ∈ rs ↔ r ∈ rs0 ∨ r ∈ rs1) ∧ (r ∈ rs → f(r) = (mk(rs0, f0) ∪ mk(rs1, f1))(r)) ⊦

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union ⊦ a ∈ s1 ∪ s2 ↔ a ∈ s1 ∨ a ∈ s2; (s)

Proof step 21 from proof sep (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: r

Proof step 22 from proof sep (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 23:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), mk(rs0, f) ≠ mk(rs0, f0), disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ¬ hP0(mk(rs0, f)) ⊦

Rule argument

Additional information

Used formulas: mk(rs0, f) = mk(rs0, f0)

Proof step 23 from proof sep (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:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ¬ hP0(mk(rs0, f)), ∃ r. ¬((r ∈ mk(rs0, f) ↔ r ∈ mk(rs0, f0)) ∧ (r ∈ mk(rs0, f) → mk(rs0, f)(r) = mk(rs0, f0)(r))) ⊦

Rule argument

Additional information

Used terms: mk(rs0, f0), mk(rs0, f)

Proof step 24 from proof sep (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), # rs0 ≠ 0, f(r) ≠ f0(r), rs0 ≠ ∅, disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs0, ¬ hP0(mk(rs0, f)) ⊦

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; at-mk: ⊦ r ∈ rs → mk(rs, f)(r) = f(r); size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 26 from proof sep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

  # rs0 ≠ 0, f(r) ≠ f0(r), rs0 ≠ ∅, disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs0, ¬ hP0(mk(rs0, f)), ∀ 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 27 from proof sep (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  # rs0 ≠ 0, f(r) ≠ f0(r), rs0 ≠ ∅, disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs0, ¬ hP0(mk(rs0, f)), ∀ r0. (r0 ∈ rs ↔ r0 ∈ rs0 ∨ r0 ∈ rs1) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0) ∪ mk(rs1, f1))(r0)) ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ disjoint(rs0, rs1) → (r ∈ mk(rs0, f0) ∪ mk(rs1, f1) ↔ r ∈ rs0 ∨ r ∈ rs1); in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; at-mk: ⊦ r ∈ rs → mk(rs, f)(r) = f(r);

Proof step 29 from proof sep (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: at-unil: ⊦ disjoint(rs0, rs1) ∧ r ∈ rs0 → (mk(rs0, f0) ∪ mk(rs1, f1))(r) = f0(r); Used terms: r

Proof step 30 from proof sep (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 31:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), mk(rs1, f) ≠ mk(rs1, f1), disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ¬ hP1(mk(rs1, f)) ⊦

Rule argument

Additional information

Used formulas: mk(rs1, f) = mk(rs1, f1)

Proof step 31 from proof sep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

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

• Proof step 33:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), ¬ hP1(mk(rs1, f)), ∃ r. ¬((r ∈ mk(rs1, f) ↔ r ∈ mk(rs1, f1)) ∧ (r ∈ mk(rs1, f) → mk(rs1, f)(r) = mk(rs1, f1)(r))) ⊦

Rule argument

Additional information

Used terms: mk(rs1, f1), mk(rs1, f)

Proof step 32 from proof sep (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  mk(rs, f) = mk(rs0, f0) ∪ mk(rs1, f1), # rs1 ≠ 0, f(r) ≠ f1(r), rs1 ≠ ∅, disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs1, ¬ hP1(mk(rs1, f)) ⊦

Rule argument

Additional information

Used simplifier rules: in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; at-mk: ⊦ r ∈ rs → mk(rs, f)(r) = f(r); size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 34 from proof sep (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:

  # rs1 ≠ 0, f(r) ≠ f1(r), rs1 ≠ ∅, disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs1, ¬ hP1(mk(rs1, f)), ∀ 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 35 from proof sep (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  # rs1 ≠ 0, f(r) ≠ f1(r), rs1 ≠ ∅, disjoint(rs0, rs1), hP0(mk(rs0, f0)), hP1(mk(rs1, f1)), r ∈ rs1, ¬ hP1(mk(rs1, f)), ∀ r0. (r0 ∈ rs ↔ r0 ∈ rs0 ∨ r0 ∈ rs1) ∧ (r0 ∈ rs → f(r0) = (mk(rs0, f0) ∪ mk(rs1, f1))(r0)) ⊦

Rule argument

Additional information

Used simplifier rules: in-uni: ⊦ disjoint(rs0, rs1) → (r ∈ mk(rs0, f0) ∪ mk(rs1, f1) ↔ r ∈ rs0 ∨ r ∈ rs1); in-mk: ⊦ r ∈ mk(rs, f) ↔ r ∈ rs; at-mk: ⊦ r ∈ rs → mk(rs, f)(r) = f(r);

Proof step 37 from proof sep (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: at-unir: ⊦ disjoint(rs0, rs1) ∧ r ∈ rs1 → (mk(rs0, f0) ∪ mk(rs1, f1))(r) = f1(r); ⊦ disjoint(s, s0) ∧ a ∈ s0 → (a ∈ s ↔ false); (as) Used terms: r

Proof step 38 from proof sep (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  disjoint(rs0, rs1), hP0(mk(rs0, f)), hP1(mk(rs1, f)), ¬ (hP0 * hP1)(mk(rs0, f) ∪ mk(rs1, f)) ⊦

Rule argument

Additional information

Used simplifier rules: uni: ⊦ disjoint(rs0, rs1) → mk(rs0 ∪ rs1, f) = mk(rs0, f) ∪ mk(rs1, f); unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union

Proof step 39 from proof sep (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

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

Rule argument

Additional information

Used simplifier rules: disj: ⊦ mk(rs0, f0) ⊥ mk(rs1, f1) ↔ rs0 ∩ rs1 = ∅; ⊦ s1 ∩ s2 = ∅ ↔ disjoint(s1, s2); (s) int-a: ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1; from specification set-union int-c: ⊦ s ∩ s0 = s0 ∩ s; from specification set-union Used terms: hP0, mk(rs0, f), hP1, mk(rs1, f)

Proof step 40 from proof sep (previous step) (back to tree)

A spec-lemma