# How to say "these should not be equal"
**URL:** https://alloytools.discourse.group/t/how-to-say-these-should-not-be-equal/27
**Category:** models
**Created:** [August 20, 2020, 5:45pm UTC](https://alloytools.discourse.group/t/how-to-say-these-should-not-be-equal/27 "2020-08-20T17:45:10Z")
**Posts on this page:** 4
**Page:** 1
### Author:  [@brianhicks](https://alloytools.discourse.group/u/brianhicks)
#### Post date: [August 20, 2020, 5:45pm UTC](https://alloytools.discourse.group/t/how-to-say-these-should-not-be-equal/27/1 "2020-08-20T17:45:10Z")
hey, it’s git time again! I’m picking back up from the model from [No instances of Tree—why?](https://alloytools.discourse.group/t/no-instances-of-tree-why/19/5), which now looks like this:
```auto
sig Object {}
sig Tree {
children: some (Object + Tree)
}
fact {
no t: Tree | t in t.^children
}
pred Default {}
run Default for 3
```
instead of moving on to model git’s commits immediately, I’m pausing here to make sure my model’s trees do not do anything that real git trees couldn’t. After producing a bunch of instances, I see that my model can produce this instance:
But I can’t produce it by manipulating objects in `git`! Hooray for content-addressed stores, I guess.
I _think_ the thing I want to say is “there are no two trees with the same children”. The thing I’m trying naively is adding the following fact to the `fact` block in the model above:
```auto
no t, u: Tree | t.children = u.children
```
but when I run that, I just get a bunch of empty trees, so I suspect that this does not do the thing I think it does! I sat down and thought about how `.` works, and my best guess is that I’m actually asking something about the nature of the children rather than the nature of the trees.
So, two questions:
1. how do I enact the intent I described above?
2. what is the code I wrote actually doing?
---
### Author:  [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)
#### Post date: [August 20, 2020, 9:30pm UTC](https://alloytools.discourse.group/t/how-to-say-these-should-not-be-equal/27/2 "2020-08-20T21:30:25Z")
Hi Brian,
The problem is that the constraint `t.children = u.children` will be true when `u = t`! So the only was to satisfy the quantified formula is to ensure there are no trees. The fix is to write something like
`no t, u: Tree | t.children = u.children and t != u`
or
`no disj t, u: Tree | t.children = u.children`
BTW, if you want to ensure that no two distinct trees overlap in their children, you’ll need something different, like
`no disj t, u: Tree | some t.children & u.children`
which can also be written as a declaration constraint
`children in Tree lone -> (Object + Tree)`
saying that at most one (less than or equal to one, or lone) tree is mapped to a given child.
---
### Author:  [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)
#### Post date: [August 21, 2020, 8:03am UTC](https://alloytools.discourse.group/t/how-to-say-these-should-not-be-equal/27/3 "2020-08-21T08:03:40Z")
> [@DanielJackson](#):
>
> So the only was to satisfy the quantified formula is to ensure there are no trees.
This is a very frequent problem I ran into. A quantification is `true` when there are no elements. I often have to check if there are _any_ elements.
---
### Author:  [@brianhicks](https://alloytools.discourse.group/u/brianhicks)
#### Post date: [August 24, 2020, 7:15pm UTC](https://alloytools.discourse.group/t/how-to-say-these-should-not-be-equal/27/4 "2020-08-24T19:15:32Z")
thanks again, folks! 😁