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, n, s, i being Variable of g st ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . 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, n, s, i being Variable of g st ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . 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, n, s, i being Variable of g st ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); :: thesis: for x, n, s, i being Variable of g st ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

set f = g;

let x, n, s, i be Variable of g; :: thesis: ( ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) implies for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N )

given d being Function such that A1: d . x = 0 and

A2: d . n = 1 and

A3: d . s = 2 and

A4: d . i = 3 and

A5: d . b = 4 ; :: thesis: for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

A6: ( n <> i & n <> b & i <> b ) by A2, A4, A5;

set S = Funcs (X,INT);

let q be Element of Funcs (X,INT); :: thesis: for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

reconsider q1 = g . (q,(s := 1)) as Element of Funcs (X,INT) ;

reconsider q2 = g . (q1,(i := 1)) as Element of Funcs (X,INT) ;

A7: s <> i by A3, A4;

then A8: q2 . s = q1 . s by Th25;

defpred S_{1}[ Element of Funcs (X,INT)] means ex K being Nat st

( K = ($1 . i) - 1 & $1 . s = (q . x) |^ K & $1 . x = q . x );

set I = s *= x;

set q0 = q;

A9: (q . x) |^ 0 = 1 by NEWTON:4;

A10: s <> n by A2, A3;

then A11: for q being Element of Funcs (X,INT) st S_{1}[q] holds

( (g . (q,(s *= x))) . i = q . i & (g . (q,(s *= x))) . n = q . n ) by A7, Th32;

A12: s <> b by A3, A5;

A13: for q being Element of Funcs (X,INT) st S_{1}[q] holds

( S_{1}[g . (q,((s *= x) \; (i += 1)))] & S_{1}[g . (q,(i leq n))] )

reconsider F = for-do ((i := a),(i leq n),(i += 1),(s *= x)) as Element of A ;

A23: F = for-do ((i := a),(i leq n),(i += 1),(s *= x)) ;

A24: q2 . i = 1 by Th25;

A25: q2 . x = q1 . x by A1, A4, Th25;

A26: q1 . s = 1 by Th25;

q1 . x = q . x by A1, A3, Th25;

then A27: S_{1}[g . (q1,(i := a))]
by A26, A8, A24, A25, A9;

A28: ( S_{1}[g . (q1,F)] & ( a . q1 <= q1 . n implies (g . (q1,F)) . i = (q1 . n) + 1 ) & ( a . q1 > q1 . n implies (g . (q1,F)) . i = a . q1 ) & (g . (q1,F)) . n = q1 . n )
from AOFA_I00:sch 1(A23, A27, A13, A11, A6);

A30: q1 . n = q . n by A10, Th25;

