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 n, s, i being Variable of g st ex d being Function st
( 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 := 2),(i leq n),(i += 1),(s *= i)))) . s = 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 n, s, i being Variable of g st ex d being Function st
( 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 := 2),(i leq n),(i += 1),(s *= i)))) . s = N !
let b be Element of X; :: thesis: for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for n, s, i being Variable of g st ex d being Function st
( 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 := 2),(i leq n),(i += 1),(s *= i)))) . s = N !
let g be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for n, s, i being Variable of g st ex d being Function st
( 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 := 2),(i leq n),(i += 1),(s *= i)))) . s = N !
set f = g;
let n, s, i be Variable of g; :: thesis: ( ex d being Function st
( 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 := 2),(i leq n),(i += 1),(s *= i)))) . s = N ! )
given d being Function such that A0:
( 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 := 2),(i leq n),(i += 1),(s *= i)))) . s = 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 := 2),(i leq n),(i += 1),(s *= i)))) . s = N !
let N be natural number ; :: thesis: ( N = q . n implies (g . q,((s := 1) \; (for-do (i := 2),(i leq n),(i += 1),(s *= i)))) . s = N ! )
assume A1:
N = q . n
; :: thesis: (g . q,((s := 1) \; (for-do (i := 2),(i leq n),(i += 1),(s *= i)))) . s = N !
set S = Funcs X,INT ;
set T = (Funcs X,INT ) \ b,0 ;
reconsider q1 = g . q,(s := 1) as Element of Funcs X,INT ;
reconsider q2 = g . q1,(i := 2) as Element of Funcs X,INT ;
set I = s *= i;
reconsider a = . 2,A,g as INT-Expression of A,g ;
reconsider F = for-do (i := a),(i leq n),(i += 1),(s *= i) as Element of A ;
defpred S1[ Element of Funcs X,INT ] means ex K being natural number st
( K = ($1 . i) - 1 & $1 . s = K ! );
F:
F = for-do (i := a),(i leq n),(i += 1),(s *= i)
;
A2:
( 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 )
by A2, Th011;
Q2:
( q2 . n = q1 . n & q2 . s = q1 . s & q2 . i = 2 & 2 - 1 = 1 )
by A2, D, Th011;
A:
S1[g . q1,(i := a)]
by Th011, Q2, NEWTON:19;
C:
for q being Element of Funcs X,INT st S1[q] holds
( (g . q,(s *= i)) . i = q . i & (g . q,(s *= i)) . n = q . n )
by A2, Th113;
B:
for q being Element of Funcs X,INT st S1[q] holds
( S1[g . q,((s *= i) \; (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 *= i) \; (i += 1))] & S1[g . q,(i leq n)] ) )
given Ki being
natural number such that A3:
(
Ki = (q . i) - 1 &
q . s = Ki ! )
;
:: thesis: ( S1[g . q,((s *= i) \; (i += 1))] & S1[g . q,(i leq n)] )
reconsider q3 =
g . q,
(s *= i) 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 *= i) \; (i += 1))
by AOFA_000:def 29;
(
q3 . i = q . i &
q3 . s = (q . s) * (q . i) &
q4 . s = q3 . s &
((q . i) + 1) - 1
= q . i &
((q . i) - 1) + 1
= q . i &
q4 . i = (q3 . i) + 1 )
by A2, Th012, Th213;
then
(
Ki + 1
= (q4 . i) - 1 &
q4 . s = (Ki + 1) ! )
by A3, NEWTON:21;
hence
S1[
g . q,
((s *= i) \; (i += 1))]
by A4;
:: thesis: S1[g . q,(i leq n)]
(
q' . s = q . s &
q' . i = q . i )
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);
M:
a . q1 = 2
by FUNCOP_1:13;
thus (g . q,((s := 1) \; (for-do (i := 2),(i leq n),(i += 1),(s *= i)))) . s =
(g . q1,F) . s
by AOFA_000:def 29
.=
N !
by M, A1, Q1, E, NAT_1:27, NEWTON:18, NEWTON:19
; :: thesis: verum