scheme :: NAT_D:sch 1
Euklides{ F₁( Nat) -> Nat, F₂() -> Nat, F₃() -> Nat } :

ex n being Nat st
( F₁(n) = F₂() gcd F₃() & F₁((n + 1)) = 0 )

provided

A1: ( 0 < F₃() & F₃() < F₂() ) and
A2: ( F₁(0) = F₂() & F₁(1) = F₃() ) and
A3: for n being Nat holds F₁((n + 2)) = F₁(n) mod F₁((n + 1))