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;

A16: now :: thesis: for s being Element of Funcs (X,INT) holds
( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| )

let s be Element of Funcs (X,INT); :: thesis: ( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| )
set s1 = g . (s,(z := ((. x) - (. y))));
set s2 = g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0));
set q = g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))));
set qz = g . ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))),(z *= (- 1)));
A17: ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . z) * (- 1) = - ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . z) ;
set s3 = g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y));
set s4 = g . ((g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))),(y := z));
A18: g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) = g . ((g . (s,(((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)))),(y := z)) by AOFA_000:def 29
.= g . ((g . ((g . (s,((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))))),(x := y))),(y := z)) by AOFA_000:def 29
.= g . ((g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))),(y := z)) by AOFA_000:def 29 ;
( (g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 1 implies g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0)) in (Funcs (X,INT)) \ (b,0) ) ;
then A19: ( (g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 1 implies g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1))))) = g . ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))),(z *= (- 1))) ) by A1;
A20: (. x) . s = s . x by Th22;
A21: (g . ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))),(z *= (- 1)))) . y = (g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . y by A6, Th31;
A22: (. y) . s = s . y by Th22;
((. x) - (. y)) . s = ((. x) . s) - ((. y) . s) by Def11;
then A23: (g . (s,(z := ((. x) - (. y))))) . z = (s . x) - (s . y) by A20, A22, Th26;
A24: ( (g . (s,(z := ((. x) - (. y))))) . z < 0 implies (g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 1 ) by Th38;
A25: (g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . z = (g . (s,(z := ((. x) - (. y))))) . z by A2, A5, Th38;
A26: (g . ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))),(z *= (- 1)))) . z = ((g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . z) * (- 1) by Th31;
A27: (g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))) . z = (g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))) . z by A14, Th27;
A28: (g . ((g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))),(y := z))) . y = (g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))) . z by Th27;
( (g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 0 implies g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0)) nin (Funcs (X,INT)) \ (b,0) ) by Th2;
then A29: ( (g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 0 implies g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1))))) = g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0)) ) by A1, AOFA_000:80;
A30: ( (g . (s,(z := ((. x) - (. y))))) . z >= 0 implies (g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . b = 0 ) by Th38;
A31: (g . (s,(z := ((. x) - (. y))))) . y = s . y by A6, Th26;
A32: (g . ((g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))),(x := y))) . x = (g . ((g . (s,(z := ((. x) - (. y))))),(if-then ((z lt 0),(z *= (- 1)))))) . y by Th27;
(g . ((g . (s,(z := ((. x) - (. y))))),(z lt 0))) . y = (g . (s,(z := ((. x) - (. y))))) . y by A2, A4, Th38;
hence ( (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x = s . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y = |.((s . x) - (s . y)).| ) by A15, A29, A19, A25, A24, A30, A21, A26, A17, A18, A31, A23, A32, A27, A28, Th27, ABSVALUE:def 1; :: thesis: verum

end;

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)))]

proof

let s be Element of Funcs (X,INT); :: thesis: ( S₂[s] & s in (Funcs (X,INT)) \ (b,0) & S₁[s] implies S₂[g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))] )
reconsider s99 = g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z))) as Element of Funcs (X,INT) ;
A34: |.(n gcd m).| = n gcd m by ABSVALUE:def 1;
A35: s99 . y = |.((s . x) - (s . y)).| by A16;
assume A36: S₂[s] ; :: thesis: ( not s in (Funcs (X,INT)) \ (b,0) or not S₁[s] or S₂[g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (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
A37: S₁[s] ; :: thesis: S₂[g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))]
n gcd m divides n9 - m9 by A36, PREPOWER:94;
hence ( n gcd m divides (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x & n gcd m divides (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x > 0 & (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y >= 0 ) by A16, A36, A37, A35, A34, INT_2:16; :: thesis: for c being Nat st c divides (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x & c divides (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y holds
c divides n gcd m
let c be Nat; :: thesis: ( c divides (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x & c divides (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y implies c divides n gcd m )
reconsider c9 = c as Element of NAT by ORDINAL1:def 12;
assume that
A38: c divides (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . x and
A39: c divides (g . (s,((((z := ((. x) - (. y))) \; (if-then ((z lt 0),(z *= (- 1))))) \; (x := y)) \; (y := z)))) . y ; :: thesis: c divides n gcd m
A40: |.c.| = c by ABSVALUE:def 1;
A41: s99 . x = s . y by A16;
c9 divides |.(n9 - m9).| by A16, A39;
then A42: c divides n9 - m9 by A40, INT_2:16;
c divides m9 by A16, A38;
then c divides (n9 - m9) + m9 by A42, WSIERP_1:4;
hence c divides n gcd m by A36, A41, A38; :: thesis: verum

end;

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) ) )

proof

let s be Element of Funcs (X,INT); :: thesis: ( S₂[s] implies ( 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) ) ) )
assume A44: S₂[s] ; :: thesis: ( 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 s9 = g . (s,(y gt 0)) as Element of Funcs (X,INT) ;
A45: s9 . y = s . y by A2, A4, Th38;
s9 . x = s . x by A2, A3, Th38;
hence S₂[g . (s,(y gt 0))] by A44, A45; :: thesis: ( g . (s,(y gt 0)) in (Funcs (X,INT)) \ (b,0) iff S₁[g . (s,(y gt 0))] )
A46: ( 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 S₁[g . (s,(y gt 0))] ) by A44, A46, Th2, Th38; :: thesis: verum

end;

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