## The supremum

We have seen how to use the $\equiv$ operator to calculate with booleans. It is time to investigate another operator, the supremum, written as $\sqcup$‘ and pronounced cup’.
$\sqcup$ has a higher binding power than $\equiv$ which means that the expression

$X\sqcup Y\ \equiv\ Z$

$(X\sqcup Y)\equiv Z$

(Notice the greater space around $\equiv$ in the first expression).

The first two properties of the supremum are familiar:Associativity:$(X\sqcup Y)\sqcup Z\ \equiv\ X\sqcup(Y\sqcup Z)$

Symmetry:

$X\sqcup Y\ \equiv\ Y\sqcup X$

The next two are new:

Idempotence:

$X\sqcup X\ \equiv\ X$

Distributivity/Factoring:

$X\sqcup (Y\equiv Z)\ \equiv\ X\sqcup Y\ \equiv\ X\sqcup Z$

Armed with these rules, we can now prove our first property concerning the supremum:Distributivity/Factoring:

$X\sqcup (Y\sqcup Z)\ \equiv\ (X\sqcup Y)\sqcup (X\sqcup Z)$

Proof

$\quad(X\sqcup Y)\sqcup (X\sqcup Z)$

$\equiv\quad\{associativity\}$

$\quad X\sqcup (Y\sqcup X)\sqcup Z$

$\equiv\quad\{symmetry\}$

$\quad X\sqcup (X\sqcup Y)\sqcup Z$

$\equiv\quad\{associativity\}$

$\quad(X\sqcup X)\sqcup (Y\sqcup Z)$

$\equiv\quad\{idempotence\}$

$\quad X\sqcup (Y\sqcup Z)$

Our next rule isFixed point:

$X\sqcup\top\ \equiv\ \top$

Proof

$\quad X\sqcup\top$

$\equiv\quad\{(2)\}$

$\quad X\sqcup(Y\equiv Y)$

$\equiv\quad\{distributivity\}$

$\quad X\sqcup Y\ \equiv\ X\sqcup Y$

$\equiv\quad\{reflexivity\}$

$\quad\top$