decreasing function used to proof termination of a loop
monoton fallende Funktion, die benutzt werden kann, um zu beweisen, dass eine Schleife terminiert
Loop variant