Def  == {i:| 0i }

is mentioned by

Thm* i:{8...}. m,n:. 3m+5n = i	[stamps]
Thm* (m,n:. 3m+5n = 7)	[stamps_why_8cents]
Thm* i:{8...}. m,n:. 3m+5n = i	[stamps_sfa]
Thm* b:, a:. u,v:. GCD(a;b;ua+vb)	[bezout_ident_n_sfa]
Thm* n:. CoPrime(fib(n),fib(n+1))	[fib_coprime_sfa3]
Thm* n:. CoPrime(fib(n),fib(n+1))	[fib_coprime_sfa2]
Thm* n:. CoPrime(fib(n),fib(n+1))	[fib_coprime_sfa]
Thm* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists_n_sfa]

In prior sections: int 1 bool 1 int 2 num thy 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html