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);
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 :: thesis: for s being Element of Funcs (X,INT) holds
( (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) )

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 N + 1 ; :: thesis: ( N + 1 = ((g . (s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1)))) . i) - 1 & (g . (s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1)))) . x = Fib (N + 1) & (g . (s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1)))) . y = Fib ((N + 1) + 1) )
g . (s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))) = s2 by AOFA_000:def 29;
hence ( N + 1 = ((g . (s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1)))) . i) - 1 & (g . (s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1)))) . x = Fib (N + 1) & (g . (s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1)))) . y = Fib ((N + 1) + 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;
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, Th25; :: thesis: verum