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, INT_1:3, SUBSET_1:def 8;
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));
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;
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:3, INT_1:61;
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 SUBSET_1:def 8;
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:56; :: 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