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 A0: ( d . b = 0 & d . x = 1 & d . y = 2 & 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 ) )
D1: ( x <> y & y <> z & z <> x ) by A0;
Z0: ( g complies_with_if_wrt (Funcs X,INT ) \ b,0 & g complies_with_while_wrt (Funcs X,INT ) \ b,0 ) by AOFA_000:def 32;
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);
set C = y gt 0 ;

IT: 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));
( ( (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 ) & ( (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 ) ) by LemTS;
then Q5: ( ( (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 ) ) & ( (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 Z0, AOFA_000:80, AOFA_000:def 30;
02: ( (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . x = (g . s,(z := ((. x) - (. y)))) . x & (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . y = (g . s,(z := ((. x) - (. y)))) . y & (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . z = (g . s,(z := ((. x) - (. y)))) . z ) by A0, Th015;
04: ( ( (g . s,(z := ((. x) - (. y)))) . z < 0 implies (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . b = 1 ) & ( (g . s,(z := ((. x) - (. y)))) . z >= 0 implies (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . b = 0 ) ) by Th015;
05: ( (g . (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )),(z *= (- 1))) . x = (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . x & (g . (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )),(z *= (- 1))) . y = (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . y & (g . (g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )),(z *= (- 1))) . z = ((g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . z) * (- 1) & ((g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . z) * (- 1) = - ((g . (g . s,(z := ((. x) - (. y)))),(z lt 0 )) . z) ) by D1, Th013;
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);
00: 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 ;
( ((. x) - (. y)) . s = ((. x) . s) - ((. y) . s) & (. x) . s = s . x & (. y) . s = s . y ) by ThE1, DEFminus3;
then 01: ( (g . s,(z := ((. x) - (. y)))) . x = s . x & (g . s,(z := ((. x) - (. y)))) . y = s . y & (g . s,(z := ((. x) - (. y)))) . z = (s . x) - (s . y) ) by D1, Th111;
03: ( (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 & (g . (g . (g . s,(z := ((. x) - (. y)))),(if-then (z lt 0 ),(z *= (- 1)))),(x := y)) . y = (g . (g . s,(z := ((. x) - (. y)))),(if-then (z lt 0 ),(z *= (- 1)))) . y & (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 D1, Th211;
( (g . (g . (g . (g . s,(z := ((. x) - (. y)))),(if-then (z lt 0 ),(z *= (- 1)))),(x := y)),(y := z)) . x = (g . (g . (g . s,(z := ((. x) - (. y)))),(if-then (z lt 0 ),(z *= (- 1)))),(x := y)) . x & (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 D1, Th211;
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 00, 01, 02, 03, 04, 05, Q5, ABSVALUE:def 1; :: thesis: verum

end;

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 ) )
thus ( (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 IT; :: 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
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 A1: ( n = s . x & 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 )
reconsider s1 = g . s,(y gt 0 ) as Element of Funcs X,INT ;
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 ;
defpred S₁[ Element of Funcs X,INT ] means ( $1 . x >= 0 & $1 . y > 0 );
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 ( 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 ) );
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 AB: ( s in (Funcs X,INT ) \ b,0 iff S₁[s] ) by A1;
C: 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 00: ( s . x >= 0 & 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 s' = g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) as Element of Funcs X,INT ;
reconsider s'' = g . s',(y gt 0 ) as Element of Funcs X,INT ;
01: g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 )) = s'' by AOFA_000:def 29;
02: ( s'' . x = s' . x & s'' . y = s' . y & ( s' . y > 0 implies s'' . b = 1 ) & ( s' . y <= 0 implies s'' . b = 0 ) ) by A0, Th015;
04: ( s' . y = abs ((s . x) - (s . y)) & s' . x = s . y ) by IT;
thus ( 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 00, 01, 02, LemTS, IT; :: thesis: H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s)
reconsider nx = s . x, ny = s . y, nn = s'' . y as Element of NAT by 00, 04, A0, Th015, INT_1:16;
( max (2 * ny),((2 * nn) + 1) = 2 * ny or max (2 * ny),((2 * nn) + 1) = (2 * nn) + 1 ) by XXREAL_0:16;
then 03: H₁(s'') = IFEQ nn,0 ,0 ,(IFEQ ny,0 ,2,(IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1)))) by 02, 04, FUNCT_7:def 1;
( max (2 * nx),((2 * ny) + 1) = 2 * nx or max (2 * nx),((2 * ny) + 1) = (2 * ny) + 1 ) by XXREAL_0:16;
then 03': 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 00, FUNCOP_1:def 8 ;
(2 * ny) + 1 > 2 * ny by NAT_1:13;
then 05: max (2 * nx),((2 * ny) + 1) > 2 * ny by XXREAL_0:30;

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

suppose 07: 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 06: ( nx - ny = 0 & H₁(s) = IFEQ nx,ny,1,(max (2 * nx),((2 * ny) + 1)) & IFEQ nx,ny,1,(max (2 * nx),((2 * ny) + 1)) = 1 ) by 00, 03', FUNCOP_1:def 8;
nn = 0 by 02, 04, 07, ABSVALUE:7;
hence H₁(g . s,(((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) by 01, 06, FUNCOP_1:def 8; :: thesis: verum

end;

suppose S: 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 06: ( nx - ny > 0 & nx > 0 ) by XREAL_1:52;
06': IFEQ nx,ny,1,(max (2 * nx),((2 * ny) + 1)) = max (2 * nx),((2 * ny) + 1) by S, FUNCOP_1:def 8;
07': nn = nx - ny by 02, 04, 06, ABSVALUE:def 1;
07: H₁(s) = max (2 * nx),((2 * ny) + 1) by 03', 06', S, FUNCOP_1:def 8;
H₁(s'') = IFEQ ny,0 ,2,(IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1))) by 03, 06, 02, 04, ABSVALUE:def 1, FUNCOP_1:def 8
.= IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1)) by 00, FUNCOP_1:def 8 ;
then 08: ( ( ny = nn implies H₁(s'') = 1 ) & ( ny <> nn implies H₁(s'') = max (2 * ny),((2 * nn) + 1) ) ) by FUNCOP_1:def 8;
nn < nx by 00, 07', XREAL_1:46;
then nn + 1 <= nx by NAT_1:13;
then ( 2 * (nn + 1) <= 2 * nx & 2 * (nn + 1) = (2 * nn) + (2 * 1) & (2 * nn) + 2 = ((2 * nn) + 1) + 1 ) by XREAL_1:66;
then (2 * nn) + 1 < 2 * nx by NAT_1:13;
then ( 1 <= (2 * nn) + 1 & (2 * nn) + 1 < H₁(s) ) by 07, NAT_1:11, 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 01, 08, 05, 07, XXREAL_0:2, XXREAL_0:29; :: thesis: verum

end;

suppose 0A: ( 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)

then nx - ny < 0 by XREAL_1:51;
then ( nn = - (nx - ny) & - (nx - ny) = ny - nx ) by 04, 02, ABSVALUE:def 1;
then 0D: ( nn < ny & nn > 0 ) by 0A, XREAL_1:46, XREAL_1:52;
then 2 * nn < 2 * ny by XREAL_1:70;
then (2 * nn) + 1 < (2 * ny) + 1 by XREAL_1:8;
then 0B: (2 * nn) + 1 < max (2 * nx),((2 * ny) + 1) by XXREAL_0:30;
0C: H₁(s) = IFEQ nx,ny,1,(max (2 * nx),((2 * ny) + 1)) by 03', 0A, FUNCOP_1:def 8
.= max (2 * nx),((2 * ny) + 1) by 0A, FUNCOP_1:def 8 ;
H₁(s'') = IFEQ ny,0 ,2,(IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1))) by 03, 0D, FUNCOP_1:def 8
.= IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1)) by 00, FUNCOP_1:def 8
.= max (2 * ny),((2 * nn) + 1) by 0D, 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 01, 05, 0B, 0C, XXREAL_0:29; :: thesis: verum

end;

suppose 09: 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 0A: H₁(s) = 2 by 03', FUNCOP_1:def 8;
nx - ny < 0 by 00, 09;
then 0B: nn = - (nx - ny) by 04, 02, ABSVALUE:def 1
.= ny by 09 ;
then H₁(s'') = IFEQ ny,0 ,2,(IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1))) by 00, 03, FUNCOP_1:def 8
.= IFEQ ny,nn,1,(max (2 * ny),((2 * nn) + 1)) by 00, FUNCOP_1:def 8
.= 1 by 0B, 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 01, 0A; :: thesis: verum

end;

end;

end;

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(AB, C);
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