n,m:
, f:(T
T). f^n+m = f^n o f^mn,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))n:, h,f:(TT). f^n o h = primrec(n;h;i,g. f o g)| Rank | Theorem | Name |
| 2 | n,m:, f:(TT). f^n+m = f^n o f^m | [fun_exp_add] |
| cites the following: | ||
| 0 | 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] |
| 1 | n:, h,f:(TT). f^n o h = primrec(n;h;i,g. f o g) | [fun_exp_compose] |