let a, b be Element of INT ; :: thesis: ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of 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 );
Q1: for n, x, y being Element of NAT ex x1, y1 being Element of NAT st S₁[n,x,y,x1,y1] ;
consider A, B being Function of NAT,NAT such that
P2: ( A . 0 = abs a & B . 0 = abs b & ( for n being Element of NAT holds S₁[n,A . n,B . n,A . (n + 1),B . (n + 1)] ) ) from RECDEF_2:sch 3(Q1);
take A ; :: thesis: ex B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )
take B ; :: thesis: ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) )
thus ( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) ) by P2; :: thesis: verum