Give definitions for common notation
Add main theorem

- see exercise 3.8 in AoP
- add well-defined mutually recursive functions corollary (tentative)