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) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT st n = s . x & m = s . y & n > m & ( 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) \; (z %= y)) \; (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) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT st n = s . x & m = s . y & n > m & ( 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) \; (z %= y)) \; (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) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT st n = s . x & m = s . y & n > m & ( 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) \; (z %= y)) \; (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) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT st n = s . x & m = s . y & n > m & ( 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) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) )
set h = g;
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) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT st n = s . x & m = s . y & n > m & ( 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) \; (z %= y)) \; (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) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT st n = s . x & m = s . y & n > m & ( 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) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) )
D1: ( x <> y & y <> z & z <> x ) by A0;
set I = (((z := x) \; (z %= y)) \; (x := y)) \; (y := z);
set C = y gt 0 ;

IT: now

let s be Element of Funcs X,INT ; :: thesis: ( (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) )
reconsider s1 = g . s,(z := x) as Element of Funcs X,INT ;
reconsider s2 = g . s1,(z %= y) as Element of Funcs X,INT ;
reconsider s3 = g . s2,(x := y) as Element of Funcs X,INT ;
reconsider s4 = g . s3,(y := z) as Element of Funcs X,INT ;
00: g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) = g . (g . s,(((z := x) \; (z %= y)) \; (x := y))),(y := z) by AOFA_000:def 29
.= g . (g . (g . s,((z := x) \; (z %= y))),(x := y)),(y := z) by AOFA_000:def 29
.= s4 by AOFA_000:def 29 ;
01: ( s1 . x = s . x & s1 . y = s . y & s1 . z = s . x ) by D1, Th211;
02: ( s2 . x = s1 . x & s2 . y = s1 . y & s2 . z = (s1 . z) mod (s1 . y) ) by D1, Th216;
03: ( s3 . x = s2 . y & s3 . y = s2 . y & s3 . z = s2 . z ) by D1, Th211;
thus ( (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) ) by 00, 01, 02, 03, D1, Th211; :: thesis: verum

end;

let s be Element of Funcs X,INT ; :: thesis: ( (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT st n = s . x & m = s . y & n > m & ( 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) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) )
thus ( (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) ) by IT; :: thesis: for n, m being Element of NAT st n = s . x & m = s . y & n > m & ( 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) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ),s
let n, m be Element of NAT ; :: thesis: ( n = s . x & m = s . y & n > m & ( 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) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ),s )
assume A1: ( n = s . x & m = s . y & n > m ) ; :: 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) \; (z %= y)) \; (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) \; (z %= y)) \; (x := y)) \; (y := z))) as Element of Funcs X,INT ;
defpred S₁[ Element of Funcs X,INT ] means $1 . y > 0 ;
deffunc H₁( Element of Funcs X,INT ) -> Element of NAT = In ($1 . y),NAT ;
defpred S₂[ 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 S₃[ Element of Funcs X,INT ] means ( fin . x divides $1 . x & fin . x divides $1 . y );
assume ( s in (Funcs X,INT ) \ b,0 iff m > 0 ) ; :: thesis: g iteration_terminates_for ((((z := x) \; (z %= y)) \; (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) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))] implies g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 ) & ( g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 implies S₁[g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))] ) & H₁(g . s,(((((z := x) \; (z %= y)) \; (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) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))] implies g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 ) & ( g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 implies S₁[g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))] ) & H₁(g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) ) )
assume 00: s . y > 0 ; :: thesis: ( ( S₁[g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))] implies g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 ) & ( g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 implies S₁[g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))] ) & H₁(g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) )
reconsider s' = g . s,((((z := x) \; (z %= y)) \; (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) \; (z %= y)) \; (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;
hence ( S₁[g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))] iff g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 )) in (Funcs X,INT ) \ b,0 ) by 01, LemTS; :: thesis: H₁(g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s)
s' . y = (s . x) mod (s . y) by IT;
then 03: ( 0 <= s' . y & s' . y < s . y ) by 00, NEWTON:78, NEWTON:79;
then ( H₁(s'') = s' . y & H₁(s) = s . y ) by 02, FUNCT_7:def 1, INT_1:16;
hence H₁(g . s,(((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ))) < H₁(s) by 03, AOFA_000:def 29; :: thesis: verum

end;

g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ),s from AOFA_000:sch 3(AB, C);
hence g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ; :: thesis: verum