let A be Euclidean preIfWhileAlgebra; 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 ; 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; 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); 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; ( 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
; 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); 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);
( 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)))]
;
( 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)
;
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;
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 ; ( 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
; (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);
( 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]
;
( 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]
;
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;
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);
( 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]
;
( 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;
( 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;
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; verum