CWS paper

[Stephen Weeks]

I'm a bit confused by your analysis.  Here's what I understand after the latest
modification.

RCont = Func U Jump U {bot}
REnv = Func -> RCont

Here is your latest definition of <=l, which is a reflexive, transitive binary
relation on RCont.

> bot <=l l' <=l l   forall l' in Label

I'm afraid I don't understand what this means.  Where is "l" quantified?  As
best as I can make out, this says that every label is <=l every other label.
I.E. the relation is pretty trivial.

Can you define <=l again for me?

Do you mean for <=l to be a partial order?