I'm reading this article on a GCD algorithm described by Dijkstra: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD316.4.html
I'm looking at program 1. In particular I'm trying to understand the proof that the loop terminates. Here is program 1 (my notation is slightly different than the one in the article):
function GCD(a,b) while a != b if a > b a = a - b else b = b - a return a
I get that max(a,b) at loop n is strictly greater than max(a,b) at loop n+1. Since a and b are integers greater than 0 it follows that max(a,b) is always greater than 0. This implies a lower bound. Therefore the while loop must terminate.
Is my understanding correct?