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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  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: apply: ⊦ hP[rs, f] ↔ hP(mk(rs, f)); 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 3 from proof split-uni (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 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: mk(rs1, f), mk(rs0, f), hP1, hP0

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

A spec-lemma