Def odd(n) == if n=0 then false else odd(n-1) fi   (recursive)

is mentioned by

Thm* n:. odd(n)  (m:. n = 2m+1  )	[odd_exists]
Thm* n:. (even(n)  (m:. n = 2m  )) & (odd(n)  (m:. n = 2m+1  ))	[even_odd_exists]
Thm* n:. odd(2n+1)	[odd_double]
Thm* m,n:. odd(mn)  odd(m) & odd(n)	[odd_mult]
Thm* m,n:. odd(m+n)  (odd(m)  odd(n))	[odd_add]
Thm* n:. (even(n) & odd(n))	[even_and_odd]
Thm* n:. even(n)  odd(n)	[even_or_odd]
Thm* n:. odd(n)  even(n)	[odd_even]
Thm* n:. even(n)  odd(n)	[even_odd]

In prior sections: hol arithmetic 1

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