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
for s being Element of Funcs (X,INT)
for n being Nat st n = s . m holds
(g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n
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
for s being Element of Funcs (X,INT)
for n being Nat st n = s . m holds
(g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n
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
for s being Element of Funcs (X,INT)
for n being Nat st n = s . m holds
(g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n
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
for s being Element of Funcs (X,INT)
for n being Nat st n = s . m holds
(g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n
set S = Funcs (X,INT);
set T = (Funcs (X,INT)) \ (b,0);
A1: g complies_with_if_wrt (Funcs (X,INT)) \ (b,0) by AOFA_000:def 32;
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 for s being Element of Funcs (X,INT)
for n being Nat st n = s . m holds
(g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n )
given d being Function such that A2: d . b = 0 and
A3: d . x = 1 and
A4: d . y = 2 and
A5: d . m = 3 ; :: thesis: for s being Element of Funcs (X,INT)
for n being Nat st n = s . m holds
(g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n
defpred S₁[ Element of Funcs (X,INT)] means $1 . m > 0 ;
set C = m gt 0;
let s be Element of Funcs (X,INT); :: thesis: for n being Nat st n = s . m holds
(g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n
let n be Nat; :: thesis: ( n = s . m implies (g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n )
defpred S₂[ Element of Funcs (X,INT)] means ( (s . x) |^ n = ($1 . y) * (($1 . x) to_power ($1 . m)) & $1 . m >= 0 );
deffunc H₁( Element of Funcs (X,INT)) -> Element of NAT = In (($1 . m),NAT);
set I = if-then ((m is_odd),(y *= x));
set J = ((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x);
set s0 = g . (s,(y := 1));
A6: m <> y by A4, A5;
then A7: (g . (s,(y := 1))) . m = s . m by Th25;
A8: for s being Element of Funcs (X,INT) st S₂[s] holds
( S₂[g . (s,(m gt 0))] & ( g . (s,(m gt 0)) in (Funcs (X,INT)) \ (b,0) implies S₁[g . (s,(m gt 0))] ) & ( S₁[g . (s,(m gt 0))] implies g . (s,(m gt 0)) in (Funcs (X,INT)) \ (b,0) ) )

proof

let s be Element of Funcs (X,INT); :: thesis: ( S₂[s] implies ( S₂[g . (s,(m gt 0))] & ( g . (s,(m gt 0)) in (Funcs (X,INT)) \ (b,0) implies S₁[g . (s,(m gt 0))] ) & ( S₁[g . (s,(m gt 0))] implies g . (s,(m gt 0)) in (Funcs (X,INT)) \ (b,0) ) ) )
assume A9: S₂[s] ; :: thesis: ( S₂[g . (s,(m gt 0))] & ( g . (s,(m gt 0)) in (Funcs (X,INT)) \ (b,0) implies S₁[g . (s,(m gt 0))] ) & ( S₁[g . (s,(m gt 0))] implies g . (s,(m gt 0)) in (Funcs (X,INT)) \ (b,0) ) )
set s1 = g . (s,(m gt 0));
A10: (g . (s,(m gt 0))) . x = s . x by A2, A3, Th38;
(g . (s,(m gt 0))) . m = s . m by A2, A5, Th38;
hence S₂[g . (s,(m gt 0))] by A2, A4, A9, A10, Th38; :: thesis: ( g . (s,(m gt 0)) in (Funcs (X,INT)) \ (b,0) iff S₁[g . (s,(m gt 0))] )
A11: ( s . m <= 0 implies (g . (s,(m gt 0))) . b = 0 ) by Th38;
( s . m > 0 implies (g . (s,(m gt 0))) . b = 1 ) by Th38;
hence ( g . (s,(m gt 0)) in (Funcs (X,INT)) \ (b,0) iff S₁[g . (s,(m gt 0))] ) by A11, Th2, Th38; :: thesis: verum

end;

A12: (g . (s,(y := 1))) . y = 1 by Th25;
set fs = g . ((g . (s,(y := 1))),(while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))));
set s1 = g . ((g . (s,(y := 1))),(m gt 0));
assume A13: n = s . m ; :: thesis: (g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n
A14: ((g . ((g . (s,(y := 1))),(while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))))) . x) to_power 0 = 1 by POWER:24;
A15: m <> x by A3, A5;
A16: 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 A17: 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) )
A18: H₁(s) = s . m by A17, 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));
A19: 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;
A20: ( (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 A20, A19, 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));
A21: ( 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 A1;
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 A22: (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 A15, Th33
.= ((g . (s,(if-then ((m is_odd),(y *= x))))) . m) div 2 by Th45
.= ((g . (s,(m is_odd))) . m) div 2 by A6, A21, Th33, AOFA_000:def 28
.= (s . m) div 2 by A2, A5, Th49 ;
A23: (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 A2, A5, Th38;
then (g . ((g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))),(m gt 0))) . m in NAT by A17, A22, 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 A17, A23, A19, A22, A18, INT_1:56; :: thesis: verum

end;

set q = s;
A24: x <> y by A3, A4;
A25: for s being Element of Funcs (X,INT) st S₂[s] & s in (Funcs (X,INT)) \ (b,0) & S₁[s] holds
S₂[g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))]

proof

