Def even(n) == if n=0 then true else even(n-1) fi   (recursive)

is mentioned by

Thm* n:. even(n)  (m:. n = 2m  )	[even_exists]
Thm* n:. (even(n)  (m:. n = 2m  )) & (odd(n)  (m:. n = 2m+1  ))	[even_odd_exists]
Thm* n:. even(2n)	[even_double]
Thm* m,n:. even(mn)  even(m)  even(n)	[even_mult]
Thm* m,n:. even(m+n)  (even(m)  even(n))	[even_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