let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being V3() 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 V3() 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) ) ) 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) ) 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))))] ( (@ 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