# The many uses of \`disj\`

**URL:** <https://alloytools.discourse.group/t/the-many-uses-of-disj/447>\
**Category:** Alloy 6\
**Created:** [February 26, 2024, 5:40pm UTC](https://alloytools.discourse.group/t/the-many-uses-of-disj/447 "2024-02-26T17:40:46Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![hwayne](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/hwayne/32/67_2.png) [@hwayne](https://alloytools.discourse.group/u/hwayne)\
**Post date:** [February 26, 2024, 5:40pm UTC](https://alloytools.discourse.group/t/the-many-uses-of-disj/447/1 "2024-02-26T17:40:46Z")

</div>

So we know that `disj` can used in quantifiers:

```auto
all disj x, y: Key |
   no x.lock & y.lock

```

But did you know you can add it to fields?

```auto
sig Key {
  lock: disj some Lock
}

```

This means the same as the above predicate. If `lock` was a var, this would hold true in every state, too.

More niche is that you can put the `disj` _before_ the field name:

```auto
sig Lock {}
sig Key {
  , disj lock, lock2: one Lock 
}

```

Now `lock` and `lock2` will be disjoint for _each_ key.

Finally, you can use `disj` as a _predicate_:

```auto
all disj x, y, z, w: Key |
   disj[x.lock, y.lock, z.lock, w.lock]

```

`disj` takes any number of parameters.