Recognizing primitive recursion

Question

I am trying to write a program to recognize if a given lambda calculus expression is primitive recursive. I believe that a general algorithm to do this does not exist, but I am interested in the most general algorithm. This is a subset of the primitive recursive functions in the LC.

Primitive recursion is built up from the following rules: "http://safalra.com/lambda-calculus/partial-recursive-functions"

To outline some of these rules

• (λfx. x) is zero
• (λnfx. f (n f x)) is successor
• etc...

Now in my program I can just recognize these axioms directly. My confusion is what happens when I get to things derived from them. Take the number 5 for example encoded as (λs.(λz.(s (s (s (s (s z))))))). This is the result of applying the the successor function to zero 5 times. But the above expression is not one of the axioms. I believe that the rule set says that the result of primitive recursive functions are also primitive recursive, but I do not see how given one of these results the result can be shown primitive recursive.

What I mean is that given just the encoding of the number 5 how can I show that it is primitive recursive? That is without brute force search building up from the axioms. Also is my method of representing the primitive recursion axioms correct (for suc and zero) or are the axioms not that literal? Thanks!