definition by cases
for , such that
Since is a total function (domain is all of ), we see that .
As above, if the functions , as well as the predicates , are primitive recursive, then so is the function defined by cases from the and .
To see this, we first need the following:
If functions are primitive recursive, so is .