module splits

sig Addr {}
sig Group {
	address: set Addr,
	split: set Group
	}

fact {
--	all g: Group | #g.address > 1
	}

fact {
	all g: Group {
		#g.address > 2 implies some g.split
		g not in g.split
		}

	all g: split.Group {
		g.address = g.split.address
		}

	all g: Group.split {
		#g.split.address < 3
		}
	
	all g: Group, disj g1, g2: g.split {
		no g1.address & g2.address

		#g1.address < #g2.address
			implies #g2.address = #g1.address + 1
		}
	}

assert A {
	all g: split.Group | #g.address = (sum g': g.split | #g'.address)

}
check A for 7

pred show () {
	some g: Group | #g.address = 5
	}
run show for 7