-__(__!(a))

__+__(a, a)

not__(__=__(a, a))

not__(__+__(a, a))

not__(__+__(s(a), a))

not__(__<=__(s(n), 0))

__<=__(def__(s(n)), 0)

__=>__(not__(a), b)

__=>__(not__(s(a)), s(b))

__=__(def__(a), b)

__*__(__@@__(1, 0), b(__div__(n, __@@__(1, 0))))

__when__else__(__@@__(1, 0), __<__(n, __@@__(1, 0)),

__*__(__@@__(1, 0), b(__div__(n, __@@__(1, 0)))))

__=__(m(m, n), __when__else__(m, __<=__(m, n), n))

__<=>__(__<__(__div__(i, p), __div__(j, q)),

__<__(__*__(i, q), __*__(j, p)))

__=__(__+__(f, -__(f)), f)

__=__(__+__(__+__(-__(f), -__(f)), -__(f)),

__+__(__+__(-__(f), -__(f)), -__(f)))

__<=__<=__(f(a), f(a), f(a))

__none__but__(f(a), a, f(a))

__one__done(f(a), a)

__-->__(f(a), f(a))

__<=__(s(a), 0)

__#(__#(m))

D__(A__(b))

not__(if__then__else__(if__then__else__(a, b, c), b, c))

__when__else__(a, exists . true, b)