Lambda Calculus – Defining (and checking) Predecessor combinator for Church numerals Studying Lambda Calculus I stumbled upon the problem of defining the  predecessor combinator for Church numerals, i.e., the operation that produces as output the Church numeral that immediately precedes a given Church numeral $c_n$.

Here there is my attempt at defining such combinator, with $\mathbf{K}_p \equiv \lambda bcdeh.deh$ and $c_n \equiv \lambda fx. f^n (x)$. Also, recall that $\mathbf{A}_+ c_n c_m = c_{n+m}$ with $\mathbf{A}_+ \equiv \lambda x_0 y_0 p_0 q_0. x_0 p_0 (y_0 p_0 q_0)$.

Statement: Let $\mathbf{P} \equiv \lambda a py. \mathbf{K}_p  a (py)$. Then, $\mathbf{P} c_{n+1} = c_n$ for every $n \in \mathbb{N}$.
'Proof': Let $c_{n+1}$ be an arbitrary Church numeral. Then, we have
  $$
\begin{align}
\mathbf{P} c_{n+1} &= (\lambda apy.\mathbf{K}_p a p y)c_{n+1}=\\
&= \lambda py.\mathbf{K}_p c_{n+1} py \color{blue}{\overset{?}{=}}\\
&\color{blue}{\overset{?}{=}} \lambda py.\mathbf{K}_p \mathbf{A}_+ c_1 c_n p y = \\
&= \lambda py.c_n p y =\\
&= \lambda py.(\lambda fx.f^n(x)) p y =\\
&= \lambda py.p^{n} (y) =\\
&= c_{n}. \hspace{7cm}\square
\end{align}
$$ 

I am not completely sure about how I handle parentheses in the step with blue equality sign and question mark, since I am not sure if the right expression is the one I wrote or rather $$\lambda py.\mathbf{K}_p c_{n+1} p y = \lambda py.\mathbf{K}_p (\mathbf{A}_+ c_1 c_n ) p y .$$
Of course this is crucial in order to get both if this is a correct definition and if the argument is correct. 
Given what above, the rest should be fine.

Thus, I am really looking forward to know if this is correct and, if not, what's wrong with it.
Any feedback as always will be greatly appreciated.
Thank you for your time.
EDIT PS: I significantly changed my attempt: the old one (that I know see is wrong) can be found below.


Statement: Let $\mathbf{P} \equiv \lambda a py. \mathbf{K}_* ( a (py))$, with $\mathbf{K}_* \equiv \lambda ab.b$ and $c_n \equiv \lambda fx. f^n (x)$. Then, $\mathbf{P} c_{n+1} = c_n$ for every $n \in \mathbb{N}$.
'Attempted Proof': Let $c_{n+1}$ be an arbitrary Church numeral. Then, we have
  $$
\begin{align}
\mathbf{P} c_{n+1} &= (\lambda apy.\mathbf{K}_* (a (py)))c_{n+1}=\\
&= \lambda py.\mathbf{K}_* (c_{n+1} (py))=\\
&= \lambda py.\mathbf{K}_* ((\lambda fx. f^{n+1} (x)) (py))=\\
&= \lambda py.\mathbf{K}_* (p^{n+1} (y)) \color{blue}{\overset{?}{=}}\\
&\color{blue}{\overset{?}{=}} \lambda py.\mathbf{K}_* p^{n+1} (y) =\\
&= \lambda py.\mathbf{K}_* p(p^{n} (y)) =\\
&= \lambda py.(\lambda ab.b) p(p^{n} (y)) =\\
&= \lambda py.p^{n} (y) =\\
&= c_{n}. \hspace{7cm}\square
\end{align}
$$ 
PS: The problem lies in how I handle parentheses in the step with blue equality sign and question mark. This has to be wrong. Also, I had some concerns with the step $$\lambda py.(\lambda ab.b) p(p^{n} (y))= \lambda py.p^{n} (y)$$ 
  since we are handling an expression of the form $p( p (p(\dots(p(y)))\dots))$, that made me feel a bit uncomfortable.
  However, I thought it should be ok, since we define $M\equiv p^n (y)$ and thus we have $$\lambda py.(\lambda ab.b) pM = \lambda py.M = \lambda py.p^{n} (y).$$ 

 A: No, in your reduction sequence there are the several occurrences of the same mistake: you don't respect the parenthesizing in your term. For instance, 
