let A be Euclidean preIfWhileAlgebra; :: thesis: for X being non empty countable set
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs (X,INT)
for n, m being Element of NAT st n = s . x & m = s . y & n > m holds
(g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m
let X be non empty countable set ; :: thesis: for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs (X,INT)
for n, m being Element of NAT st n = s . x & m = s . y & n > m holds
(g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m
let b be Element of X; :: thesis: for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)
for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs (X,INT)
for n, m being Element of NAT st n = s . x & m = s . y & n > m holds
(g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m
let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); :: thesis: for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs (X,INT)
for n, m being Element of NAT st n = s . x & m = s . y & n > m holds
(g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m
set h = g;
set S = Funcs (X,INT);
set T = (Funcs (X,INT)) \ (b,0);
let x, y, z be Variable of g; :: thesis: ( ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) implies for s being Element of Funcs (X,INT)
for n, m being Element of NAT st n = s . x & m = s . y & n > m holds
(g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m )
given d being Function such that A1: d . b = 0 and
A2: d . x = 1 and
A3: d . y = 2 and
A4: d . z = 3 ; :: thesis: for s being Element of Funcs (X,INT)
for n, m being Element of NAT st n = s . x & m = s . y & n > m holds
(g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m
set C = y gt 0;
set I = (((z := x) \; (z %= y)) \; (x := y)) \; (y := z);
let s be Element of Funcs (X,INT); :: thesis: for n, m being Element of NAT st n = s . x & m = s . y & n > m holds
(g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m
reconsider fin = g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))))) as Element of Funcs (X,INT) ;
defpred S1[ Element of Funcs (X,INT)] means ( fin . x divides $1 . x & fin . x divides $1 . y );
A5: for s being Element of Funcs (X,INT) st S1[g . (s,(y gt 0))] holds
S1[s] by A1, A2, A3, Th38;
A6: for s being Element of Funcs (X,INT) st S1[g . ((g . (s,(y gt 0))),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))] & g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) holds
S1[g . (s,(y gt 0))]
proof
let s be Element of Funcs (X,INT); :: thesis: ( S1[g . ((g . (s,(y gt 0))),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))] & g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) implies S1[g . (s,(y gt 0))] )
assume A7: S1[g . ((g . (s,(y gt 0))),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))] ; :: thesis: ( not g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) or S1[g . (s,(y gt 0))] )
reconsider s1 = g . (s,(y gt 0)) as Element of Funcs (X,INT) ;
reconsider s2 = g . (s1,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) as Element of Funcs (X,INT) ;
A8: ( s . y <= 0 implies s1 . b = 0 ) by Th38;
A9: s1 . x = s . x by A1, A2, Th38;
A10: s2 . y = (s1 . x) mod (s1 . y) by A1, A2, A3, A4, Lm1;
A11: s2 . x = s1 . y by A1, A2, A3, A4, Lm1;
A12: s1 . y = s . y by A1, A3, Th38;
assume g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) ; :: thesis: S1[g . (s,(y gt 0))]
then s . x = (((s . x) div (s . y)) * (s2 . x)) + ((s2 . y) * 1) by A9, A12, A8, A11, A10, Th2, NEWTON:66;
hence S1[g . (s,(y gt 0))] by A1, A2, A3, A4, A7, A9, Lm1, WSIERP_1:5; :: thesis: verum
end;
reconsider s1 = g . (s,(y gt 0)) as Element of Funcs (X,INT) ;
A13: s1 . y = s . y by A1, A3, Th38;
A14: ( s . y <= 0 implies s1 . b = 0 ) by Th38;
let n, m be Element of NAT ; :: thesis: ( n = s . x & m = s . y & n > m implies (g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m )
defpred S2[ Element of Funcs (X,INT)] means ( n gcd m divides $1 . x & n gcd m divides $1 . y & $1 . x > $1 . y & $1 . y >= 0 );
defpred S3[ Element of Funcs (X,INT)] means $1 . y > 0 ;
assume that
A15: n = s . x and
A16: m = s . y and
A17: n > m ; :: thesis: (g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m
( s . y > 0 implies s1 . b = 1 ) by Th38;
then ( s1 in (Funcs (X,INT)) \ (b,0) iff m > 0 ) by A16, A14, Th2;
then A18: g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0),g . (s,(y gt 0)) by A1, A2, A3, A4, A16, A13, Lm1;
A19: for s being Element of Funcs (X,INT) st S2[s] & s in (Funcs (X,INT)) \ (b,0) & S3[s] holds
S2[g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))]
proof
let s be Element of Funcs (X,INT); :: thesis: ( S2[s] & s in (Funcs (X,INT)) \ (b,0) & S3[s] implies S2[g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))] )
reconsider s99 = g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) as Element of Funcs (X,INT) ;
assume A20: S2[s] ; :: thesis: ( not s in (Funcs (X,INT)) \ (b,0) or not S3[s] or S2[g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))] )
then reconsider n9 = s . x, m9 = s . y as Element of NAT by INT_1:3;
assume that
s in (Funcs (X,INT)) \ (b,0) and
A21: S3[s] ; :: thesis: S2[g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))]
A22: s99 . x = s . y by A1, A2, A3, A4, Lm1;
A23: s99 . y = (s . x) mod (s . y) by A1, A2, A3, A4, Lm1;
n gcd m divides n9 mod m9 by A20, NAT_D:11;
hence S2[g . (s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))] by A20, A21, A22, A23, NEWTON:65; :: thesis: verum
end;
A24: for s being Element of Funcs (X,INT) st S2[s] holds
( S2[g . (s,(y gt 0))] & ( g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) implies S3[g . (s,(y gt 0))] ) & ( S3[g . (s,(y gt 0))] implies g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) ) )
proof
let s be Element of Funcs (X,INT); :: thesis: ( S2[s] implies ( S2[g . (s,(y gt 0))] & ( g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) implies S3[g . (s,(y gt 0))] ) & ( S3[g . (s,(y gt 0))] implies g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) ) ) )
assume A25: S2[s] ; :: thesis: ( S2[g . (s,(y gt 0))] & ( g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) implies S3[g . (s,(y gt 0))] ) & ( S3[g . (s,(y gt 0))] implies g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) ) )
reconsider s9 = g . (s,(y gt 0)) as Element of Funcs (X,INT) ;
s9 . y = s . y by A1, A3, Th38;
hence S2[g . (s,(y gt 0))] by A1, A2, A25, Th38; :: thesis: ( g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) iff S3[g . (s,(y gt 0))] )
A26: ( s . y <= 0 implies s9 . b = 0 ) by Th38;
( s . y > 0 implies s9 . b = 1 ) by Th38;
hence ( g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) iff S3[g . (s,(y gt 0))] ) by A26, Th2, Th38; :: thesis: verum
end;
A27: S2[s] by A15, A16, A17, NAT_D:def 5;
A28: ( S2[g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))] & not S3[g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))] ) from AOFA_000:sch 5(A27, A18, A19, A24);
 then fin . y = 0 ;
then A29: S1[g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))] by INT_2:12;
S1[s] from AOFA_000:sch 6(A29, A18, A6, A5);
then fin . x divides n gcd m by A15, A16, INT_2:22;
then ( fin . x = n gcd m or fin . x = - (n gcd m) ) by A28, INT_2:11;
hence (g . (s,(while ((y gt 0),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))))) . x = n gcd m by A28; :: thesis: verum