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:80;
hence S1[g . s,(y gt 0 )] by A1, A2, A3, A4, A7, A9, Lm1, WSIERP_1:10; :: 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:16;
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:79; :: 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:16;
S1[s] from AOFA_000:sch 6(A29, A18, A6, A5);
then fin . x divides n gcd m by A15, A16, INT_2:33;
then ( fin . x = n gcd m or fin . x = - (n gcd m) ) by A28, INT_2:15;
hence (g . s,(while (y gt 0 ),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = n gcd m by A28; :: thesis: verum
deffunc H1( Element of Funcs X,INT ) -> Element of NAT = In ($1 . y),NAT ;