Analiza algorytmu Euklidesa

Należy udowodnić że algorytm zawsze kończy obliczenia.

Algorytmiczne aksjomaty liczb naturalnych:

(n1) [math](\forall n) (n+1 \neq 0 ) [/math]

(n2) [math](\forall n)(\forall m)(n+1=m+1 \Rightarrow n=m)[/math]

(n3) [math](\forall n)[m:=0; \mathbf{while}\ m \neq n\ \mathbf{do}\ n:=n+1\ \mathbf{od}](m=n)[/math]

Możemy zdefiniować relację mniejszości

Definicja

[math]x\lty\ \stackrel{df}{\equiv}\ \neg (x=y) \wedge \left[\begin{array}{l} r:=0; \\ \mathbf{while}\ r\neq x \land r \neq y \\ \mathbf{do} \\ \quad r:=r+1 \\ \mathbf{od} \end{array} \right](r=x)[/math]

Definicja

[math]x\leq y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} r:=0; \\ \mathbf{while}\ r\neq x \land r \neq y \\ \mathbf{do} \\ \quad r:=r+1 \\ \mathbf{od} \end{array} \right](r=x)[/math]

oraz operację odejmowania

Definicja

Jeśli [math]y \lt x [/math] to operacja odejmowania jest określona tak

[math]x \stackrel{.}{-}y\ \stackrel{df}{\equiv}\ \left[\begin{array}{l} r:=y;\ q:=0; \\ \mathbf{while}\ r \neq x \ \mathbf{do} \quad r:=r+1;\ q:=q+1 \ \mathbf{od}; \\ \end{array} \right] (wynik = q) [/math]

Lemat (aksjomat Archimedesa)

Jeśli [math] 0\ltn \lt m [/math] to [math] \left[\begin{array}{l} r:=n; \\ \mathbf{while}\ r \lt m \ \mathbf{do} \quad r:=r+n; \ \mathbf{od}; \\ \end{array} \right] (r\gtm) [/math]