Here I am given an alternative definition for natural numbers.
Like this
$$ LET \ \widehat{\underline{0}} = \lambda x. x $$
$$ LET \ \widehat{\underline{1}} = (\underline{false}, \ \widehat{\underline{0}}) $$
$$ LET \ \widehat{\underline{2}} = (\underline{false}, \ \widehat{\underline{1}}) $$
$$ \vdots $$
$$ LET \ \widehat{\underline{n+1}} = (\underline{false}, \ \widehat{\underline{n}}) $$
$$ \vdots $$
I am given a task to derive $\widehat{\underline{suc}}, \ \widehat{\underline{iszero}}, \ \widehat{\underline{pre}}$ such that
$$ \widehat{\underline{suc}} \ \widehat{\underline{n}} = \widehat{\underline{n+1}} $$
$$ \widehat{\underline{iszero}} \ \widehat{\underline{0}} = \underline{true} $$
$$ \widehat{\underline{iszero}} \ (\widehat{\underline{suc}} \ \widehat{\underline{n}}) = \underline{false} $$
$$ \widehat{\underline{pre}} \ (\widehat{\underline{suc}} \ \widehat{\underline{n}}) = \widehat{\underline{n}} $$
Here's my try:
I came up with:
$$ \widehat{\underline{iszero}} = \lambda n. n \ \underline{true} $$
$$ \widehat{\underline{suc}} = \lambda n. (\underline{false}, n) $$
$$ \widehat{\underline{pre}} = \lambda n. \underline{snd} \ n $$
And here's to show they meet all requirements:
(i) $\widehat{\underline{suc}} \ \widehat{\underline{n}} = \widehat{\underline{n+1}}$
$\widehat{\underline{suc}} \ \widehat{\underline{n}} = (\lambda n. (\underline{false},n))\widehat{\underline{n}} = (\underline{false},\widehat{\underline{n}}) = \widehat{\underline{n+1}}$
(ii) $\widehat{\underline{iszero}} \ \widehat{\underline{0}} = \underline{true}$
$\widehat{\underline{iszero}} \ \widehat{\underline{0}} = (\lambda n. n \ \underline{true}) \widehat{\underline{0}} = \widehat{\underline{0}} \ \underline{true} = (\lambda x. x) \underline{true} = \underline{true}$
(iii) $\widehat{\underline{iszero}} \ (\widehat{\underline{suc}} \ \widehat{\underline{n}}) = \underline{false}$
$\widehat{\underline{iszero}} \ (\widehat{\underline{suc}} \ \widehat{\underline{n}}) = \widehat{\underline{iszero}} \ \widehat{\underline{n+1}} = (\lambda n. n \ \underline{true}) \widehat{\underline{n+1}} = \widehat{\underline{n+1}} \ \underline{true} = (\underline{false}, \widehat{\underline{n}}) \underline{true} = (\lambda f. f \ \underline{false} \ \widehat{\underline{n}}) \underline{true} = \underline{true} \ \underline{false} \ \widehat{\underline{n}} = (\lambda xy. x) \underline{false} \ \widehat{\underline{n}} = (\lambda y. \underline{false}) \widehat{\underline{n}} = \underline{false}$
(iv) $\widehat{\underline{pre}} \ (\widehat{\underline{suc}} \ \widehat{\underline{n}}) = \widehat{\underline{n}}$
$\widehat{\underline{pre}} \ (\widehat{\underline{suc}} \ \widehat{\underline{n}}) = \widehat{\underline{pre}} \ (\widehat{\underline{n+1}}) = (\lambda n. \ \underline{snd} \ n) \widehat{\underline{n+1}} = \underline{snd} \ \widehat{\underline{n+1}} = \underline{snd} \ (\underline{false}, \widehat{\underline{n}}) = \widehat{\underline{n}}$
Here $\underline{snd} \ (a,b) = b$.
Are the steps correct and reasonable? Thanks a bunch!