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 > 0 holds
(g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (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 > 0 holds
(g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (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 > 0 holds
(g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (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 > 0 holds
(g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))))) . x = n gcd m
set h = g;
set S = Funcs (X,INT);
set T = (Funcs (X,INT)) \ (b,0);
A1: g complies_with_if_wrt (Funcs (X,INT)) \ (b,0) by AOFA_000:def 32;
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 > 0 holds
(g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))))) . x = n gcd m )
given d being Function such that A2: d . b = 0 and
A3: d . x = 1 and
A4: d . y = 2 and
A5: 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 > 0 holds
(g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))))) . x = n gcd m
set C = y gt 0;
let s be Element of Funcs (X,INT); :: thesis: for n, m being Element of NAT st n = s . x & m = s . y & n > 0 holds
(g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))))) . x = n gcd m
A6: y <> z by A4, A5;
reconsider s1 = g . (s,(y gt 0)) as Element of Funcs (X,INT) ;
A7: s1 . x = s . x by A2, A3, Th38;
A8: s1 . y = s . y by A2, A4, Th38;
A9: ( s . y <= 0 implies s1 . b = 0 ) by Th38;
defpred S₁[ Element of Funcs (X,INT)] means ( $1 . x > 0 & $1 . y > 0 );
let n, m be Element of NAT ; :: thesis: ( n = s . x & m = s . y & n > 0 implies (g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))))) . x = n gcd m )
defpred S₂[ Element of Funcs (X,INT)] means ( n gcd m divides $1 . x & n gcd m divides $1 . y & $1 . x > 0 & $1 . y >= 0 & ( for c being Nat st c divides $1 . x & c divides $1 . y holds
c divides n gcd m ) );
set J = if-then ((z lt 0),(z *= (- 1)));
set I = (((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z);
assume that
A10: n = s . x and
A11: m = s . y and
A12: n > 0 ; :: thesis: (g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (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 S₁[s1] ) by A10, A12, A9, Th2, Th38;
then A13: g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)) \; (y gt 0),g . (s,(y gt 0)) by A2, A3, A4, A5, A10, A11, A12, A7, A8, Lm2;
A14: z <> x by A3, A5;
A15: x <> y by A3, A4;
A33: for s being Element of Funcs (X,INT) st S₂[s] & s in (Funcs (X,INT)) \ (b,0) & S₁[s] holds
S₂[g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))] A43: for s being Element of Funcs (X,INT) st S₂[s] holds
( S₂[g . (s,(y gt 0))] & ( g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) implies S₁[g . (s,(y gt 0))] ) & ( S₁[g . (s,(y gt 0))] implies g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) ) ) reconsider fin = g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))))) as Element of Funcs (X,INT) ;
A47: S₂[s] by A10, A11, A12, NAT_D:def 5;
A48: ( S₂[g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))))] & not S₁[g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))))] ) from AOFA_000:sch 5(A47, A13, A33, A43);
then reconsider fn = fin . x as Element of NAT by INT_1:3;
A49: fn divides 0 by NAT_D:6;
fin . y = 0 by A48;
then fn divides n gcd m by A48, A49;
hence (g . (s,(while ((y gt 0),((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))))) . x = n gcd m by A48, NAT_D:5; :: thesis: verum