homelinen

\begin{eqnarray*}
    && (\lambda xyz.xyz)(\lambda x.xx)(\lambda x.x)x \\
    & \to_\beta & (\lambda yz.xyz)[x := \lambda x.xx](\lambda x.x)x \\
    & \equiv & (\lambda yz.(\lambda x.xx)yz)(\lambda x.x)x \\
    & \to_\beta & (\lambda yz.(xx)[ x := y]z)(\lambda x.x)x \\
    & \equiv & (\lambda yz.yyz)(\lambda x.x)x \\
    & \to_\beta & (\lambda z.yy)[ y := \lambda x.x ]x \\
    & \equiv & (\lambda z.(\lambda x.x)(\lambda x.x)z)x \\
    & \to_\beta & (\lambda z.x[x := \lambda x.x]z)x \\
    & \equiv & (\lambda z.(\lambda x.x)z)x \\