>**Puzzle 210.** Show that \$$\Phi \otimes \Psi\$$ is really a feasibility relation if \$$\Phi\$$ and \$$\Psi\$$ are feasibility relations.

So we need to prove :
$\text{ if } (x_1',x_2') \le_X (x_1,x_2) \text{ and } (y_1,y_2) \le_Y (y_1',y_2')', \text{ then } (\Phi \otimes \Psi)((x_1,x_2),(y_1,y_2)) \text{ implies } (\Phi \otimes \Psi)((x_1',x_2'),(y_1',y_2'))$

Using monoidal preorder law and reordering, the left side can be written as:
$(x_1' \le_X x_1 \text{ and } y_1 \le_Y y_1') \text{ and } (x_2' \le_X x_2 \text{ and } y_2 \le_Y y_2')$

Using the definition of tensoring, we can write the right side as:
$\Phi(x_1,y_1) \wedge \Psi(x_2,y_2) \text{ implies } \Phi(x_1',y_1') \wedge \Psi(x_2',y_2')$

Which is the same as :
$\Phi(x_1,y_1) \text{ implies } \Phi(x_1',y_1') \wedge \Psi(x_2,y_2) \text{ implies } \Psi(x_2',y_2')$

Collecting common terms from both sides:
$(\text{if } x_1' \le_X x_1 \text{ and } y_1 \le_Y y_1', \text{ then } \Phi(x_1,y_1) \text{ implies } \Phi(x_1',y_1')) \wedge (\text{ if } x_2' \le_X x_2 \text{ and } y_2 \le_Y y_2', \text{ then } \Psi(x_2,y_2) \text{ implies } \Psi(x_2',y_2'))$

This is true since \$$\Phi\$$ and \$$\Psi\$$ are feasibility relations:

$\text{ if } x_1' \le_X x_1 \text{ and } y_1 \le_Y y_1', \text{ then } \Phi(x_1,y_1) \text{ implies } \Phi(x_1',y_1')$
$\text{ if } x_2' \le_X x_2 \text{ and } y_2 \le_Y y_2', \text{ then } \Psi(x_2,y_2) \text{ implies } \Psi(x_2',y_2')$