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;
reconsider n9 = n as Element of NAT by ORDINAL1:def 13;
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:29;
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, FUNCT_7:def 1, INT_1:16;
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);
( g . s,(m is_odd ) in (Funcs X,INT ) \ b,0 or g . s,(m is_odd ) nin (Funcs X,INT ) \ b,0 ) ;
then 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, AOFA_000:def 30;
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:16, INT_1:88;
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 FUNCT_7:def 1;
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:83; :: 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:16;
s . m = (((s . m) div 2) * 2) + ((s . m) mod 2) by NEWTON:80;
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:7
.= ((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:14
.= ((s . y) * ((s . x) to_power (sm mod 2))) * (((s . x) * (s . x)) to_power (sm div 2)) by NEWTON:100 ;
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);
( g . s,(m is_odd ) in (Funcs X,INT ) \ b,0 or g . s,(m is_odd ) nin (Funcs X,INT ) \ b,0 ) ;
then 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, AOFA_000:def 30;
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

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, AOFA_000:def 30;
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:29;
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, AOFA_000:def 30;
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:30;
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:46;
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