Add documentation of the encoding of functions (e.g. to the tutorial)

[viper-admin]

Created by @alexanderjsummers on 2019-01-29 14:22

Important points (e.g.):
Recursive calls in function bodies are handled via limited functions,
Calls in function postconditions are not necessarily safe from matching loops.