DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
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(AAf (i:. Bij(AAf{i}))[compose_iter_bijection]
Thm*  Surj(AAf (i:. Surj(AAf{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:kf{i}(u) = u[iter_perm_cycles_uniform]
Thm*  k:f:(k inj k), u:ki:f{i}(u) = u[compose_iter_inj_cycles]
Thm*  Inj(AAf (i:. Inj(AAf{i}))[compose_iter_injection]
Thm*  f:(AA), i:f{i} = f{i-1} o f[compose_iter_pos_comp2]
Thm*  f:(AA), i:x:Af{i}(x) = f{i-1}(f(x))[compose_iter_pos2]
Thm*  x:Af:(AA), i,j:f{i}{j}(x) = f{ij}(x)[compose_iter_prod2]
Thm*  x:Af:(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:Af:(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:Af:(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:Af(u) = u  (i:f{i}(u) = u)[compose_iter_point_id]
Thm*  f:(AA), i:x:Af{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:Af{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

DiscreteMath Sections DiscrMathExt Doc