\begin{align}
 (\lambda fx.f^{n+1}(x))(py) \neq p^{n+1}(y)
\end{align}
but 
\begin{align}
 (\lambda fx.f^{n+1}(x))(py) = \lambda x. (py)^{n+1} x.
\end{align}
Another example of this error is in your last edit:
\begin{align}
 \lambda py.\mathbf{K}_p c_{n+1} py \neq \lambda py.\mathbf{K}_p \mathbf{A}_+ c_1 c_n p y
\end{align} 
but 
\begin{align}
 \lambda py.\mathbf{K}_p c_{n+1} py = \lambda py.\mathbf{K}_p (\mathbf{A}_+ c_1 c_n) p y = \lambda py.(\lambda cdeh.deh) p y \\
= \lambda py.(\lambda deh.deh) y = \lambda pyeh.yeh.
\end{align} 
In general, given the terms $M$, $N$ and $P$, the term $M(NP)$ has a completely different meaning from $MNP$: the former means that $M$ is applied to $NP$, the latter means that $MN$ is applied to $P$. Parenthesizing is not associative in the $\lambda$-calculus.
Actually, the definition of the predecessor in the $\lambda$-calculus is quite complicated. You can read here about a funny anecdote concerning Church, Kleene and the discovery of the predecessor combinator. 
Let us define the predecessor combinator ${\bf P} \equiv \lambda nfx. n (\lambda gh.h (g f)) (\lambda u.x) (\lambda u.u)$. Then  we have:
\begin{align}
{\bf P} c_{n+1} &\equiv \big( \lambda nfx. n (\lambda gh.h (g f)) (λu.x) (λu.u) \big)c_{n+1} \\
 &= \lambda fx. c_{n+1} (\lambda gh.h (g f)) (λu.x) (λu.u) \\
 &\equiv \lambda fx. (\lambda f_0x_0.f_0^{n+1}x_0) (\lambda gh.h (g f)) (λu.x) (λu.u) \\
 &= \lambda fx. \big(\lambda x_0.(\lambda gh.h (g f))^{n+1}x_0\big)  (λu.x) (λu.u) \\
 &= \lambda fx. \big(\lambda x_0.(\lambda gh.h (g f))^{n}(\lambda h.h (x_0 f))\big)  (λu.x) (λu.u) \\
 &= \lambda fx. (\lambda gh.h (g f))^{n}(\lambda h.h ((λu.x) f))  (λu.u) \\
 &= \lambda fx. (\lambda gh.h (g f))^{n}(\lambda h.h x)  (λu.u) \\
 &= \lambda fx. (\lambda gh.h (g f))^{n-1}(\lambda h. h ((\lambda h.h x)f))  (λu.u) \\
 &= \lambda fx. (\lambda gh.h (g f))^{n-1}(\lambda h. h (f x))  (λu.u) \\
 &= \lambda fx. (\lambda gh.h (g f))^{n-2}(\lambda h. h (\lambda h. h (f x))f)  (λu.u) \\
 &= \lambda fx. (\lambda gh.h (g f))^{n-2}(\lambda h. h (f^2 x))  (λu.u) \\
 &\dots \\
 &= \lambda fx. (\lambda h. h (f^n x))  (λu.u) \\
 &= \lambda fx. (\lambda u. u) (f^n x) \\
 &= \lambda fx. f^n x \equiv c_n.
\end{align}
Therefore, ${\bf P} c_{n+1} = c_n$ for every $n \in \mathbb{N}$.
