Apparently this expression can be used to calculate the predecessor of a given church numeral:
$\renewcommand{\l}{\lambda}$ $\l n.(n\ \l p . (p.2,\ s p.2)\ (\overline{0},\ \overline{0})).1$
$<tuple>.n$ being the projection onto the $n$th element.
Now, applying this to some number, let's say $3$ I get:
$\l n.(n\ \l p . (p.2,\ s\ p.2)\ (\overline{0},\ \overline{0})).1\ \overline{3}$
$\rightarrow (\overline{3}\ ((\overline{0},\ \overline{0}).2,\ s\ (\overline{0},\ \overline{0}).2)).1$
$\rightarrow (\overline{3}\ (\overline{0},\ \overline{1})).1$
I assume I made some mistake here, because this makes no sense, because the expression is not a tuple, so there can be no projection being applied to it. Well, maybe I just need to unfold the expression further...
$\rightarrow ((\l f. \l x. f(f(f\ x)))\ (\overline{0},\ \overline{1})).1$
$\rightarrow ((\l x. (\overline{0},\ \overline{1})((\overline{0},\ \overline{1})((\overline{0},\ \overline{1})\ x)))\ ).1$
No.. this does not look any better... I can't apply $x$ the the right most/ inner most tuple, no any of the tuples to any other tuple... so... what am I missing here?
The error is where you go from
$$ \lambda n.(n\ \lambda p . (p.2,\ s\ p.2)\ (\overline{0},\ \overline{0})).1\ \overline{3} $$
to
$$ (\overline{3}\ ((\overline{0},\ \overline{0}).2,\ s\ (\overline{0},\ \overline{0}).2)).1\;. $$
In lambda calculus, function application is by convention left-associative, so
$$ \lambda n.(n\ \lambda p . (p.2,\ s\ p.2)\ (\overline{0},\ \overline{0})).1\ \overline{3} $$
is
$$ ((\overline3\ \lambda p . (p.2,\ s\ p.2))\ (\overline{0},\ \overline{0})).1 $$