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 \dfrac{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]