Erweiterter Algorithmus von Euklid

Satz: g = gcd (a, b)⇒∃p, q : ap + bq = g

Bsp: 3 = gcd(15, 21), p = ..., q = ... .

Beweis: konstruktiv, (p, q) ausrechnen durch:

egcd :: N -> N -> (Z,Z)
egcd a b = 
    if b == 0 then ( ... , ... )
    else let (d , m) = divMod a b
             (p' , q') = egcd b m
         in  ( ...  , ... )

Beweis für Algorithms:

• Korrektheit nach Konstruktion
• Termination durch Variante: ...