Def   == {i:| 0<i }

is mentioned by

Thm*  a,k:. a {k}   Type	[sized_mset_wf4]
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*  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*  f:(AA), i:. f{i} = f o f{i-1}	[compose_iter_pos_comp]
Thm*  f:(AA), i:, x:A. f{i}(x) = f(f{i-1}(x))	[compose_iter_pos]
Thm*  (k:k) ~	[card_nat_vs_nat_tuples]
Thm*  k:. (k) ~	[card_nat_vs_nat_tuple]
Thm*  A:Type, n:, x:A, xs:((n-1)A). [x/ xs]  nA	[seq_cons_wf]
Thm*  k:. k! = k(k-1)!	[factorial_via_intseg_step_rw]
Thm*  0!	[factorial_via_intseg_zero]
Thm*  a,b:. (a inj b) ~ (b((a-1) inj (b-1)))	[card_nsub_inj_vs_lopped]
Thm*  R:(AAProp).  Thm*  (A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y)) Thm*   Thm*  (k:. f:(kA). i,j:k. i<j  R(f(i);f(j)))	[no_finite_model_lemma]
Thm*   ~	[nat_plus_ooc_nat]
Thm*  a:, b:, j:b, f:((a-1) inj {x:b| x = j }). Thm*  (i.if i=a-1 j else f(i) fi)  a inj b	[nsub_inj_fill_typing]
Thm*  a:, b:, f:(a inj b). f  (a-1) inj {x:b| x = f(a-1) }	[nsub_inj_lop_typing]

In prior sections: int 1 int 2 num thy 1 SimpleMulFacts IteratedBinops

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