This goes through the typechecking of fail03.not in detail.

Before we even run, we know these constraints:
Public ⊑ Public
Secret ⊑ Secret
For all a, Lₐ ⊑ Lₐ

...this follows from the definition of ⊑, which includes equality.
So for any level l, l ⊑ l.

With the checking of fail03.not, we start with the security level of Public
(i.e. lw = Public) and an empty environment (ρ=∅).  The first rule 
executed (var ... in ...) generates a new type environment that looks 
like the following:

ρ: [x -> L₁, y -> L₂]

Immediately after generating this type environment, constraints start being
added.  Each constraint follows, along with the rule that generated it:
Public ⊑ L₁      // var ... in ...
Public ⊑ L₂      // var ... in ...
Public ⊑ Secret  // output "..."
Public ⊑ Secret  // output "..."
Public ⊑ L₃      // input
Secret ⊑ L₃      // input
L₃ ⊑ L₁          // assign (x := ...)
Public ⊑ L₁      // assign (x := ...)
Public ⊑ L₄      // var (x)
L₁ ⊑ L₄          // var (x)
L₄ ⊑ L₅          // binop (x <= 23)
Public ⊑ L₅      // binop (x <= 23)
L₅ ⊑ L₂          // assign (y := ...)
Public ⊑ L₂      // assign (y := ...)
Public ⊑ L₆      // var (y)
L₂ ⊑ L₆          // var (y)
Public ⊑ Public  // output y
L₆ ⊑ Public      // output y

From these constraints, the graph shown in fail03_constraint_graph.png can be made.
By recursively getting children of Public and Secret, we can determine
all levels which are subsets (really ⊑) of Public and Secret.  This is BEFORE
we ever consider what the security lattic actually looks like. The resulting
sets are shown below:

Public: [Public, Secret, L₁, L₂, L₃, L₄, L₅, L₆]
Secret: [Secret, L₁, L₂, L₃, L₄, L₅, L₆, Public]

With the sets in hand, we can check to see if this information is
consistent with the security lattice.

For Public, we know that for all security levels l, Public ⊑ l, so everything
in Public's set will ALWAYS be ok.

For Secret, we know that only Secret ⊑ Secret.  However, from the set
derived for Secret above, we can see that we have a constraint that shows
Secret ⊑ Public.  This is not true.  As such, we know that this program
does not typecheck with respect to the security lattice.  If Public
did not exist in this set, then this program would have typechecked ok.

As an aside, we could go backwards at this point and figure out exactly
where the error occurred.  We know that Public was included in this set due
to the edge from L₆ to Public in the constraint graph.  This edge came
from the constraint L₆ ⊑ Public.  This constraint originated with `y`
from the statement `output public y`.  In a real typechecker, we would be
able to use this information to show the user something like:

Error at line 7:
output public y
              ^
`y` is Secret, but output's channel is Public.

...but this is not necessary for this assignment.