module analysis/unionClosure

sig Set {
	elements: set Element
	}

sig Element {}

assert Closed {
	all s0, s1: Set | some s2: Set |
		s2.elements = s0.elements + s1.elements
	}
check Closed for 3 but 16 Set

fact SetGenerator {
	some s: Set | no s.elements
	all s: Set, e: Element |
		some s': Set | s'.elements = s.elements + e
	}