let s be Element of Funcs (X,INT); :: thesis: ( S₂[s] & s in (Funcs (X,INT)) \ (b,0) & S₁[s] implies S₂[g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))] )
assume that
A26: S₂[s] and
s in (Funcs (X,INT)) \ (b,0) and
S₁[s] ; :: thesis: S₂[g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))]
reconsider sm = s . m as Element of NAT by A26, INT_1:3;
s . m = (((s . m) div 2) * 2) + ((s . m) mod 2) by NEWTON:66;
then A27: (s . x) |^ n = (s . y) * (((s . x) to_power ((sm div 2) * 2)) * ((s . x) to_power (sm mod 2))) by A26, FIB_NUM2:5
.= ((s . y) * ((s . x) to_power (sm mod 2))) * ((s . x) to_power ((sm div 2) * 2))
.= ((s . y) * ((s . x) to_power (sm mod 2))) * (((s . x) to_power 2) to_power (sm div 2)) by NEWTON:9
.= ((s . y) * ((s . x) to_power (sm mod 2))) * (((s . x) * (s . x)) to_power (sm div 2)) by NEWTON:81 ;
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 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));
A28: ( 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 A1;
A29: (g . ((g . (s,(if-then ((m is_odd),(y *= x))))),(m /= 2))) . x = (g . (s,(if-then ((m is_odd),(y *= x))))) . x by A15, Th45
.= (g . (s,(m is_odd))) . x by A24, A28, Th33, AOFA_000:def 28 ;
A30: (g . ((g . (s,(if-then ((m is_odd),(y *= x))))),(m /= 2))) . y = (g . (s,(if-then ((m is_odd),(y *= x))))) . y by A6, Th45;
A31: (g . (s,(m is_odd))) . y = s . y by A2, A4, Th49;
A32: (g . (s,(m is_odd))) . x = s . x by A2, A3, Th49;
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 A33: 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 A34: (g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))) . y = (g . ((g . (s,(if-then ((m is_odd),(y *= x))))),(m /= 2))) . y by A24, Th33;
A35: sm div 2 = (s . m) div 2 ;

A36: now :: thesis: (s . y) * ((s . x) to_power (sm mod 2)) = (g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))) . y

A37: (g . (s,(m is_odd))) . b = (s . m) mod 2 by Th49;

per cases ( (g . (s,(m is_odd))) . b = 0 or (g . (s,(m is_odd))) . b = 1 ) by A35, A37, NAT_D:12;

suppose A38: (g . (s,(m is_odd))) . b = 0 ; :: thesis: (s . y) * ((s . x) to_power (sm mod 2)) = (g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))) . y

then g . (s,(m is_odd)) nin (Funcs (X,INT)) \ (b,0) by Th2;
then g . (s,(if-then ((m is_odd),(y *= x)))) = g . ((g . (s,(m is_odd))),(EmptyIns A)) by A1;
then A39: (g . (s,(if-then ((m is_odd),(y *= x))))) . y = (g . (s,(m is_odd))) . y by AOFA_000:def 28;
A40: (s . y) * 1 = s . y ;
(s . x) to_power 0 = 1 by POWER:24;
hence (s . y) * ((s . x) to_power (sm mod 2)) = (g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))) . y by A34, A30, A31, A38, A39, A40, Th49; :: thesis: verum

end;

suppose A41: (g . (s,(m is_odd))) . b = 1 ; :: thesis: (s . y) * ((s . x) to_power (sm mod 2)) = (g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))) . y

then g . (s,(m is_odd)) in (Funcs (X,INT)) \ (b,0) ;
then g . (s,(if-then ((m is_odd),(y *= x)))) = g . ((g . (s,(m is_odd))),(y *= x)) by A1;
then A42: (g . (s,(if-then ((m is_odd),(y *= x))))) . y = ((g . (s,(m is_odd))) . y) * ((g . (s,(m is_odd))) . x) by Th33;
(s . x) to_power 1 = s . x by POWER:25;
hence (s . y) * ((s . x) to_power (sm mod 2)) = (g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))) . y by A32, A34, A30, A31, A41, A42, Th49; :: thesis: verum

end;

end;

end;

(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 A15, A33, Th33
.= ((g . (s,(if-then ((m is_odd),(y *= x))))) . m) div 2 by Th45
.= ((g . (s,(m is_odd))) . m) div 2 by A6, A28, Th33, AOFA_000:def 28
.= (s . m) div 2 by A2, A5, Th49 ;
hence S₂[g . (s,(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))] by A33, A29, A32, A36, A27, Th33; :: thesis: verum

end;

A43: ( (g . (s,(y := 1))) . m <= 0 implies (g . ((g . (s,(y := 1))),(m gt 0))) . b = 0 ) by Th38;
( (g . (s,(y := 1))) . m > 0 implies (g . ((g . (s,(y := 1))),(m gt 0))) . b = 1 ) by Th38;
then A44: ( g . ((g . (s,(y := 1))),(m gt 0)) in (Funcs (X,INT)) \ (b,0) iff S₁[g . ((g . (s,(y := 1))),(m gt 0))] ) by A43, Th2, Th38;
A45: g iteration_terminates_for (((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)) \; (m gt 0),g . ((g . (s,(y := 1))),(m gt 0)) from AOFA_000:sch 3(A44, A16);
(g . (s,(y := 1))) . x = s . x by A24, Th25;
then A46: S₂[g . (s,(y := 1))] by A13, A7, A12, POWER:41;
A47: ( S₂[g . ((g . (s,(y := 1))),(while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))))] & not S₁[g . ((g . (s,(y := 1))),(while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))))] ) from AOFA_000:sch 5(A46, A45, A25, A8);
then (g . ((g . (s,(y := 1))),(while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x)))))) . m = 0 ;
hence (g . (s,((y := 1) \; (while ((m gt 0),(((if-then ((m is_odd),(y *= x))) \; (m /= 2)) \; (x *= x))))))) . y = (s . x) |^ n by A47, A14, AOFA_000:def 29; :: thesis: verum