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_{1}[ 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_{1}[g . (s2,(i := a))]
by A19, A16, A15, A18, A13, A1, PRE_FF:1;

A22: n <> z by A3, A6;

_{1}[s] holds

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

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_{1}[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_{1}[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

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

( 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

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) )

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

( S

proof

reconsider F = for-do ((i := a),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))) as Element of A ;
let s be Element of Funcs (X,INT); :: thesis: ( S_{1}[s] implies ( S_{1}[g . (s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1)))] & S_{1}[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_{1}[g . (s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1)))] & S_{1}[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_{1}[g . (s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1)))]
:: thesis: S_{1}[g . (s,(i leq n))]

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;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

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

proof

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) )
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;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

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

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

( (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

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