// Theorem 4.4.7: Any pair of synchronization actions of distinct actors concerning distinct mutexes are independent
if (mutex_ != other->mutex_)
return false;
// Theorem 4.4.11: LOCK indep TEST/WAIT.
// If both enabled, the result does not depend on their order. If WAIT is not enabled, LOCK won't enable it.
// Theorem 4.4.7: Any pair of synchronization actions of distinct actors concerning distinct mutexes are independent
if (mutex_ != other->mutex_)
return false;
// Theorem 4.4.11: LOCK indep TEST/WAIT.
// If both enabled, the result does not depend on their order. If WAIT is not enabled, LOCK won't enable it.