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