k:
, x,y:
k. (y, x) o (y, x) = (
x.x)n,m:, f:(T
T). f^n+m = f^n o f^mn:, h,f:(TT). f^n o h = primrec(n;h;i,g. f o g)k,m:, f:(km), g:(m).
Thm* increasing(f;k)
increasing(g;m) increasing(g o f;k)x.x;i,g. f o g)is mentioned by
| k:, x,y:k. (y, x) o (y, x) = (x.x) | [flip_inverse] |
| n,m:, f:(TT). f^n+m = f^n o f^m | [fun_exp_add] |
| n:, h,f:(TT). f^n o h = primrec(n;h;i,g. f o g) | [fun_exp_compose] |
| k,m:, f:(km), g:(m).
Thm* increasing(f;k) increasing(g;m) increasing(g o f;k) | [compose_increasing] |
| x.x;i,g. f o g) | [fun_exp] |
In prior sections: fun 1 list 1
Try larger context:
MarkB generic
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html