let a, b be Integer; :: thesis: ex A, B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )
defpred S₁[ Nat, Nat, Nat, Nat, Nat] means ( $4 = $3 & $5 = $2 mod $3 );
A1: for n being Nat
for x, y being Element of NAT ex x1, y1 being Element of NAT st S₁[n,x,y,x1,y1] ;
consider A, B being sequence of NAT such that
A2: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for n being Nat holds S₁[n,A . n,B . n,A . (n + 1),B . (n + 1)] ) ) from RECDEF_2:sch 3(A1);
take A ; :: thesis: ex B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )
take B ; :: thesis: ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )
thus ( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) by A2; :: thesis: verum