John, I'm referring to #10, where \\(F(z) = 0 * z\\) is defined. This would suggest \\(z \le z'\\) iff \\(F(z) \le F(z')\\), which is the codiscrete preorder; but this connective step wasn't obvious.