n:
, h,f:(T
T). f^n o h = primrec(n;h;
i,g. f o g)n,m:, b:T, c:((n+m)TT).
Thm* primrec(n+m;b;c) = primrec(n;primrec(m;b;c);
i,t. c(i+m,t))| Theorem | Name |
| n:, h,f:(TT). f^n o h = primrec(n;h;i,g. f o g) | [fun_exp_compose] |
| cites the following: | |
| n,m:, b:T, c:((n+m)TT).
Thm* primrec(n+m;b;c) = primrec(n;primrec(m;b;c); i,t. c(i+m,t)) | [primrec_add] |