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 ;
Z0: ( g complies_with_while_wrt (Funcs X,INT ) \ b,0 & 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 A0: ( d . b = 0 & d . x = 1 & d . y = 2 & 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
D0: ( m <> x & m <> y & x <> y & b <> x & b <> y & b <> m ) by A0;
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
set q = s;
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 )
assume A1: 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
set C = m gt 0 ;
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);
set s1 = g . (g . s,(y := 1)),(m gt 0 );
set fs = g . (g . s,(y := 1)),(while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)));
A3: ( (g . s,(y := 1)) . x = s . x & (g . s,(y := 1)) . m = s . m & (g . s,(y := 1)) . y = 1 ) by D0, Th011;
A4: ( (g . (g . s,(y := 1)),(m gt 0 )) . x = (g . s,(y := 1)) . x & (g . (g . s,(y := 1)),(m gt 0 )) . m = (g . s,(y := 1)) . m & (g . (g . s,(y := 1)),(m gt 0 )) . y = (g . s,(y := 1)) . y & ( (g . s,(y := 1)) . m > 0 implies (g . (g . s,(y := 1)),(m gt 0 )) . b = 1 ) & ( (g . s,(y := 1)) . m <= 0 implies (g . (g . s,(y := 1)),(m gt 0 )) . b = 0 ) ) by A0, Th015;
defpred S1[ Element of Funcs X,INT ] means ( (s . x) |^ n = ($1 . y) * (($1 . x) to_power ($1 . m)) & $1 . m >= 0 );
defpred S2[ Element of Funcs X,INT ] means $1 . m > 0 ;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
A: S1[g . s,(y := 1)] by A1, A3, POWER:46;
deffunc H1( Element of Funcs X,INT ) -> Element of NAT = In ($1 . m),NAT ;
B0: ( g . (g . s,(y := 1)),(m gt 0 ) in (Funcs X,INT ) \ b,0 iff S2[g . (g . s,(y := 1)),(m gt 0 )] ) by A4, LemTS;
B1: for s being Element of Funcs X,INT st S2[s] holds
( ( S2[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 S2[g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))] ) & H1(g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))) < H1(s) )
proof
let s be Element of Funcs X,INT ; :: thesis: ( S2[s] implies ( ( S2[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 S2[g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))] ) & H1(g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))) < H1(s) ) )
assume 00: s . m > 0 ; :: thesis: ( ( S2[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 S2[g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))] ) & H1(g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))) < H1(s) )
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 );
01: ( ( (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 ) & ( (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 ) & (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 & 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 A0, Th015, AOFA_000:def 29;
hence ( S2[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 LemTS; :: thesis: H1(g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))) < H1(s)
set q0 = g . s,(m is_odd );
set q1 = g . s,(if-then (m is_odd ),(y *= 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 03: ( 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 Z0, 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 02: (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 D0, Th213
.= ((g . s,(if-then (m is_odd ),(y *= x))) . m) div 2 by Th017
.= ((g . s,(m is_odd )) . m) div 2 by D0, 03, Th213, AOFA_000:def 28
.= (s . m) div 2 by A0, Th218 ;
then ( (g . (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))),(m gt 0 )) . m in NAT & s . m in NAT ) by 00, 01, INT_1:16, INT_1:88;
then ( H1(s) = s . m & H1(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 H1(g . s,((((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)) \; (m gt 0 ))) < H1(s) by 00, 01, 02, INT_1:83; :: thesis: verum
end;
B: 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(B0, B1);
 C: for s being Element of Funcs X,INT st S1[s] & s in (Funcs X,INT ) \ b,0 & S2[s] holds
S1[g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))]
proof
let s be Element of Funcs X,INT ; :: thesis: ( S1[s] & s in (Funcs X,INT ) \ b,0 & S2[s] implies S1[g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))] )
assume 00: ( S1[s] & s in (Funcs X,INT ) \ b,0 & S2[s] ) ; :: thesis: S1[g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))]
reconsider sm = s . m as Element of NAT by 00, INT_1:16;
set sJ = g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x));
set q0 = g . s,(m is_odd );
set q1 = g . s,(if-then (m is_odd ),(y *= 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 03: ( 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 Z0, 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 07: 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 02: (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 D0, Th213
.= ((g . s,(if-then (m is_odd ),(y *= x))) . m) div 2 by Th017
.= ((g . s,(m is_odd )) . m) div 2 by D0, 03, Th213, AOFA_000:def 28
.= (s . m) div 2 by A0, Th218 ;
(g . (g . s,(if-then (m is_odd ),(y *= x))),(m /= 2)) . x = (g . s,(if-then (m is_odd ),(y *= x))) . x by D0, Th017
.= (g . s,(m is_odd )) . x by D0, 03, Th213, AOFA_000:def 28 ;
then 06: ( (g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) . x = ((g . s,(m is_odd )) . x) * ((g . s,(m is_odd )) . x) & (g . s,(m is_odd )) . x = s . x ) by A0, Th218, 07, Th213;
08: ( (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 & (g . (g . s,(if-then (m is_odd ),(y *= x))),(m /= 2)) . y = (g . s,(if-then (m is_odd ),(y *= x))) . y & (g . s,(m is_odd )) . y = s . y ) by 07, D0, Th213, Th017, Th218;
04: ( sm div 2 = (s . m) div 2 & sm mod 2 = (s . m) mod 2 ) ;
09: now
I1: (g . s,(m is_odd )) . b = (s . m) mod 2 by Th218;
per cases ( (g . s,(m is_odd )) . b = 0 or (g . s,(m is_odd )) . b = 1 ) by 04, I1, NAT_D:12;
suppose I2: (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 LemTS;
then g . s,(if-then (m is_odd ),(y *= x)) = g . (g . s,(m is_odd )),(EmptyIns A) by Z0, AOFA_000:def 30;
then ( (g . s,(if-then (m is_odd ),(y *= x))) . y = (g . s,(m is_odd )) . y & (s . x) to_power 0 = 1 & (s . y) * 1 = s . y ) by AOFA_000:def 28, 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 I2, 08, Th218; :: thesis: verum
end;
suppose I3: (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 Z0, AOFA_000:def 30;
then ( (g . s,(if-then (m is_odd ),(y *= x))) . y = ((g . s,(m is_odd )) . y) * ((g . s,(m is_odd )) . x) & (s . x) to_power 1 = s . x ) by Th213, 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 I3, 08, 06, Th218; :: thesis: verum
end;
end;
end;
s . m = (((s . m) div 2) * 2) + ((s . m) mod 2) by NEWTON:80;
then (s . x) |^ n = (s . y) * (((s . x) to_power ((sm div 2) * 2)) * ((s . x) to_power (sm mod 2))) by 00, 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 ;
hence S1[g . s,(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))] by 02, 06, 09; :: thesis: verum
end;
D: for s being Element of Funcs X,INT st S1[s] holds
( S1[g . s,(m gt 0 )] & ( g . s,(m gt 0 ) in (Funcs X,INT ) \ b,0 implies S2[g . s,(m gt 0 )] ) & ( S2[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: ( S1[s] implies ( S1[g . s,(m gt 0 )] & ( g . s,(m gt 0 ) in (Funcs X,INT ) \ b,0 implies S2[g . s,(m gt 0 )] ) & ( S2[g . s,(m gt 0 )] implies g . s,(m gt 0 ) in (Funcs X,INT ) \ b,0 ) ) )
assume 00: S1[s] ; :: thesis: ( S1[g . s,(m gt 0 )] & ( g . s,(m gt 0 ) in (Funcs X,INT ) \ b,0 implies S2[g . s,(m gt 0 )] ) & ( S2[g . s,(m gt 0 )] implies g . s,(m gt 0 ) in (Funcs X,INT ) \ b,0 ) )
set s1 = g . s,(m gt 0 );
( (g . s,(m gt 0 )) . m = s . m & (g . s,(m gt 0 )) . x = s . x & (g . s,(m gt 0 )) . y = s . y ) by A0, Th015;
hence S1[g . s,(m gt 0 )] by 00; :: thesis: ( g . s,(m gt 0 ) in (Funcs X,INT ) \ b,0 iff S2[g . s,(m gt 0 )] )
( ( s . m > 0 implies (g . s,(m gt 0 )) . b = 1 ) & ( s . m > 0 or s . m <= 0 ) & ( s . m <= 0 implies (g . s,(m gt 0 )) . b = 0 ) ) by Th015;
hence ( g . s,(m gt 0 ) in (Funcs X,INT ) \ b,0 iff S2[g . s,(m gt 0 )] ) by Th015, LemTS; :: thesis: verum
end;
E: ( S1[g . (g . s,(y := 1)),(while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)))] & not S2[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(A, B, C, D);
 then ( (g . (g . s,(y := 1)),(while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x)))) . m = 0 & ((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;
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 E, AOFA_000:def 29; :: thesis: verum