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, m being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := 1) \; (while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : s . m >= 0 }
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, m being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := 1) \; (while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : s . m >= 0 }
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, m being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := 1) \; (while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : s . m >= 0 }
let g be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for x, y, m being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := 1) \; (while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : s . m >= 0 }
set S = Funcs X,INT ;
set T = (Funcs X,INT ) \ b,0 ;
let x, y, m be Variable of g; :: thesis: ( ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) implies (y := 1) \; (while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : s . m >= 0 } )
set P = { s where s is Element of Funcs X,INT : s . m >= 0 } ;
given d being Function such that A1: d . b = 0 and
A2: d . x = 1 and
A3: d . y = 2 and
A4: d . m = 3 ; :: thesis: (y := 1) \; (while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : s . m >= 0 }
set C = m gt 0 ;
A5: y := 1 is_terminating_wrt g,{ s where s is Element of Funcs X,INT : s . m >= 0 } by AOFA_000:107;
deffunc H₁( Element of Funcs X,INT ) -> Element of NAT = In ($1 . m),NAT ;
defpred S₁[ Element of Funcs X,INT ] means $1 . m > 0 ;
set I = if-then (m is_odd ),(y *= x);
set J = ((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x);
A6: g complies_with_if_wrt (Funcs X,INT ) \ b,0 by AOFA_000:def 32;
A7: { s where s is Element of Funcs X,INT : s . m >= 0 } is_invariant_wrt m gt 0 ,g

proof

let s be Element of Funcs X,INT ; :: according to AOFA_000:def 39 :: thesis: ( not s in { s where s is Element of Funcs X,INT : s . m >= 0 } or g . s,(m gt 0 ) in { s where s is Element of Funcs X,INT : s . m >= 0 } )
assume s in { s where s is Element of Funcs X,INT : s . m >= 0 } ; :: thesis: g . s,(m gt 0 ) in { s where s is Element of Funcs X,INT : s . m >= 0 }
then A8: ex s9 being Element of Funcs X,INT st
( s = s9 & s9 . m >= 0 ) ;
(g . s,(m gt 0 )) . m = s . m by A1, A4, Th38;
hence g . s,(m gt 0 ) in { s where s is Element of Funcs X,INT : s . m >= 0 } by A8; :: thesis: verum

end;

A9: for s being Element of Funcs X,INT st s in { s where s is Element of Funcs X,INT : s . m >= 0 } & g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 ) in (Funcs X,INT ) \ b,0 holds
g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) in { s where s is Element of Funcs X,INT : s . m >= 0 }

proof

let s be Element of Funcs X,INT ; :: thesis: ( s in { s where s is Element of Funcs X,INT : s . m >= 0 } & g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 ) in (Funcs X,INT ) \ b,0 implies g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) in { s where s is Element of Funcs X,INT : s . m >= 0 } )
assume s in { s where s is Element of Funcs X,INT : s . m >= 0 } ; :: thesis: ( not g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 ) in (Funcs X,INT ) \ b,0 or g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) in { s where s is Element of Funcs X,INT : s . m >= 0 } )
assume g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 ) in (Funcs X,INT ) \ b,0 ; :: thesis: g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) in { s where s is Element of Funcs X,INT : s . m >= 0 }
then (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) . m > 0 by Th40;
hence g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) in { s where s is Element of Funcs X,INT : s . m >= 0 } ; :: thesis: verum

end;

A10: m <> y by A3, A4;
A11: { s where s is Element of Funcs X,INT : s . m >= 0 } is_invariant_wrt y := 1,g

proof

let s be Element of Funcs X,INT ; :: according to AOFA_000:def 39 :: thesis: ( not s in { s where s is Element of Funcs X,INT : s . m >= 0 } or g . s,(y := 1) in { s where s is Element of Funcs X,INT : s . m >= 0 } )
assume s in { s where s is Element of Funcs X,INT : s . m >= 0 } ; :: thesis: g . s,(y := 1) in { s where s is Element of Funcs X,INT : s . m >= 0 }
then A12: ex s9 being Element of Funcs X,INT st
( s = s9 & s9 . m >= 0 ) ;
(g . s,(y := 1)) . m = s . m by A10, Th25;
hence g . s,(y := 1) in { s where s is Element of Funcs X,INT : s . m >= 0 } by A12; :: thesis: verum

end;

A13: m <> x by A2, A4;
A14: for s being Element of Funcs X,INT st g . s,(m gt 0 ) in { s where s is Element of Funcs X,INT : s . m >= 0 } holds
g iteration_terminates_for (((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ),g . s,(m gt 0 )

proof

A15: for s being Element of Funcs X,INT st S₁[s] holds
( ( S₁[g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))] implies g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 )) in (Funcs X,INT ) \ b,0 ) & ( g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 )) in (Funcs X,INT ) \ b,0 implies S₁[g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))] ) & H₁(g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))) < H₁(s) )

