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, x, y, z, i being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds
for s being Element of Funcs X,INT
for N being Element of NAT st N = s . n holds
(g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib 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, x, y, z, i being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds
for s being Element of Funcs X,INT
for N being Element of NAT st N = s . n holds
(g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib 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, x, y, z, i being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds
for s being Element of Funcs X,INT
for N being Element of NAT st N = s . n holds
(g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib N
let g be Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0 ; :: thesis: for n, x, y, z, i being Variable of g st ex d being Function st
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) holds
for s being Element of Funcs X,INT
for N being Element of NAT st N = s . n holds
(g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib N
A1: 0 + 1 = 1 ;
set S = Funcs X,INT ;
set T = (Funcs X,INT ) \ b,0 ;
let n, x, y, z, i be Variable of g; :: thesis: ( ex d being Function st
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & d . i = 5 ) implies for s being Element of Funcs X,INT
for N being Element of NAT st N = s . n holds
(g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib N )
given d being Function such that A2: d . b = 0 and
A3: d . n = 1 and
A4: d . x = 2 and
A5: d . y = 3 and
A6: d . z = 4 and
A7: d . i = 5 ; :: thesis: for s being Element of Funcs X,INT
for N being Element of NAT st N = s . n holds
(g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib N
A8: n <> x by A3, A4;
A9: y <> z by A5, A6;
A10: x <> z by A4, A6;
A11: i <> z by A6, A7;
A12: n <> y by A3, A5;
let s be Element of Funcs X,INT ; :: thesis: for N being Element of NAT st N = s . n holds
(g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib N
reconsider s1 = g . s,(x := 0 ) as Element of Funcs X,INT ;
reconsider s2 = g . s1,(y := 1) as Element of Funcs X,INT ;
reconsider s4 = g . s2,(i := 1) as Element of Funcs X,INT ;
A13: s4 . i = 1 by Th25;
A14: i <> y by A5, A7;
then A15: s4 . y = s2 . y by Th25;
set I = ((z := x) \; (x := y)) \; (y += z);
A16: s2 . y = 1 by Th25;
A17: i <> x by A4, A7;
then A18: s4 . x = s2 . x by Th25;
defpred S₁[ Element of Funcs X,INT ] means ex N being Element of NAT st
( N = ($1 . i) - 1 & $1 . x = Fib N & $1 . y = Fib (N + 1) );
reconsider a = . 1,A,g as INT-Expression of A,g ;
A19: s1 . x = 0 by Th25;
A20: x <> y by A4, A5;
then s2 . x = s1 . x by Th25;
then A21: S₁[g . s2,(i := a)] by A19, A16, A15, A18, A13, A1, PRE_FF:1;
A22: n <> z by A3, A6;

A23: now

let s be Element of Funcs X,INT ; :: thesis: ( (g . s,(((z := x) \; (x := y)) \; (y += z))) . i = s . i & (g . s,(((z := x) \; (x := y)) \; (y += z))) . n = s . n & (g . s,(((z := x) \; (x := y)) \; (y += z))) . x = s . y & (g . s,(((z := x) \; (x := y)) \; (y += z))) . y = (s . x) + (s . y) )
reconsider s1 = g . s,(z := x) as Element of Funcs X,INT ;
reconsider s2 = g . s1,(x := y) as Element of Funcs X,INT ;
reconsider s3 = g . s2,(y += z) as Element of Funcs X,INT ;
A24: g . s,(((z := x) \; (x := y)) \; (y += z)) = g . (g . s,((z := x) \; (x := y))),(y += z) by AOFA_000:def 29
.= s3 by AOFA_000:def 29 ;
A25: s1 . z = s . x by Th27;
A26: s2 . n = s1 . n by A8, Th27;
A27: s1 . i = s . i by A11, Th27;
A28: s2 . z = s1 . z by A10, Th27;
A29: s2 . y = s1 . y by A20, Th27;
A30: s2 . i = s1 . i by A17, Th27;
A31: s1 . y = s . y by A9, Th27;
A32: s2 . x = s1 . y by Th27;
s1 . n = s . n by A22, Th27;
hence ( (g . s,(((z := x) \; (x := y)) \; (y += z))) . i = s . i & (g . s,(((z := x) \; (x := y)) \; (y += z))) . n = s . n & (g . s,(((z := x) \; (x := y)) \; (y += z))) . x = s . y & (g . s,(((z := x) \; (x := y)) \; (y += z))) . y = (s . x) + (s . y) ) by A12, A14, A20, A31, A25, A27, A26, A32, A29, A28, A30, A24, Th30; :: thesis: verum

end;

A33: for s being Element of Funcs X,INT st S₁[s] holds
( S₁[g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))] & S₁[g . s,(i leq n)] )

proof

let s be Element of Funcs X,INT ; :: thesis: ( S₁[s] implies ( S₁[g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))] & S₁[g . s,(i leq n)] ) )
given N being Element of NAT such that A34: N = (s . i) - 1 and
A35: s . x = Fib N and
A36: s . y = Fib (N + 1) ; :: thesis: ( S₁[g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))] & S₁[g . s,(i leq n)] )
reconsider s1 = g . s,(((z := x) \; (x := y)) \; (y += z)) as Element of Funcs X,INT ;
reconsider s2 = g . s1,(i += 1) as Element of Funcs X,INT ;
A37: s1 . x = s . y by A23;
A38: s2 . i = (s1 . i) + 1 by Th28;
A39: s1 . y = (s . x) + (s . y) by A23;
A40: s2 . y = s1 . y by A14, Th28;
thus S₁[g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))] :: thesis: S₁[g . s,(i leq n)]

