let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for x, y, m being pure Element of the generators of G . I
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st
( d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for x, y, m being pure Element of the generators of G . I
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st
( d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for x, y, m being pure Element of the generators of G . I
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st
( d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for x, y, m being pure Element of the generators of G . I
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st
( d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
let G be basic GeneratorSystem over S,X,T; :: thesis: for I being integer SortSymbol of S
for x, y, m being pure Element of the generators of G . I
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st
( d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
let I be integer SortSymbol of S; :: thesis: for x, y, m being pure Element of the generators of G . I
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st
( d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
let x, y, m be pure Element of the generators of G . I; :: thesis: for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st
( d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
let b be pure Element of the generators of G . the bool-sort of S; :: thesis: for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st
( d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
let A be elementary IfWhileAlgebra of the generators of G; :: thesis: for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st
( d . x = 1 & d . y = 2 & d . m = 3 ) holds
(y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b); :: thesis: ( G is C -supported & f in C -Execution (A,b,(\false C)) & ex d being Function st
( d . x = 1 & d . y = 2 & d . m = 3 ) implies (y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } )
assume A1: ( G is C -supported & f in C -Execution (A,b,(\false C)) ) ; :: thesis: ( for d being Function holds
( not d . x = 1 or not d . y = 2 or not d . m = 3 ) or (y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } )
set ST = C -States the generators of G;
set TV = (\false C) -States ( the generators of G,b);
set P = { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } ;
given d being Function such that A2: d . x = 1 and
A3: d . y = 2 and
A4: d . m = 3 ; :: thesis: (y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
A5: I <> the bool-sort of S by AOFA_A00:53;
set W = b gt ((@ m),(\0 (T,I)),A);
A6: y := ((\1 (T,I)),A) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } by AOFA_000:107;
deffunc H₁( Element of C -States the generators of G) -> Element of NAT = In ((($1 . I) . m),NAT);
defpred S₁[ Element of C -States the generators of G] means ($1 . I) . m > 0 ;
set K = if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)));
set J = ((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A));
A7: f complies_with_if_wrt (\false C) -States ( the generators of G,b) by AOFA_000:def 32;
A8: { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } is_invariant_wrt b gt ((@ m),(\0 (T,I)),A),f

proof

let s be Element of C -States the generators of G; :: according to AOFA_000:def 39 :: thesis: ( not s in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } or f . (s,(b gt ((@ m),(\0 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } )
assume s in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } ; :: thesis: f . (s,(b gt ((@ m),(\0 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
then A9: ex s1 being Element of C -States the generators of G st
( s = s1 & (s1 . I) . m >= 0 ) ;
((f . (s,(b gt ((@ m),(\0 (T,I)),A)))) . I) . m = (s . I) . m by A1, Th66;
hence f . (s,(b gt ((@ m),(\0 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } by A9; :: thesis: verum

end;

A10: for s being Element of C -States the generators of G st s in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } & f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) holds
f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }

proof

let s be Element of C -States the generators of G; :: thesis: ( s in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } & f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) implies f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } )
assume s in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } ; :: thesis: ( not f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) or f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } )
A11: (\0 (T,I)) value_at (C,(f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))))) = 0 by Th36;
assume f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) ; :: thesis: f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
then (@ m) value_at (C,(f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))))) > (\0 (T,I)) value_at (C,(f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))))) by A1, Th66;
then ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) . I) . m > 0 by A11, Th61;
hence f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } ; :: thesis: verum

end;

A12: m <> y by A4, A3;
A13: { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } is_invariant_wrt y := ((\1 (T,I)),A),f

proof

let s be Element of C -States the generators of G; :: according to AOFA_000:def 39 :: thesis: ( not s in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } or f . (s,(y := ((\1 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } )
assume s in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } ; :: thesis: f . (s,(y := ((\1 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 }
then A14: ex s9 being Element of C -States the generators of G st
( s = s9 & (s9 . I) . m >= 0 ) ;
((f . (s,(y := ((\1 (T,I)),A)))) . I) . m = (s . I) . m by A12, A1, Th65;
hence f . (s,(y := ((\1 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } by A14; :: thesis: verum

end;

A15: m <> x by A4, A2;
A16: for s being Element of C -States the generators of G st f . (s,(b gt ((@ m),(\0 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } holds
f iteration_terminates_for (((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)),f . (s,(b gt ((@ m),(\0 (T,I)),A)))

proof

A17: for s being Element of C -States the generators of G st S₁[s] holds
( ( S₁[f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))] implies f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)))) in (\false C) -States ( the generators of G,b) implies S₁[f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))] ) & H₁(f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))) < H₁(s) )

proof

let s be Element of C -States the generators of G; :: thesis: ( S₁[s] implies ( ( S₁[f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))] implies f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)))) in (\false C) -States ( the generators of G,b) implies S₁[f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))] ) & H₁(f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))) < H₁(s) ) )
assume A18: (s . I) . m > 0 ; :: thesis: ( ( S₁[f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))] implies f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)))) in (\false C) -States ( the generators of G,b) implies S₁[f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))] ) & H₁(f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))) < H₁(s) )
A19: H₁(s) = (s . I) . m by A18, SUBSET_1:def 8, INT_1:3;
set q1 = f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))));
set q0 = f . (s,((@ m) is_odd (b,A)));
set sJ = f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))));
set sC = f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A)));
A20: f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)))) = f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A))) by AOFA_000:def 29;
A21: ( ((f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A)))) . I) . m = ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) . I) . m & (\0 (T,I)) value_at (C,(f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A))))) = 0 ) by Th36, A5, A1, Th65;
A22: ( (@ m) value_at (C,(f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))))) = ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) . I) . m & (\0 (T,I)) value_at (C,(f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))))) = 0 ) by Th36, Th61;
thus ( S₁[f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))] iff f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)))) in (\false C) -States ( the generators of G,b) ) by A21, A20, A22, A1, Th66; :: thesis: H₁(f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))) < H₁(s)
set q2 = f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)));
set q3 = f . ((f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)))),(x := (((@ x) * (@ x)),A)));
A23: ( f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A))))) = f . ((f . (s,((@ m) is_odd (b,A)))),(y := (((@ y) * (@ x)),A))) or f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A))))) = f . ((f . (s,((@ m) is_odd (b,A)))),(EmptyIns A)) ) by A7;
A24: (@ m) value_at (C,(f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A))))))) = ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))) . I) . m by Th61;
A25: (\2 (T,I)) value_at (C,(f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A))))))) = 2 by Th40;
f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A))) = f . (s,((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A)))) by AOFA_000:def 29;
then f . ((f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)))),(x := (((@ x) * (@ x)),A))) = f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))) by AOFA_000:def 29;
then A26: ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) . I) . m = ((f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)))) . I) . m by A15, A1, Th65
.= ((@ m) div (\2 (T,I))) value_at (C,(f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A))))))) by A1, Th65
.= ((@ m) value_at (C,(f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))))) div ((\2 (T,I)) value_at (C,(f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))))) by Th43
.= (((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))) . I) . m) div 2 by A24, A25, AOFA_A00:55
.= (((f . (s,((@ m) is_odd (b,A)))) . I) . m) div 2 by A12, A23, A1, Th65, AOFA_000:def 28
.= ((s . I) . m) div 2 by A5, Th65, A1 ;
A27: ((f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A)))) . I) . m = ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) . I) . m by A1, Th66;
then ((f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A)))) . I) . m in NAT by A18, A26, INT_1:3, INT_1:61;
then H₁(f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A)))) = ((f . ((f . (s,(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))),(b gt ((@ m),(\0 (T,I)),A)))) . I) . m by SUBSET_1:def 8;
hence H₁(f . (s,((((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A))))) < H₁(s) by A18, A27, A20, A26, A19, INT_1:56; :: thesis: verum

end;

let s0 be Element of C -States the generators of G; :: thesis: ( f . (s0,(b gt ((@ m),(\0 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } implies f iteration_terminates_for (((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)),f . (s0,(b gt ((@ m),(\0 (T,I)),A))) )
assume f . (s0,(b gt ((@ m),(\0 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } ; :: thesis: f iteration_terminates_for (((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)),f . (s0,(b gt ((@ m),(\0 (T,I)),A)))
set s1 = f . (s0,(b gt ((@ m),(\0 (T,I)),A)));
A28: ( (s0 . I) . m = (@ m) value_at (C,s0) & (\0 (T,I)) value_at (C,s0) = 0 ) by Th36, Th61;
then A29: ( (s0 . I) . m <= 0 implies f . (s0,(b gt ((@ m),(\0 (T,I)),A))) nin (\false C) -States ( the generators of G,b) ) by A1, Th66;
( (s0 . I) . m > 0 implies f . (s0,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) ) by A28, A1, Th66;
then A30: ( f . (s0,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) iff S₁[f . (s0,(b gt ((@ m),(\0 (T,I)),A)))] ) by A29, A1, Th66;
thus f iteration_terminates_for (((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))) \; (b gt ((@ m),(\0 (T,I)),A)),f . (s0,(b gt ((@ m),(\0 (T,I)),A))) from AOFA_000:sch 3(A30, A17); :: thesis: verum

end;

((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } by AOFA_000:107;
then while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A)))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } by A8, A10, A16, AOFA_000:104, AOFA_000:118;
hence (y := ((\1 (T,I)),A)) \; (while ((b gt ((@ m),(\0 (T,I)),A)),(((if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))) \; (m := (((@ m) div (\2 (T,I))),A))) \; (x := (((@ x) * (@ x)),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . I) . m >= 0 } by A6, A13, AOFA_000:111; :: thesis: verum