For this example in my text book about program correctness, how would you prove the loop invariant

Example. Prove that the following function terminates: 1 def term ex(x, y) Pre: x and y are natural numbers. a=x b y 5 while a 0 or b 0: ifa>0: else: 10 return x y Proof. Intuitively, the loop terminates because when the loop runs, ei- ther a or b decreases, and will stop when a and b reach o. To make this argument formal, we need the following loop invariant: a,b2 0, whose proof we leave as an exercise. INTRODUCTION TO THE THEORY OF CO The loop variant we define is u = a + b, let us prove the necessary properties for v: In the loop, either a decreases by 1, or b decreases by 1. In either case, v-a + b decreases by 1. Therefore v is decreasing. Since our loop invariant says that a,b 20, we have that v 2 0 as well. Therefore v EN Example. Prove that the following function terminates: 1 def term ex(x, y) Pre: x and y are natural numbers. a=x b y 5 while a 0 or b 0: ifa>0: else: 10 return x y Proof. Intuitively, the loop terminates because when the loop runs, ei- ther a or b decreases, and will stop when a and b reach o. To make this argument formal, we need the following loop invariant: a,b2 0, whose proof we leave as an exercise. INTRODUCTION TO THE THEORY OF CO The loop variant we define is u = a + b, let us prove the necessary properties for v: In the loop, either a decreases by 1, or b decreases by 1. In either case, v-a + b decreases by 1. Therefore v is decreasing. Since our loop invariant says that a,b 20, we have that v 2 0 as well. Therefore v EN