let s1, s2 be Element of [:INT,INT,INT:]; :: thesis: ( ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Nat 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) ) ) & istop = min* { i where i is Nat : w . i = 0 } & ( 0 <= g . istop implies s1 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies s1 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) & ex g, w, q, t, a, b, v, u being sequence of INT ex istop being Nat 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) ) ) & istop = min* { i where i is Nat : w . i = 0 } & ( 0 <= g . istop implies s2 = [(a . istop),(b . istop),(g . istop)] ) & ( g . istop < 0 implies s2 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) implies s1 = s2 )
assume A6: ex g1, w1, q1, t1, a1, b1, v1, u1 being sequence of INT ex istop1 being Nat st
( a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Nat holds
( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & istop1 = min* { i where i is Nat : w1 . i = 0 } & ( 0 <= g1 . istop1 implies s1 = [(a1 . istop1),(b1 . istop1),(g1 . istop1)] ) & ( g1 . istop1 < 0 implies s1 = [(- (a1 . istop1)),(- (b1 . istop1)),(- (g1 . istop1))] ) ) ; :: thesis: ( for g, w, q, t, a, b, v, u being sequence of INT
for istop being Nat holds
( not a . 0 = 1 or not b . 0 = 0 or not g . 0 = x or not q . 0 = 0 or not u . 0 = 0 or not v . 0 = 1 or not w . 0 = y or not t . 0 = 0 or ex i being Nat st
( 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)) implies not w . (i + 1) = t . (i + 1) ) or not istop = min* { i where i is Nat : w . i = 0 } or ( 0 <= g . istop & not s2 = [(a . istop),(b . istop),(g . istop)] ) or ( g . istop < 0 & not s2 = [(- (a . istop)),(- (b . istop)),(- (g . istop))] ) ) or s1 = s2 )
assume A7: ex g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT ex istop2 being Nat st
( a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Nat holds
( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) & istop2 = min* { i where i is Nat : w2 . i = 0 } & ( 0 <= g2 . istop2 implies s2 = [(a2 . istop2),(b2 . istop2),(g2 . istop2)] ) & ( g2 . istop2 < 0 implies s2 = [(- (a2 . istop2)),(- (b2 . istop2)),(- (g2 . istop2))] ) ) ; :: thesis: s1 = s2
consider g1, w1, q1, t1, a1, b1, v1, u1 being sequence of INT, istop1 being Nat such that
A8: ( a1 . 0 = 1 & b1 . 0 = 0 & g1 . 0 = x & q1 . 0 = 0 & u1 . 0 = 0 & v1 . 0 = 1 & w1 . 0 = y & t1 . 0 = 0 & ( for i being Nat holds
( q1 . (i + 1) = (g1 . i) div (w1 . i) & t1 . (i + 1) = (g1 . i) mod (w1 . i) & a1 . (i + 1) = u1 . i & b1 . (i + 1) = v1 . i & g1 . (i + 1) = w1 . i & u1 . (i + 1) = (a1 . i) - ((q1 . (i + 1)) * (u1 . i)) & v1 . (i + 1) = (b1 . i) - ((q1 . (i + 1)) * (v1 . i)) & w1 . (i + 1) = t1 . (i + 1) ) ) & istop1 = min* { k where k is Nat : w1 . k = 0 } & ( 0 <= g1 . istop1 implies s1 = [(a1 . istop1),(b1 . istop1),(g1 . istop1)] ) & ( g1 . istop1 < 0 implies s1 = [(- (a1 . istop1)),(- (b1 . istop1)),(- (g1 . istop1))] ) ) by A6;
consider g2, w2, q2, t2, a2, b2, v2, u2 being sequence of INT, istop2 being Nat such that
A9: ( a2 . 0 = 1 & b2 . 0 = 0 & g2 . 0 = x & q2 . 0 = 0 & u2 . 0 = 0 & v2 . 0 = 1 & w2 . 0 = y & t2 . 0 = 0 & ( for i being Nat holds
( q2 . (i + 1) = (g2 . i) div (w2 . i) & t2 . (i + 1) = (g2 . i) mod (w2 . i) & a2 . (i + 1) = u2 . i & b2 . (i + 1) = v2 . i & g2 . (i + 1) = w2 . i & u2 . (i + 1) = (a2 . i) - ((q2 . (i + 1)) * (u2 . i)) & v2 . (i + 1) = (b2 . i) - ((q2 . (i + 1)) * (v2 . i)) & w2 . (i + 1) = t2 . (i + 1) ) ) & istop2 = min* { k where k is Nat : w2 . k = 0 } & ( 0 <= g2 . istop2 implies s2 = [(a2 . istop2),(b2 . istop2),(g2 . istop2)] ) & ( g2 . istop2 < 0 implies s2 = [(- (a2 . istop2)),(- (b2 . istop2)),(- (g2 . istop2))] ) ) by A7;
( g1 = g2 & w1 = w2 & a1 = a2 & b1 = b2 ) by A8, A9, Lm7;
hence s1 = s2 by A8, A9; :: thesis: verum