scheme :: NEWTON:sch 1
Euklides9{ F1( Nat) -> Element of NAT , F2( Nat) -> Element of NAT , F3() -> Element of NAT , F4() -> Element of NAT } :
ex k being Nat st
( F1(k) = F3() gcd F4() & F2(k) = 0 )
provided
A1: 0 < F4() and
A2: F4() < F3() and
A3: F1(0) = F3() and
A4: F2(0) = F4() and
A5: for k being Nat st F2(k) > 0 holds
( F1((k + 1)) = F2(k) & F2((k + 1)) = F1(k) mod F2(k) )