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 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 = abs ((s . x) - (s . y)) & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) )
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 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 = abs ((s . x) - (s . y)) & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) )
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 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 = abs ((s . x) - (s . y)) & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) )
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 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 = abs ((s . x) - (s . y)) & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) )
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 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 = abs ((s . x) - (s . y)) & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) ) )
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 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 = abs ((s . x) - (s . y)) & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) )
A5: y <> z by A3, A4;
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 = abs ((s . x) - (s . y)) & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) )
set J = if-then (z lt 0 ),(z *= (- 1));
A6: g complies_with_if_wrt (Funcs X,INT ) \ b,0 by AOFA_000:def 32;
A7: z <> x by A2, A4;
set I = (((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z);
A8: x <> y by A2, A3;

A9: now

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 = abs ((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));
A10: ((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);
A11: 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 A12: ( (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 A6, AOFA_000:def 30;
A13: (. x) . s = s . x by Th22;
A14: (g . (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )),(z *= (- 1))) . y = (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . y by A5, Th31;
A15: (. y) . s = s . y by Th22;
((. x) - (. y)) . s = ((. x) . s) - ((. y) . s) by Def11;
then A16: (g . s,(z := ((. x) - (. y)))) . z = (s . x) - (s . y) by A13, A15, Th26;
A17: ( (g . s,(z := ((. x) - (. y)))) . z < 0 implies (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . b = 1 ) by Th38;
A18: (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . z = (g . s,(z := ((. x) - (. y)))) . z by A1, A4, Th38;
A19: (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;
A20: (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 A7, Th27;
A21: (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 A22: ( (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 A6, AOFA_000:80;
A23: ( (g . s,(z := ((. x) - (. y)))) . z >= 0 implies (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . b = 0 ) by Th38;
A24: (g . s,(z := ((. x) - (. y)))) . y = s . y by A5, Th26;
A25: (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 A1, A3, 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 = abs ((s . x) - (s . y)) ) by A8, A22, A12, A18, A17, A23, A14, A19, A10, A11, A24, A16, A25, A20, A21, Th27, ABSVALUE:def 1; :: thesis: verum

end;

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 = abs ((s . x) - (s . y)) ) ; :: thesis: for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s
deffunc H₁( Element of Funcs X,INT ) -> Element of NAT = IFEQ ($1 . y),0 ,0 ,(IFEQ ($1 . x),0 ,2,(IFEQ ($1 . x),($1 . y),1,(In (max (2 * ($1 . x)),((2 * ($1 . y)) + 1)),NAT )));
defpred S₁[ Element of Funcs X,INT ] means ( $1 . x >= 0 & $1 . y > 0 );
set C = y gt 0 ;
A26: for s being Element of Funcs X,INT st S₁[s] holds
( ( S₁[g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))] implies g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 ) & ( g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 implies S₁[g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))] ) & H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) )

proof

let s be Element of Funcs X,INT ; :: thesis: ( S₁[s] implies ( ( S₁[g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))] implies g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 ) & ( g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 implies S₁[g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))] ) & H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) ) )
assume that
A27: s . x >= 0 and
A28: s . y > 0 ; :: thesis: ( ( S₁[g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))] implies g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 ) & ( g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 implies S₁[g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))] ) & H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) )
reconsider s9 = g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) as Element of Funcs X,INT ;
reconsider s99 = g . s9,(y gt 0 ) as Element of Funcs X,INT ;
A29: s9 . y = abs ((s . x) - (s . y)) by A9;
then reconsider nx = s . x, ny = s . y, nn = s99 . y as Element of NAT by A1, A3, A27, A28, Th38, INT_1:16;
A30: g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 )) = s99 by AOFA_000:def 29;
A31: s99 . x = s9 . x by A1, A2, Th38;
A32: ( s9 . y <= 0 implies s99 . b = 0 ) by Th38;
A33: ( s9 . y > 0 implies s99 . b = 1 ) by Th38;
hence ( S₁[g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))] iff g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 ) by A9, A28, A30, A31, A32, Th2, Th38; :: thesis: H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s)
A34: s9 . x = s . y by A9;
( max (2 * ny),((2 * nn) + 1) = 2 * ny or max (2 * ny),((2 * nn) + 1) = (2 * nn) + 1 ) by XXREAL_0:16;
then A35: H₁(s99) = IFEQ nn,0 ,0 ,(IFEQ ny,0 ,2,(IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1)))) by A31, A34, FUNCT_7:def 1;
(2 * ny) + 1 > 2 * ny by NAT_1:13;
then A36: max (2 * nx),((2 * ny) + 1) > 2 * ny by XXREAL_0:30;
A37: s99 . y = s9 . y by A1, A3, Th38;
( max (2 * nx),((2 * ny) + 1) = 2 * nx or max (2 * nx),((2 * ny) + 1) = (2 * ny) + 1 ) by XXREAL_0:16;
then A38: H₁(s) = IFEQ ny,0 ,0 ,(IFEQ nx,0 ,2,(IFEQ nx,ny,1,(max (2 * nx),((2 * ny) + 1)))) by FUNCT_7:def 1
.= IFEQ nx,0 ,2,(IFEQ nx,ny,1,(max (2 * nx),((2 * ny) + 1))) by A28, FUNCOP_1:def 8 ;

