Boolean function encoded with lambda calculus I have a function $G = \lambda xy.(M(N x y))$, where $M = \lambda zxy.zyx$ and $N = \lambda xy.xyx$, which encodes a boolean function of two arguments $f(x,y)$
By $\beta$-reduction, $G T T$ and $G T F$ (where $T = \lambda xy.x$ and $F = \lambda xy.y$ represent the booleans true and false, respectively) reduce to $\lambda xy. xyx T T$ and $\lambda xy. xyx F T$ and equivalently for the other two combination of booleans.
So basically you could say, that given two arguments $A$ and $B$:
$$
GAB = \lambda xy. xyx B A 
$$
And as far as I know, $\lambda xy. xyx$ defines AND operation.
So, that should mean that I have a logical operation $AND$ which takes the two arguments provided.
However, when I test $G$ using Mikrokosmos with those values I get a table of the logical operation $NAND$
\begin{array}{|c c|c|}
x& y &  f(x,y)\\ 
T & T & F\\
T & F & T\\
F & T & T\\
F & F & T\\
\end{array}
Am I missing something in my $\beta$-reduction or am I misinterpreting the results? Which one is correct?
 A: The result shown by Mikrokosmos is correct. It is not true that $GTT$ $\beta$-reduces to $\lambda xy.xyxTT$. Let us see why.
It is true that $N = \lambda xy.xyx $ represent the logical connective $\mathit{AND}$. Indeed,
\begin{align}
Txy &= (\lambda x'y'.x')xy &&& Fxy &= (\lambda x'y'.y')xy
\\
&\to_\beta (\lambda y'.x)y &&& &\to_\beta (\lambda y'.y')y
\\
&\to_\beta x &&& &\to_\beta y
\end{align}
and so
\begin{align}
NTz &= (\lambda xy.xyx)Tz &&& NFz &= (\lambda xy.xyx)Fz
\\
&\to_\beta (\lambda y.TyT)z &&& &\to_\beta (\lambda y.FyF)z
\\
&\to_\beta TzT &&& &\to_\beta FzF
\\
&\to_\beta^* z &&& &\to_\beta F
\end{align}
Moreover, $M = \lambda zxy.zyx$ represents the logical connective $\mathit{NOT}$. Indeed,
\begin{align}
MT &= (\lambda zxy.zyx)T &&& MF &= (\lambda zxy.zyx)F
\\
&\to_\beta \lambda xy.Tyx &&& &\to_\beta \lambda xy.Fyx
\\
&\to_\beta^* \lambda xy.y &&& &\to_\beta^* \lambda xy.x
\\
&= F &&& &= T
\end{align}
Therefore, $G$ represents the logical connective $\mathit{NAND}$. Indeed,
\begin{align}
GTT &= (\lambda xy. M(Nxy))TT &&& GTF &= (\lambda xy. M(Nxy))TF
\\
&\to_\beta (\lambda y. M(NTy))T &&& &\to_\beta (\lambda y. M(NTy))F
\\
&\to_\beta M(NTT) &&& &\to_\beta M(NTF)
\\
&\to_\beta^* MT &&& &\to_\beta^* MF
\\
&\to_\beta^* F &&& &\to_\beta^* T
\end{align}
\begin{align}
GFT &= (\lambda xy. M(Nxy))FT &&& GFF &= (\lambda xy. M(Nxy))FF
\\
&\to_\beta (\lambda y. M(NFy))T &&& &\to_\beta (\lambda y. M(NFy))F
\\
&\to_\beta M(NFT) &&& &\to_\beta M(NFF)
\\
&\to_\beta^* MF &&& &\to_\beta^* MF
\\
&\to_\beta^* T &&& &\to_\beta^* T
\end{align}
