Theorem split-union

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: Frame, Imp2, adjunction, and-imp, and-split, imp-mono, introduce-sharing, precise-split-l, precise-split-r, prop-sep, sep-ass, sep-com, stability, true-elim,
• Used by units in proved state: embed-aux, iter-store, separation-rg, iter-set, heap-fun, maplet,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 1
• Proof steps: 3
• Used lemmas: sep,
• Used spec theorems:
  • Used simplifier rules: