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 A being IfWhileAlgebra of the generators of G
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 f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
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 A being IfWhileAlgebra of the generators of G
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 f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
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 A being IfWhileAlgebra of the generators of G
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 f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
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 f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
let G be basic GeneratorSystem over S,X,T; :: thesis: for A being IfWhileAlgebra of the generators of G
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 f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
let A be IfWhileAlgebra of the generators of G; :: 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 f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
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 f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
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 f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
let b be pure Element of the generators of G . the bool-sort of S; :: 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 & ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) holds
for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
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 & ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) implies for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n )
assume A1: G is C -supported ; :: thesis: ( for d being Function holds
( not d . b = 0 or not d . x = 1 or not d . y = 2 or not d . m = 3 ) or for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n )
given d being Function such that A2: ( d . b = 0 & d . x = 1 & d . y = 2 & d . m = 3 ) ; :: thesis: for s being Element of C -States the generators of G
for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
let s be Element of C -States the generators of G; :: thesis: for n being Nat st n = (s . I) . m & f in C -Execution (A,b,(\false C)) holds
((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
let n be Nat; :: thesis: ( n = (s . I) . m & f in C -Execution (A,b,(\false C)) implies ((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n )
assume that
A3: n = (s . I) . m and
A4: f in C -Execution (A,b,(\false C)) ; :: thesis: ((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n
set Q = S;
set S = C -States the generators of G;
set W = T;
set g = f;
set T = (\false C) -States ( the generators of G,b);
set s0 = f . (s,(y := ((\1 (T,I)),A)));
A5: f complies_with_if_wrt (\false C) -States ( the generators of G,b) by AOFA_000:def 32;
defpred S₁[ Element of C -States the generators of G] means ($1 . I) . m > 0 ;
set Z = C;
set C = b gt ((@ m),(\0 (T,I)),A);
defpred S₂[ Element of C -States the generators of G] means ( ((s . I) . x) |^ n = (($1 . I) . y) * ((($1 . I) . x) to_power (($1 . I) . m)) & ($1 . I) . m >= 0 );
deffunc H₁( Element of C -States the generators of G) -> Element of NAT = In ((($1 . I) . m),NAT);
set Y = I;
set I = 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));
A6: m <> y by A2;
then A7: ((f . (s,(y := ((\1 (T,I)),A)))) . I) . m = (s . I) . m by A1, A4, Th65;
A8: for s being Element of C -States the generators of G st S₂[s] holds
( S₂[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] & ( f . (s,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) implies S₁[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] ) & ( S₁[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] implies f . (s,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) ) )

proof

let s be Element of C -States the generators of G; :: thesis: ( S₂[s] implies ( S₂[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] & ( f . (s,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) implies S₁[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] ) & ( S₁[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] implies f . (s,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) ) ) )
assume A9: S₂[s] ; :: thesis: ( S₂[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] & ( f . (s,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) implies S₁[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] ) & ( S₁[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] implies f . (s,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) ) )
set s1 = f . (s,(b gt ((@ m),(\0 (T,I)),A)));
A10: ((f . (s,(b gt ((@ m),(\0 (T,I)),A)))) . I) . x = (s . I) . x by A1, A4, Th66;
((f . (s,(b gt ((@ m),(\0 (T,I)),A)))) . I) . m = (s . I) . m by A1, A4, Th66;
hence S₂[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] by A1, A4, A9, A10, Th66; :: thesis: ( f . (s,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) iff S₁[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] )
A11: ( (\0 (T,I)) value_at (C,s) = 0 & (@ m) value_at (C,s) = (s . I) . m ) by Th36, Th61;
then A12: ( (s . I) . m <= 0 implies f . (s,(b gt ((@ m),(\0 (T,I)),A))) nin (\false C) -States ( the generators of G,b) ) by A1, A4, Th66;
( (s . I) . m > 0 implies f . (s,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) ) by A11, A1, A4, Th66;
hence ( f . (s,(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) iff S₁[f . (s,(b gt ((@ m),(\0 (T,I)),A)))] ) by A1, A4, A12, Th66; :: thesis: verum

end;

A13: ((f . (s,(y := ((\1 (T,I)),A)))) . I) . y = (\1 (T,I)) value_at (C,s) by A1, A4, Th65
.= 1 by Th37 ;
set fs = f . ((f . (s,(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))))));
set s1 = f . ((f . (s,(y := ((\1 (T,I)),A)))),(b gt ((@ m),(\0 (T,I)),A)));
A14: (((f . ((f . (s,(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))))))) . I) . x) to_power 0 = 1 by POWER:24;
A15: m <> x by A2;
A16: 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 A17: (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) )
A18: H₁(s) = (s . I) . m by A17, 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)));
A19: 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;
A20: ( (\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 & (@ 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 ) by Th36, Th61;
then A21: ( ((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 implies 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))) nin (\false C) -States ( the generators of G,b) ) by A1, A4, Th66;
( ((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 implies 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) ) by A20, A1, A4, Th66;
hence ( 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, A19, A1, A4, 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)));
A22: ( 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 A5;
A23: ( (@ 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 & (\2 (T,I)) value_at (C,(f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A))))))) = 2 ) by Th61, 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 A24: ((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 A1, A4, A15, Th65
.= ((@ m) div (\2 (T,I))) value_at (C,(f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A))))))) by A1, A4, 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 A23, AOFA_A00:55
.= (((f . (s,((@ m) is_odd (b,A)))) . I) . m) div 2 by A1, A4, A6, A22, Th65, AOFA_000:def 28
.= ((s . I) . m) div 2 by A1, A4, Th67 ;
A25: ((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, A4, 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 A17, A24, 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 A17, A25, A19, A24, A18, INT_1:56; :: thesis: verum

end;

set q = s;
A26: x <> y by A2;
A27: for s being Element of C -States the generators of G st S₂[s] & s in (\false C) -States ( the generators of G,b) & 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))))]

proof

let s be Element of C -States the generators of G; :: thesis: ( S₂[s] & s in (\false C) -States ( the generators of G,b) & 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))))] )
assume that
A28: S₂[s] and
s in (\false C) -States ( the generators of G,b) and
S₁[s] ; :: 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))))]
reconsider sm = (s . I) . m as Element of NAT by A28, INT_1:3;
(s . I) . m = ((sm div 2) * 2) + (sm mod 2) by NEWTON:66;
then A29: ((s . I) . x) |^ n = ((s . I) . y) * ((((s . I) . x) to_power ((sm div 2) * 2)) * (((s . I) . x) to_power (sm mod 2))) by A28, FIB_NUM2:5
.= (((s . I) . y) * (((s . I) . x) to_power (sm mod 2))) * (((s . I) . x) to_power ((sm div 2) * 2))
.= (((s . I) . y) * (((s . I) . x) to_power (sm mod 2))) * ((((s . I) . x) to_power 2) to_power (sm div 2)) by NEWTON:9
.= (((s . I) . y) * (((s . I) . x) to_power (sm mod 2))) * ((((s . I) . x) * ((s . I) . x)) to_power (sm div 2)) by NEWTON:81 ;
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 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)));
A30: ( 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 A5;
A31: ((f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)))) . I) . x = ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))) . I) . x by A1, A4, A15, Th65
.= ((f . (s,((@ m) is_odd (b,A)))) . I) . x by A1, A4, A26, A30, Th65, AOFA_000:def 28 ;
A32: ((f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)))) . I) . y = ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))) . I) . y by A1, A4, A6, Th65;
A33: ((f . (s,((@ m) is_odd (b,A)))) . I) . y = (s . I) . y by A1, A4, Th67;
A34: ((f . (s,((@ m) is_odd (b,A)))) . I) . x = (s . I) . x by A1, A4, Th67;
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 A35: 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 A36: ((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) . y = ((f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)))) . I) . y by A1, A4, A26, Th65;
A37: sm div 2 = ((s . I) . m) div 2 ;

A38: now :: thesis: ((s . I) . y) * (((s . I) . x) to_power (sm mod 2)) = ((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) . y

A39: (@ m) value_at (C,s) = (s . I) . m by Th61;
then A40: ((f . (s,((@ m) is_odd (b,A)))) . the bool-sort of S) . b = ((s . I) . m) mod 2 by A1, A4, Th67;

per cases ( ((f . (s,((@ m) is_odd (b,A)))) . the bool-sort of S) . b = FALSE or ((f . (s,((@ m) is_odd (b,A)))) . the bool-sort of S) . b = TRUE ) by A37, A40, NAT_D:12;

suppose A41: ((f . (s,((@ m) is_odd (b,A)))) . the bool-sort of S) . b = FALSE ; :: thesis: ((s . I) . y) * (((s . I) . x) to_power (sm mod 2)) = ((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) . y

( f . (s,((@ m) is_odd (b,A))) is ManySortedFunction of the generators of G, the Sorts of C & \false C = FALSE ) by Th10, AOFA_A00:48;
then f . (s,((@ m) is_odd (b,A))) nin (\false C) -States ( the generators of G,b) by A41, AOFA_A00:def 20;
then f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A))))) = f . ((f . (s,((@ m) is_odd (b,A)))),(EmptyIns A)) by A5;
then A42: ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))) . I) . y = ((f . (s,((@ m) is_odd (b,A)))) . I) . y by AOFA_000:def 28;
A43: ((s . I) . y) * 1 = (s . I) . y ;
((s . I) . x) to_power 0 = 1 by POWER:24;
hence ((s . I) . y) * (((s . I) . x) to_power (sm mod 2)) = ((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) . y by A1, A4, A39, A36, A32, A33, A41, A42, A43, Th67; :: thesis: verum

end;

suppose A44: ((f . (s,((@ m) is_odd (b,A)))) . the bool-sort of S) . b = TRUE ; :: thesis: ((s . I) . y) * (((s . I) . x) to_power (sm mod 2)) = ((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) . y

A45: ( (@ y) value_at (C,(f . (s,((@ m) is_odd (b,A))))) = ((f . (s,((@ m) is_odd (b,A)))) . I) . y & (@ x) value_at (C,(f . (s,((@ m) is_odd (b,A))))) = ((f . (s,((@ m) is_odd (b,A)))) . I) . x ) by Th61;
( f . (s,((@ m) is_odd (b,A))) is ManySortedFunction of the generators of G, the Sorts of C & \false C = FALSE ) by Th10, AOFA_A00:48;
then f . (s,((@ m) is_odd (b,A))) in (\false C) -States ( the generators of G,b) by A44, AOFA_A00:def 20;
then 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))) by A5;
then A46: ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))) . I) . y = ((@ y) * (@ x)) value_at (C,(f . (s,((@ m) is_odd (b,A))))) by A1, A4, Th65
.= ((@ y) value_at (C,(f . (s,((@ m) is_odd (b,A)))))) * ((@ x) value_at (C,(f . (s,((@ m) is_odd (b,A)))))) by Th42
.= (((f . (s,((@ m) is_odd (b,A)))) . I) . y) * (((f . (s,((@ m) is_odd (b,A)))) . I) . x) by A45, AOFA_A00:55 ;
( ((s . I) . x) to_power 1 = (s . I) . x & (@ m) value_at (C,s) = (s . I) . m ) by Th61, POWER:25;
hence ((s . I) . y) * (((s . I) . x) to_power (sm mod 2)) = ((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) . y by A1, A4, A34, A36, A32, A33, A44, A46, Th67; :: thesis: verum

end;

end;

end;

A47: ( (@ 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 & (\2 (T,I)) value_at (C,(f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A))))))) = 2 ) by Th61, Th40;
A48: ((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 A1, A4, A15, A35, Th65
.= ((@ m) div (\2 (T,I))) value_at (C,(f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A))))))) by A1, A4, 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 A47, AOFA_A00:55
.= (((f . (s,((@ m) is_odd (b,A)))) . I) . m) div 2 by A1, A4, A6, A30, Th65, AOFA_000:def 28
.= ((s . I) . m) div 2 by A1, A4, Th67 ;
A49: (@ x) value_at (C,(f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A))))) = ((f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)))) . I) . x by Th61;
((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) . x = ((@ x) * (@ x)) value_at (C,(f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A))))) by A1, A4, A35, Th65
.= ((@ x) 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) value_at (C,(f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)))))) by Th42
.= (((f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)))) . I) . x) * (((f . ((f . (s,(if-then (((@ m) is_odd (b,A)),(y := (((@ y) * (@ x)),A)))))),(m := (((@ m) div (\2 (T,I))),A)))) . I) . x) by A49, AOFA_A00:55 ;
hence 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))))] by A48, A29, A31, A34, A38; :: thesis: verum

end;

( (@ m) value_at (C,(f . (s,(y := ((\1 (T,I)),A))))) = ((f . (s,(y := ((\1 (T,I)),A)))) . I) . m & (\0 (T,I)) value_at (C,(f . (s,(y := ((\1 (T,I)),A))))) = 0 & ((f . ((f . (s,(y := ((\1 (T,I)),A)))),(b gt ((@ m),(\0 (T,I)),A)))) . I) . m = ((f . (s,(y := ((\1 (T,I)),A)))) . I) . m ) by A1, A4, Th36, Th61, Th66;
then A50: ( f . ((f . (s,(y := ((\1 (T,I)),A)))),(b gt ((@ m),(\0 (T,I)),A))) in (\false C) -States ( the generators of G,b) iff S₁[f . ((f . (s,(y := ((\1 (T,I)),A)))),(b gt ((@ m),(\0 (T,I)),A)))] ) by A1, A4, Th66;
A51: 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 . ((f . (s,(y := ((\1 (T,I)),A)))),(b gt ((@ m),(\0 (T,I)),A))) from AOFA_000:sch 3(A50, A16);
((f . (s,(y := ((\1 (T,I)),A)))) . I) . x = (s . I) . x by A1, A4, A26, Th65;
then A52: S₂[f . (s,(y := ((\1 (T,I)),A)))] by A3, A7, A13, POWER:41;
A53: ( S₂[f . ((f . (s,(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))))))] & not S₁[f . ((f . (s,(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))))))] ) from AOFA_000:sch 5(A52, A51, A27, A8);
then ((f . ((f . (s,(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))))))) . I) . m = 0 ;
hence ((f . (s,((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)))))))) . I) . y = ((s . I) . x) |^ n by A53, A14, AOFA_000:def 29; :: thesis: verum