Model the membership merges using TLA+

[ktoso]

Would be nice to model the merge formally, to sanity check we're not missing any edge case.

The merges are generally simple, except for removal which involves some special handling.

[ktoso]

See https://github.com/apple/swift-distributed-actors/tree/master/Models for other model examples