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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: modifysep-def: ⊦ hP[rs, f, g] ↔ hP[rs, λ r. f(r) ×× g(r)]__; 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] unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[refset] una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[refset] ⊦ hP0[rs0, f]__ ∧ hP1[rs1, f]__ ∧ rs0 ∩ rs1 = ∅ → (hP0 * hP1)[rs0 ∪ rs1, f]__; (ss) int-c: ⊦ s ∩ s0 = s0 ∩ s; from specification set-union[refset] int-a: ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1; from specification set-union[refset]