## Logical Operations

Alloy supports the standard boolean operators:

** !F // negations: not F
F && G // conjunction: F and G
F || G // disjunction: F or G
**

It's useful to have a variety of implication operators:

** F => G // implication: same as !F || G
G <=> G // bi-implication: same as (F => G) && (G => F)
F => G else H // conditional: if F then G else H; same as (F => G) && (!F=> H)
**

If you do not write sufficient parentheses, Alloy assumes that
certain operations bind tighter than others. In order from tightest to loosest:

** not (!)
and (&&)
implication/conditional (=>)
bi-implication (<=>)
or (||)
**

Thus, the following pairs of expressions are equivalent

** !A && B // (!A) && B
A && B || C // (A && B) || C
A || B && C // A || (B && C)
A => B => C // (A => B) => C
**

You are permitted to add excess parentheses at your judgement.
Thus, `A`, `(A)`, and
`((A))` are all equivalent.

If you write several statements in the curly braces of the body of
a `fact`,
`assert`, or quantifier, those statements are implicityly conjoined
(`&&`). That is,

**fact Fibbles {
(no X) && (all y:Y | y in Foo)
}
**

could be written as

**fact Fibbles {
no X
all y:Y | y in Foo
}
**

and

**all x: e | F && G && H
**

could be written as

**all x: e {F G H}
**