CONSTANTS
  Shards = {h, d}
  Old = {a, b}
  Fresh = {x, y}
  N = 2
  Claiming = TRUE

SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT NoPartialShard
INVARIANT RejectedBatchWritesNothing
INVARIANT AuditOnlyCommitted
INVARIANT AtMostOnePerCreate
INVARIANT RetryConverges
CHECK_DEADLOCK FALSE