> **Puzzle 209.** Suppose you are trying to fry some eggs and also toast some slices of bread. Describe each process separately as a feasibility relation from \\(\mathbb{N}\\) to \\(\mathbb{N}\\) and then tensor these relations. What is the result?

Michael wrote:

> The exact requirements of frying and toasting is vague...

Yes - I wanted to make people think a little. If you have some number \\(x\\) of eggs, and you want fried eggs, you can get at most \\(x\\) fried eggs. Similarly with toasting slices of bread. I wanted people to translate these well-known facts into feasibility relations.

> Define \\(\Phi(x,x’)\\) to be feasibility for frying where you get one fried egg (x) from one egg (x’). Similarly define \\(\Psi(y,y’)\\) to be feasibility for toasting where you get one toast (y) from one slice of bread (y’).Then :

> \[

\Phi(x,x') =

\begin{cases}

\texttt{true} & \mbox{if } x \leq x' \\\\

\texttt{false} & \mbox{otherwise.}

\end{cases}

\]

> \[

\Psi(y,y') =

\begin{cases}

\texttt{true} & \mbox{if } y \leq y' \\\\

\texttt{false} & \mbox{otherwise.}

\end{cases}

\]

Right! And now we tensor them together...

> \[

(\Phi \otimes \Psi)((x,y),(x',y')) =

\begin{cases}

\texttt{true} & \mbox{if } (x \leq x') \mbox{ and } (y \leq y') \\\\

\texttt{false} & \mbox{otherwise.}

\end{cases}

\]

Right!

Okay, on to the next puzzle.

> **Puzzle 211.** What general mathematical result is Puzzle 209 an example of?

Michael wrote:

> This is just the monoidal preorder law.

Hmm. First of all, the monoidal preorder law isn't a "result", it's just part of a definition. In a monoidal preorder we must have

\[ x \le x' \text{ and } y \le y \text{ implies } x \otimes x' \le y \otimes y' \]

\\(\textbf{Bool}\\) is a monoidal preorder, and the monoidal preorder law for \\(\textbf{Bool}\\) says

\[ x \le x' \text{ and } y \le y \text{ implies } x \wedge x' \le y \wedge y' \]

I believe this law is the key to solving Puzzle 210:

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

But Puzzle 209 is about something more specific.

So, let me give some hints.

In Puzzle 209 the feasibility relation we're calling \\(\Phi\\) is just any old feasibility relation from \\(\mathbb{N}\\) to \\(\mathbb{N}\\): it's a very famous one, with a name! Similarly for \\(\Psi\\)... and similarly for \\(\Phi \otimes \Psi\\). So the answer to Puzzle 209 is a special case of a general result - a result I haven't stated yet. I'm trying to get people to guess this result based on this particular example.

Michael wrote:

> The exact requirements of frying and toasting is vague...

Yes - I wanted to make people think a little. If you have some number \\(x\\) of eggs, and you want fried eggs, you can get at most \\(x\\) fried eggs. Similarly with toasting slices of bread. I wanted people to translate these well-known facts into feasibility relations.

> Define \\(\Phi(x,x’)\\) to be feasibility for frying where you get one fried egg (x) from one egg (x’). Similarly define \\(\Psi(y,y’)\\) to be feasibility for toasting where you get one toast (y) from one slice of bread (y’).Then :

> \[

\Phi(x,x') =

\begin{cases}

\texttt{true} & \mbox{if } x \leq x' \\\\

\texttt{false} & \mbox{otherwise.}

\end{cases}

\]

> \[

\Psi(y,y') =

\begin{cases}

\texttt{true} & \mbox{if } y \leq y' \\\\

\texttt{false} & \mbox{otherwise.}

\end{cases}

\]

Right! And now we tensor them together...

> \[

(\Phi \otimes \Psi)((x,y),(x',y')) =

\begin{cases}

\texttt{true} & \mbox{if } (x \leq x') \mbox{ and } (y \leq y') \\\\

\texttt{false} & \mbox{otherwise.}

\end{cases}

\]

Right!

Okay, on to the next puzzle.

> **Puzzle 211.** What general mathematical result is Puzzle 209 an example of?

Michael wrote:

> This is just the monoidal preorder law.

Hmm. First of all, the monoidal preorder law isn't a "result", it's just part of a definition. In a monoidal preorder we must have

\[ x \le x' \text{ and } y \le y \text{ implies } x \otimes x' \le y \otimes y' \]

\\(\textbf{Bool}\\) is a monoidal preorder, and the monoidal preorder law for \\(\textbf{Bool}\\) says

\[ x \le x' \text{ and } y \le y \text{ implies } x \wedge x' \le y \wedge y' \]

I believe this law is the key to solving Puzzle 210:

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

But Puzzle 209 is about something more specific.

So, let me give some hints.

In Puzzle 209 the feasibility relation we're calling \\(\Phi\\) is just any old feasibility relation from \\(\mathbb{N}\\) to \\(\mathbb{N}\\): it's a very famous one, with a name! Similarly for \\(\Psi\\)... and similarly for \\(\Phi \otimes \Psi\\). So the answer to Puzzle 209 is a special case of a general result - a result I haven't stated yet. I'm trying to get people to guess this result based on this particular example.