per cases ( nx = ny or nx > ny or ( nx < ny & nx > 0 ) or nx = 0 ) by XXREAL_0:1;

suppose A39: nx = ny ; :: thesis: H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s)

then A40: IFEQ nx,ny,1,(max (2 * nx),((2 * ny) + 1)) = 1 by FUNCOP_1:def 8;
A41: nn = 0 by A37, A29, A39, ABSVALUE:7;
H₁(s) = IFEQ nx,ny,1,(max (2 * nx),((2 * ny) + 1)) by A28, A38, A39, FUNCOP_1:def 8;
hence H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) by A30, A40, A41, FUNCOP_1:def 8; :: thesis: verum

end;

suppose A42: nx > ny ; :: thesis: H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s)

then IFEQ nx,ny,1,(max (2 * nx),((2 * ny) + 1)) = max (2 * nx),((2 * ny) + 1) by FUNCOP_1:def 8;
then A43: H₁(s) = max (2 * nx),((2 * ny) + 1) by A38, A42, FUNCOP_1:def 8;
A44: nx - ny > 0 by A42, XREAL_1:52;
then A45: H₁(s99) = IFEQ ny,0 ,2,(IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1))) by A37, A33, A32, A29, A35, ABSVALUE:def 1, FUNCOP_1:def 8
.= IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1)) by A28, FUNCOP_1:def 8 ;
then A46: ( ny = nn implies H₁(s99) = 1 ) by FUNCOP_1:def 8;
nn = nx - ny by A37, A29, A44, ABSVALUE:def 1;
then nn < nx by A28, XREAL_1:46;
then nn + 1 <= nx by NAT_1:13;
then A47: 2 * (nn + 1) <= 2 * nx by XREAL_1:66;
A48: 1 <= (2 * nn) + 1 by NAT_1:11;
A49: ( ny <> nn implies H₁(s99) = max (2 * ny),((2 * nn) + 1) ) by A45, FUNCOP_1:def 8;
(2 * nn) + 2 = ((2 * nn) + 1) + 1 ;
then (2 * nn) + 1 < 2 * nx by A47, NAT_1:13;
then (2 * nn) + 1 < H₁(s) by A43, XXREAL_0:30;
hence H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) by A30, A36, A43, A46, A49, A48, XXREAL_0:2, XXREAL_0:29; :: thesis: verum

end;

suppose A50: ( nx < ny & nx > 0 ) ; :: thesis: H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s)

A51: - (nx - ny) = ny - nx ;
A52: nx - ny < 0 by A50, XREAL_1:51;
then A53: nn = - (nx - ny) by A37, A29, ABSVALUE:def 1;
then A54: nn < ny by A50, A51, XREAL_1:46;
2 * nn < 2 * ny by A50, A53, A51, XREAL_1:46, XREAL_1:70;
then (2 * nn) + 1 < (2 * ny) + 1 by XREAL_1:8;
then A55: (2 * nn) + 1 < max (2 * nx),((2 * ny) + 1) by XXREAL_0:30;
nn > 0 by A37, A29, A52, A51, ABSVALUE:def 1;
then A56: H₁(s99) = IFEQ ny,0 ,2,(IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1))) by A35, FUNCOP_1:def 8
.= IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1)) by A28, FUNCOP_1:def 8
.= max (2 * ny),((2 * nn) + 1) by A54, FUNCOP_1:def 8 ;
H₁(s) = IFEQ nx,ny,1,(max (2 * nx),((2 * ny) + 1)) by A38, A50, FUNCOP_1:def 8
.= max (2 * nx),((2 * ny) + 1) by A50, FUNCOP_1:def 8 ;
hence H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) by A30, A36, A55, A56, XXREAL_0:29; :: thesis: verum

end;

suppose A57: nx = 0 ; :: thesis: H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s)

then A58: H₁(s) = 2 by A38, FUNCOP_1:def 8;
A59: nn = - (nx - ny) by A28, A37, A29, A57, ABSVALUE:def 1
.= ny by A57 ;
then H₁(s99) = IFEQ ny,0 ,2,(IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1))) by A28, A35, FUNCOP_1:def 8
.= IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1)) by A28, FUNCOP_1:def 8
.= 1 by A59, FUNCOP_1:def 8 ;
hence H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) by A30, A58; :: thesis: verum

end;

end;

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 ;
reconsider s1 = g . s,(y gt 0 ) as Element of Funcs X,INT ;
let n, m be Element of NAT ; :: thesis: ( n = s . x & m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) implies g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s )
assume that
A60: n = s . x and
A61: m = s . y ; :: thesis: ( ( s in (Funcs X,INT ) \ b,0 & not m > 0 ) or ( m > 0 & not s in (Funcs X,INT ) \ b,0 ) or g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s )
assume ( s in (Funcs X,INT ) \ b,0 iff m > 0 ) ; :: thesis: g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s
then A62: ( s in (Funcs X,INT ) \ b,0 iff S₁[s] ) by A60, A61;
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s from AOFA_000:sch 3(A62, A26);
hence g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ; :: thesis: verum
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 ) );