1. The problem statement, all variables and given/known data Here is the program given: Code (Python): # PRE-condition: m and n are positive natural numbers. # POST-condition: returns a tuple of natural numbers (k, l, b) such that k*m = l*n = b, # and if natural number c is a positive multiple of both m and n then b <= c. def g(m, n): a=m b=n k=1 l=1 while a != b: if a < b: a += m k += 1 else: b += n l += 1 return (k, l, b) The question asks to prove g is correct. 2. Relevant equations Iterative Method of Proving Program Correctness 3. The attempt at a solution Now I understand how to prove the correctness of an iterative program, but am confused on how to determine a proper Loop Invariant LI for this proof. I believe the if else condition in the while loop is confusing me, as I'm not sure if I should have two loop invariants or two cases for the LI. Now consider the loop to iterate at least i times. If I take the contents of the if statement ONLY I could easily write a = (1 + i)m and k = i + 1, as a rough start for the LI. Likewise considering the contents of the else statement I have b = (1 + i)n and l = i + 1. Now obviously this isn't true. But with the absence of the if/else statements I think I would know how to proceed. My issue is I don't know how many iterations occur where the if statement executes and how many occur where the else statement occurs. Also trying to relate it to the number of iterations of the loop, and post condition seems tricky. Any advice would be greatly appreciated.