If we take \\( \mathcal{V} \\) to be \\( \textbf{Bool} := (\mathbb{B}, \le_{Bool}, \text{true}, \wedge) \\)

and \\( \mathcal{X}(m, n) := m \le_X n \\), \\( \mathcal{Y}(m, n) := m \le_Y n \\), \\( \Phi(m, n) := m \le_{\Phi} n \\) , then

\[ \mathcal{X}(x' , x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y' ) \le_{Bool} \Phi(x' , y' ) \]

becomes

\[ ( x' \le_X x ) \wedge \Phi(x, y) \wedge ( y \le_Y y' ) \le_{Bool} \Phi(x' , y' ) \]

Which is (almost) the feasibility relation mentioned in the introduction.

\[ \text{ if } x' \le_X x \text{ and } y \le_Y y' \text{ then } \Phi(x, y) \le_{Bool} \Phi(x' , y' ) \]

Does the difference in \\( \le \\) and "then" matter? Is one of them wrong?

I suppose it is the fact that \\( \textbf{Bool} \\) is quantale that makes them equivalent.

Help!

and \\( \mathcal{X}(m, n) := m \le_X n \\), \\( \mathcal{Y}(m, n) := m \le_Y n \\), \\( \Phi(m, n) := m \le_{\Phi} n \\) , then

\[ \mathcal{X}(x' , x) \otimes \Phi(x, y) \otimes \mathcal{Y}(y, y' ) \le_{Bool} \Phi(x' , y' ) \]

becomes

\[ ( x' \le_X x ) \wedge \Phi(x, y) \wedge ( y \le_Y y' ) \le_{Bool} \Phi(x' , y' ) \]

Which is (almost) the feasibility relation mentioned in the introduction.

\[ \text{ if } x' \le_X x \text{ and } y \le_Y y' \text{ then } \Phi(x, y) \le_{Bool} \Phi(x' , y' ) \]

Does the difference in \\( \le \\) and "then" matter? Is one of them wrong?

I suppose it is the fact that \\( \textbf{Bool} \\) is quantale that makes them equivalent.

Help!