f:(T
T), m:(T
).
Thm* (
x:T. m(f(x))
m(x) & (m(f(x)) = m(x) 
f(x) = x))
Thm*
Thm* (
x:T. 
n:. f(f^n(x)) = f^n(x))n,m:, f:(TT). f^n+m = f^n o f^mf:(TT), n:
, x:T. f(f^n-1(x)) = f^n(x)| Rank | Theorem | Name |
| 5 | f:(TT), m:(T).
Thm* ( x:T. m(f(x))m(x) & (m(f(x)) = m(x) f(x) = x))
Thm*
Thm* ( x:T. n:. f(f^n(x)) = f^n(x)) | [iteration_terminates] |
| cites the following: | ||
| 2 | n,m:, f:(TT). f^n+m = f^n o f^m | [fun_exp_add] |
| 4 | f:(TT), n:, x:T. f(f^n-1(x)) = f^n(x) | [fun_exp_add1_sub] |