proof

let s be Element of Funcs X,INT ; :: thesis: ( S₁[s] implies ( ( S₁[g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))] implies g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 )) in (Funcs X,INT ) \ b,0 ) & ( g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 )) in (Funcs X,INT ) \ b,0 implies S₁[g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))] ) & H₁(g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))) < H₁(s) ) )
assume A16: s . m > 0 ; :: thesis: ( ( S₁[g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))] implies g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 )) in (Funcs X,INT ) \ b,0 ) & ( g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 )) in (Funcs X,INT ) \ b,0 implies S₁[g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))] ) & H₁(g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))) < H₁(s) )
A17: H₁(s) = s . m by A16, FUNCT_7:def 1, INT_1:16;
set q1 = g . s,(if-then (m is_odd ),(y *= x));
set q0 = g . s,(m is_odd );
set sJ = g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x));
set sC = g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 );
A18: g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 )) = g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 ) by AOFA_000:def 29;
A19: ( (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) . m <= 0 implies (g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 )) . b = 0 ) by Th38;
( (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) . m > 0 implies (g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 )) . b = 1 ) by Th38;
hence ( S₁[g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))] iff g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 )) in (Funcs X,INT ) \ b,0 ) by A19, A18, Th2, Th38; :: thesis: H₁(g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))) < H₁(s)
set q2 = g . (g . s,(if-then (m is_odd ),(y *= x))),(m /= 2);
set q3 = g . (g . (g . s,(if-then (m is_odd ),(y *= x))),(m /= 2)),(x *= x);
( g . s,(m is_odd ) in (Funcs X,INT ) \ b,0 or g . s,(m is_odd ) nin (Funcs X,INT ) \ b,0 ) ;
then A20: ( g . s,(if-then (m is_odd ),(y *= x)) = g . (g . s,(m is_odd )),(y *= x) or g . s,(if-then (m is_odd ),(y *= x)) = g . (g . s,(m is_odd )),(EmptyIns A) ) by A6, AOFA_000:def 30;
g . (g . s,(if-then (m is_odd ),(y *= x))),(m /= 2) = g . s,((if-then (m is_odd ),(y *= x)) \; (m /= 2)) by AOFA_000:def 29;
then g . (g . (g . s,(if-then (m is_odd ),(y *= x))),(m /= 2)),(x *= x) = g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) by AOFA_000:def 29;
then A21: (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) . m = (g . (g . s,(if-then (m is_odd ),(y *= x))),(m /= 2)) . m by A13, Th33
.= ((g . s,(if-then (m is_odd ),(y *= x))) . m) div 2 by Th45
.= ((g . s,(m is_odd )) . m) div 2 by A10, A20, Th33, AOFA_000:def 28
.= (s . m) div 2 by A1, A4, Th49 ;
A22: (g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 )) . m = (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) . m by A1, A4, Th38;
then (g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 )) . m in NAT by A16, A21, INT_1:16, INT_1:88;
then H₁(g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 )) = (g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 )) . m by FUNCT_7:def 1;
hence H₁(g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))) < H₁(s) by A16, A22, A18, A21, A17, INT_1:83; :: thesis: verum

end;

let s0 be Element of Funcs X,INT ; :: thesis: ( g . s0,(m gt 0 ) in { s where s is Element of Funcs X,INT : s . m >= 0 } implies g iteration_terminates_for (((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ),g . s0,(m gt 0 ) )
assume g . s0,(m gt 0 ) in { s where s is Element of Funcs X,INT : s . m >= 0 } ; :: thesis: g iteration_terminates_for (((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ),g . s0,(m gt 0 )
set s1 = g . s0,(m gt 0 );
A23: ( s0 . m <= 0 implies (g . s0,(m gt 0 )) . b = 0 ) by Th38;
( s0 . m > 0 implies (g . s0,(m gt 0 )) . b = 1 ) by Th38;
then A24: ( g . s0,(m gt 0 ) in (Funcs X,INT ) \ b,0 iff S₁[g . s0,(m gt 0 )] ) by A23, Th2, Th38;
thus g iteration_terminates_for (((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ),g . s0,(m gt 0 ) from AOFA_000:sch 3(A24, A15); :: thesis: verum

end;

((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : s . m >= 0 } by AOFA_000:107;
then while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : s . m >= 0 } by A7, A9, A14, AOFA_000:104, AOFA_000:118;
hence (y := 1) \; (while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) is_terminating_wrt g,{ s where s is Element of Funcs X,INT : s . m >= 0 } by A5, A11, AOFA_000:111; :: thesis: verum