proof

take N1 = N + 1; :: thesis: ( N1 = ((g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))) . i) - 1 & (g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))) . x = Fib N1 & (g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))) . y = Fib (N1 + 1) )
g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1)) = s2 by AOFA_000:def 29;
hence ( N1 = ((g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))) . i) - 1 & (g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))) . x = Fib N1 & (g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))) . y = Fib (N1 + 1) ) by A17, A23, A34, A35, A36, A37, A39, A40, A38, Th28, PRE_FF:1; :: thesis: verum

end;

take N ; :: thesis: ( N = ((g . s,(i leq n)) . i) - 1 & (g . s,(i leq n)) . x = Fib N & (g . s,(i leq n)) . y = Fib (N + 1) )
thus ( N = ((g . s,(i leq n)) . i) - 1 & (g . s,(i leq n)) . x = Fib N & (g . s,(i leq n)) . y = Fib (N + 1) ) by A2, A4, A5, A7, A34, A35, A36, Th35; :: thesis: verum

end;

reconsider F = for-do (i := a),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z)) as Element of A ;
reconsider s3 = g . s2,(for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))) as Element of Funcs X,INT ;
let N be Element of NAT ; :: thesis: ( N = s . n implies (g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib N )
assume A41: N = s . n ; :: thesis: (g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib N
A42: F = for-do (i := a),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z)) ;
g . s,((x := 0 ) \; (y := 1)) = s2 by AOFA_000:def 29;
then A43: g . s,(((x := 0 ) \; (y := 1)) \; F) = s3 by AOFA_000:def 29;
A44: ( ( 0 <= N & N <= 0 ) or N >= 0 + 1 ) by NAT_1:13;
A45: ( n <> i & n <> b & i <> b ) by A2, A3, A7;
A46: a . s2 = 1 by FUNCOP_1:13;
A47: for s being Element of Funcs X,INT st S₁[s] holds
( (g . s,(((z := x) \; (x := y)) \; (y += z))) . i = s . i & (g . s,(((z := x) \; (x := y)) \; (y += z))) . n = s . n ) by A23;
A48: ( S₁[g . s2,F] & ( a . s2 <= s2 . n implies (g . s2,F) . i = (s2 . n) + 1 ) & ( a . s2 > s2 . n implies (g . s2,F) . i = a . s2 ) & (g . s2,F) . n = s2 . n ) from AOFA_I00:sch 1(A42, A21, A33, A47, A45);
s2 . n = s1 . n by A12, Th25;
hence (g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib N by A41, A43, A8, A48, A44, A46, Th25; :: thesis: verum