Lambda Calculus Xor How do you prove $\mathsf{xor} \, \mathsf{True}\, \mathsf{True}$ is false in lambda calculus using call-by-value reduction.
This is the approach I tried but it is not working:
$$\mathsf{xor} \equiv \lambda xy.x(y F T) y$$
$$\mathsf{xor} \, T T \equiv (\lambda xy.x(y F T)y) T 
T$$
$$\mathsf{xor}\, T T \equiv (\lambda xy.x(y (\lambda x y.y) (\lambda x y.x))y) T 
T$$
Then by beta reduction of leftmost inner
$$\mathsf{xor}\, T T \equiv (\lambda xy.x(y (\lambda y.y) )y) T 
T$$
But I feel there is a mistake somewhere as the steps above did not lead me to the expected answer.

You are mistaken. The subterm $yFT$ does not contain any $\beta$-redex. Indeed, every term of the form $MNL$ must be read as $(MN)L$, and not as $M(NL)$ (technically, the application is said to be left-associative).
This means that $yFT = (yF)T = (y (\lambda xy.y))\lambda xy.x$ and so there is no $\beta$-redex to fire.
Therefore, in the term $\mathsf{xor}\, T T = (\lambda xy.x(y (\lambda x y.y) (\lambda x y.x))y) T T$ there is only one $\beta$-redex, made up of the subterm from the first occurrence of $\lambda x$ to the first occurrence of $T$.
You can easily see that the leftmost-innermost reduction from $\mathsf{xor}\, T T $ yields $F$, as expected.
