> using the tool on the page you can prove that 1. the while-loop terminates Not quite. Proving that a while loop terminates is usually done by establishing a

> using the tool on the page you can prove that 1. the while-loop terminates Not quite. Proving that a while loop terminates is usually done by establishing a loop variant - intuitively, a claim that the inputs to the loop become "smaller" in some sense, i.e. closer to some exit condition/base case, with each iteration of the loop. Loop invariants don't suffice on their own.