define : term -> thm
(f [] = a) /\ (!h t. CONS h t = k[f,h,t])
(!n. f(2 * n) = a[f,n]) /\ (!n. f(2 * n + 1) = b[f,n])
# define `multifactorial m n = if m = 0 then 1 else if n <= m then n else n * multifactorial m (n - m)`;; val it : thm = |- multifactorial m n = (if m = 0 then 1 else if n <= m then n else n * multifactorial m (n - m))
# define `!n. collatz(n) = if n <= 1 then n else if EVEN(n) then collatz(n DIV 2) else collatz(3 * n + 1)`;;