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 natural number 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 natural number 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 natural number 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 natural number 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 natural number 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 A0:
( d . x = 0 & d . n = 1 & d . s = 2 & d . i = 3 & d . b = 4 )
; :: thesis: for q being Element of Funcs X,INT
for N being natural number 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 q be Element of Funcs X,INT ; :: thesis: for N being natural number 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 N be natural number ; :: 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 A1:
N = q . n
; :: thesis: (g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N
set S = Funcs X,INT ;
set T = (Funcs X,INT ) \ b,0 ;
set q0 = q;
reconsider q1 = g . q,(s := 1) as Element of Funcs X,INT ;
reconsider q2 = g . q1,(i := 1) as Element of Funcs X,INT ;
set I = s *= x;
reconsider a = . 1,A,g as INT-Expression of A,g ;
reconsider F = for-do (i := a),(i leq n),(i += 1),(s *= x) as Element of A ;
defpred S1[ Element of Funcs X,INT ] means ex K being natural number st
( K = ($1 . i) - 1 & $1 . s = (q . x) |^ K & $1 . x = q . x );
F:
F = for-do (i := a),(i leq n),(i += 1),(s *= x)
;
A2:
( i <> x & b <> x & s <> x & s <> n & s <> i & s <> b )
by A0;
D:
( n <> i & n <> b & i <> b )
by A0;
Q1:
( q1 . n = q . n & q1 . s = 1 & ((q . n) + 1) - 1 = q . n & q1 . x = q . x )
by A2, Th011;
Q2:
( q2 . n = q1 . n & q2 . s = q1 . s & q2 . i = 1 & q2 . x = q1 . x & 1 - 1 = 0 )
by A2, D, Th011;
(q . x) |^ 0 = 1
by NEWTON:9;
then A:
S1[g . q1,(i := a)]
by Q1, Q2;
C:
for q being Element of Funcs X,INT st S1[q] holds
( (g . q,(s *= x)) . i = q . i & (g . q,(s *= x)) . n = q . n )
by A2, Th113;
B:
for q being Element of Funcs X,INT st S1[q] holds
( S1[g . q,((s *= x) \; (i += 1))] & S1[g . q,(i leq n)] )
proof
let q be
Element of
Funcs X,
INT ;
:: thesis: ( S1[q] implies ( S1[g . q,((s *= x) \; (i += 1))] & S1[g . q,(i leq n)] ) )
given Ki being
natural number such that A3:
(
Ki = (q . i) - 1 &
q . s = (q . x) |^ Ki &
q . x = q . x )
;
:: thesis: ( S1[g . q,((s *= x) \; (i += 1))] & S1[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 ;
reconsider q' =
g . q,
(i leq n) as
Element of
Funcs X,
INT ;
A4:
q4 = g . q,
((s *= x) \; (i += 1))
by AOFA_000:def 29;
A5:
(
q3 . i = q . i &
q3 . s = (q . s) * (q . x) &
q4 . s = q3 . s &
((q . i) + 1) - 1
= q . i &
q3 . x = q . x &
q4 . x = q3 . x &
((q . i) - 1) + 1
= q . i &
q4 . i = (q3 . i) + 1 )
by A2, Th012, Th213;
then
(
Ki + 1
= (q4 . i) - 1 &
q4 . s = (q . x) |^ (Ki + 1) )
by A3, NEWTON:11;
hence
S1[
g . q,
((s *= x) \; (i += 1))]
by A3, A4, A5;
:: thesis: S1[g . q,(i leq n)]
(
q' . s = q . s &
q' . i = q . i &
q' . x = q . x )
by A2, D, Th114;
hence
S1[
g . q,
(i leq n)]
by A3;
:: thesis: verum
end;
E:
( S1[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(F, A, B, C, D);
N:
( N = 0 or N >= 1 )
by NAT_1:26;
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 A1, Q1, E, N, FUNCOP_1:13
; :: thesis: verum