let N be Nat; :: thesis: ( N = q . n implies (g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N )

assume A31: N = q . n ; :: thesis: (g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

A32: ( N = 0 or N >= 1 ) by NAT_1:25;

thus (g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (g . (q1,F)) . s by AOFA_000:def 29

.= (q . x) |^ N by A31, A30, A28, A32 ; :: thesis: verum

for b being Element of X

for g being Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0)

for x, n, s, i being Variable of g st ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . 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, n, s, i being Variable of g st ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . 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, n, s, i being Variable of g st ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

let g be Euclidean ExecutionFunction of A, Funcs (X,INT),(Funcs (X,INT)) \ (b,0); :: thesis: for x, n, s, i being Variable of g st ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) holds

for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

set f = g;

let x, n, s, i be Variable of g; :: thesis: ( ex d being Function st

( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 ) implies for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N )

given d being Function such that A1: d . x = 0 and

A2: d . n = 1 and

A3: d . s = 2 and

A4: d . i = 3 and

A5: d . b = 4 ; :: thesis: for q being Element of Funcs (X,INT)

for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

A6: ( n <> i & n <> b & i <> b ) by A2, A4, A5;

set S = Funcs (X,INT);

let q be Element of Funcs (X,INT); :: thesis: for N being Nat st N = q . n holds

(g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

reconsider q1 = g . (q,(s := 1)) as Element of Funcs (X,INT) ;

reconsider q2 = g . (q1,(i := 1)) as Element of Funcs (X,INT) ;

A7: s <> i by A3, A4;

then A8: q2 . s = q1 . s by Th25;

defpred S

( K = ($1 . i) - 1 & $1 . s = (q . x) |^ K & $1 . x = q . x );

set I = s *= x;

set q0 = q;

A9: (q . x) |^ 0 = 1 by NEWTON:4;

A10: s <> n by A2, A3;

then A11: for q being Element of Funcs (X,INT) st S

( (g . (q,(s *= x))) . i = q . i & (g . (q,(s *= x))) . n = q . n ) by A7, Th32;

A12: s <> b by A3, A5;

A13: for q being Element of Funcs (X,INT) st S

( S

proof

reconsider a = . (1,A,g) as INT-Expression of A,g ;
let q be Element of Funcs (X,INT); :: thesis: ( S_{1}[q] implies ( S_{1}[g . (q,((s *= x) \; (i += 1)))] & S_{1}[g . (q,(i leq n))] ) )

given Ki being Nat such that A14: Ki = (q . i) - 1 and

A15: q . s = (q . x) |^ Ki and

A16: q . x = q . x ; :: thesis: ( S_{1}[g . (q,((s *= x) \; (i += 1)))] & S_{1}[g . (q,(i leq n))] )

reconsider q3 = g . (q,(s *= x)) as Element of Funcs (X,INT) ;

reconsider q4 = g . (q3,(i += 1)) as Element of Funcs (X,INT) ;

A17: q3 . s = (q . s) * (q . x) by Th33;

q4 . s = q3 . s by A7, Th28;

then A18: q4 . s = (q . x) |^ (Ki + 1) by A15, A16, A17, NEWTON:6;

A19: q4 = g . (q,((s *= x) \; (i += 1))) by AOFA_000:def 29;

A20: q3 . x = q . x by A1, A3, Th33;

q4 . i = (q3 . i) + 1 by Th28;

then Ki + 1 = (q4 . i) - 1 by A7, A14, Th33;

hence S_{1}[g . (q,((s *= x) \; (i += 1)))]
by A1, A4, A16, A19, A20, A18, Th28; :: thesis: S_{1}[g . (q,(i leq n))]

reconsider q9 = g . (q,(i leq n)) as Element of Funcs (X,INT) ;

A21: q9 . s = q . s by A12, Th35;

A22: q9 . i = q . i by A6, Th35;

q9 . x = q . x by A1, A5, Th35;

hence S_{1}[g . (q,(i leq n))]
by A14, A15, A16, A21, A22; :: thesis: verum

end;given Ki being Nat such that A14: Ki = (q . i) - 1 and

A15: q . s = (q . x) |^ Ki and

A16: q . x = q . x ; :: thesis: ( S

reconsider q3 = g . (q,(s *= x)) as Element of Funcs (X,INT) ;

reconsider q4 = g . (q3,(i += 1)) as Element of Funcs (X,INT) ;

A17: q3 . s = (q . s) * (q . x) by Th33;

q4 . s = q3 . s by A7, Th28;

then A18: q4 . s = (q . x) |^ (Ki + 1) by A15, A16, A17, NEWTON:6;

A19: q4 = g . (q,((s *= x) \; (i += 1))) by AOFA_000:def 29;

A20: q3 . x = q . x by A1, A3, Th33;

q4 . i = (q3 . i) + 1 by Th28;

then Ki + 1 = (q4 . i) - 1 by A7, A14, Th33;

hence S

reconsider q9 = g . (q,(i leq n)) as Element of Funcs (X,INT) ;

A21: q9 . s = q . s by A12, Th35;

A22: q9 . i = q . i by A6, Th35;

q9 . x = q . x by A1, A5, Th35;

hence S

reconsider F = for-do ((i := a),(i leq n),(i += 1),(s *= x)) as Element of A ;

A23: F = for-do ((i := a),(i leq n),(i += 1),(s *= x)) ;

A24: q2 . i = 1 by Th25;

A25: q2 . x = q1 . x by A1, A4, Th25;

A26: q1 . s = 1 by Th25;

q1 . x = q . x by A1, A3, Th25;

then A27: S

A28: ( S

A30: q1 . n = q . n by A10, Th25;

let N be Nat; :: thesis: ( N = q . n implies (g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N )

assume A31: N = q . n ; :: thesis: (g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (q . x) |^ N

A32: ( N = 0 or N >= 1 ) by NAT_1:25;

thus (g . (q,((s := 1) \; (for-do ((i := 1),(i leq n),(i += 1),(s *= x)))))) . s = (g . (q1,F)) . s by AOFA_000:def 29

.= (q . x) |^ N by A31, A30, A28, A32 ; :: thesis: verum