Def  f{i}(x) == if i=0 x else f(f{i-1}(x)) fi  (recursive)

is mentioned by

Thm*  InvFuns(A;A;f;g)  (i:. InvFuns(A;A;f{i};g{i}))	[compose_iter_inverses]
Thm*  Bij(A; A; f)  (i:. Bij(A; A; f{i}))	[compose_iter_bijection]
Thm*  Surj(A; A; f)  (i:. Surj(A; A; f{i}))	[compose_iter_surjection]
Thm*  f:(A inj A), i:. f{i}  A inj A	[compose_iter_injection2]
Thm*  k:, f:(k inj k). i:. f{i} = Id  kk	[iter_perm_cycles_uniform2]
Thm*  k:, f:(k inj k). i:. u:k. f{i}(u) = u	[iter_perm_cycles_uniform]
Thm*  k:, f:(k inj k), u:k. i:. f{i}(u) = u	[compose_iter_inj_cycles]
Thm*  Inj(A; A; f)  (i:. Inj(A; A; f{i}))	[compose_iter_injection]
Thm*  f:(AA), i:. f{i} = f{i-1} o f	[compose_iter_pos_comp2]
Thm*  f:(AA), i:, x:A. f{i}(x) = f{i-1}(f(x))	[compose_iter_pos2]
Thm*  x:A, f:(AA), i,j:. f{i}{j}(x) = f{ij}(x)	[compose_iter_prod2]
Thm*  x:A, f:(AA), i,j,k:. k = ij  f{i}{j}(x) = f{k}(x)  A	[compose_iter_prod]
Thm*  f:(AA), k:, i:{0...k}. f{k} = f{i} o f{k-i}	[compose_iter_sum_comp_rw]
Thm*  x:A, f:(AA), k:, i:{0...k}. f{k}(x) = f{i}(f{k-i}(x))	[compose_iter_sum_rw]
Thm*  f:(AA), i,j,k:. k = i+j  f{i} o f{j} = f{k}	[compose_iter_sum_comp]
Thm*  x:A, f:(AA), i,j,k:. k = i+j  f{i}(f{j}(x)) = f{k}(x)	[compose_iter_sum]
Thm*  i:. Id{i} = Id  AA	[compose_iter_id]
Thm*  f:(AA), i:. f{i} = f o f{i-1}	[compose_iter_pos_comp]
Thm*  f:(AA), u:A. f(u) = u  (i:. f{i}(u) = u)	[compose_iter_point_id]
Thm*  f:(AA), i:, x:A. f{i}(x) = f(f{i-1}(x))	[compose_iter_pos]
Thm*  f:(AA). f{1} = f	[compose_iter_once]
Thm*  f:(AA). f{0} = Id	[compose_iter_zero_id]
Thm*  f:(AA), x:A. f{0}(x) = x	[compose_iter_zero]
Def  nat_to_nat_pair(i) == next_nat_pair{i}(<0,0>)	[nat_to_nat_pair]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html