let x, y be Element of INT ; :: thesis: ex g, w, q, t, a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
defpred S1[ Nat, Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer] means ( $6 = $4 div $5 & $7 = $4 mod $5 & $8 = $5 & $9 = $7 );
A1: for n being Nat
for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1]
proof
let n be Nat; :: thesis: for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1]
let x, y, z, w be Element of INT ; :: thesis: ex x1, y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1]
reconsider x1 = z div w as Element of INT by INT_1:def 2;
reconsider y1 = z mod w as Element of INT by INT_1:def 2;
set z1 = w;
set w1 = y1;
take x1 ; :: thesis: ex y1, z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1]
take y1 ; :: thesis: ex z1, w1 being Element of INT st S1[n,x,y,z,w,x1,y1,z1,w1]
take w ; :: thesis: ex w1 being Element of INT st S1[n,x,y,z,w,x1,y1,w,w1]
take y1 ; :: thesis: S1[n,x,y,z,w,x1,y1,w,y1]
thus S1[n,x,y,z,w,x1,y1,w,y1] ; :: thesis: verum
end;
reconsider i1 = 1 as Element of INT by INT_1:def 2;
reconsider i0 = 0 as Element of INT by INT_1:def 2;
consider q, t, g, w being sequence of INT such that
A2: ( q . 0 = i0 & t . 0 = i0 & g . 0 = x & w . 0 = y & ( for i being Nat holds S1[i,q . i,t . i,g . i,w . i,q . (i + 1),t . (i + 1),g . (i + 1),w . (i + 1)] ) ) from NTALGO_1:sch 1(A1);
 defpred S2[ Nat, Integer, Integer, Integer, Integer, Integer, Integer, Integer, Integer] means ( $6 = $4 & $7 = $5 & $8 = $2 - ((q . ($1 + 1)) * $4) & $9 = $3 - ((q . ($1 + 1)) * $5) );
A3: for n being Nat
for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S2[n,x,y,z,w,x1,y1,z1,w1]
proof
let n be Nat; :: thesis: for x, y, z, w being Element of INT ex x1, y1, z1, w1 being Element of INT st S2[n,x,y,z,w,x1,y1,z1,w1]
let x, y, z, w be Element of INT ; :: thesis: ex x1, y1, z1, w1 being Element of INT st S2[n,x,y,z,w,x1,y1,z1,w1]
reconsider qn1 = q . (n + 1) as Element of INT ;
set x1 = z;
set y1 = w;
reconsider z1 = x - ((q . (n + 1)) * z) as Element of INT by INT_1:def 2;
reconsider w1 = y - ((q . (n + 1)) * w) as Element of INT by INT_1:def 2;
take z ; :: thesis: ex y1, z1, w1 being Element of INT st S2[n,x,y,z,w,z,y1,z1,w1]
take w ; :: thesis: ex z1, w1 being Element of INT st S2[n,x,y,z,w,z,w,z1,w1]
take z1 ; :: thesis: ex w1 being Element of INT st S2[n,x,y,z,w,z,w,z1,w1]
take w1 ; :: thesis: S2[n,x,y,z,w,z,w,z1,w1]
thus S2[n,x,y,z,w,z,w,z1,w1] ; :: thesis: verum
end;
consider a, b, u, v being sequence of INT such that
A4: ( a . 0 = i1 & b . 0 = i0 & u . 0 = i0 & v . 0 = i1 & ( for i being Nat holds S2[i,a . i,b . i,u . i,v . i,a . (i + 1),b . (i + 1),u . (i + 1),v . (i + 1)] ) ) from NTALGO_1:sch 1(A3);
 take g ; :: thesis: ex w, q, t, a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take w ; :: thesis: ex q, t, a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take q ; :: thesis: ex t, a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take t ; :: thesis: ex a, b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take a ; :: thesis: ex b, v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take b ; :: thesis: ex v, u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take v ; :: thesis: ex u being sequence of INT st
( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
take u ; :: thesis: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) )
thus ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Nat holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) by A2, A4; :: thesis: verum