Description:
-
def EuclidAgl(a,b): if b = 0: return a else: return EuclidAlg(b, a mod b)
- If then lemma
- Euclid’s algorithm, on input EuclidAlg(a, b) for not both 0, always terminates and produces the correct output.theorem
- For every two recursive calls made by EuclidAlg, the first argument a is at least reduced by halved.claim
- Euclid’s algorithm, on input EuclidAlg(a, b) for not both 0, always terminates in time proportional to .theorem