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
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 A0:
( d . b = 0 & d . n = 1 & d . x = 2 & d . y = 3 & d . z = 4 & 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
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
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 A1:
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
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 s3 = g . s2,(for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))) as Element of Funcs X,INT ;
reconsider s4 = g . s2,(i := 1) as Element of Funcs X,INT ;
set I = ((z := x) \; (x := y)) \; (y += z);
reconsider a = . 1,A,g as INT-Expression of A,g ;
reconsider F = for-do (i := a),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z)) as Element of A ;
g . s,((x := 0 ) \; (y := 1)) = s2
by AOFA_000:def 29;
then S0:
g . s,(((x := 0 ) \; (y := 1)) \; F) = s3
by AOFA_000:def 29;
D0:
( n <> x & i <> x & n <> y & i <> y & x <> y & i <> n & n <> z & i <> z & x <> z & y <> z )
by A0;
then S1:
( s1 . n = s . n & s1 . x = 0 )
by Th011;
S2:
( s2 . n = s1 . n & s2 . y = 1 & s2 . x = s1 . x )
by D0, Th011;
S3:
( s4 . n = s2 . n & s4 . y = s2 . y & s4 . x = s2 . x & s4 . i = 1 )
by D0, Th011;
defpred S1[ 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) );
F:
F = for-do (i := a),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))
;
( 1 - 1 = 0 & 0 + 1 = 1 )
;
then A:
S1[g . s2,(i := a)]
by S1, S2, S3, PRE_FF:1;
Si:
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 ;
R1:
(
s1 . n = s . n &
s1 . x = s . x &
s1 . y = s . y &
s1 . z = s . x &
s1 . i = s . i )
by D0, Th211;
R2:
(
s2 . n = s1 . n &
s2 . x = s1 . y &
s2 . y = s1 . y &
s2 . z = s1 . z &
s2 . i = s1 . i )
by D0, Th211;
R4:
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
;
thus
(
(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 R1, R2, D0, R4, Th212;
:: thesis: verum end;
B:
for s being Element of Funcs X,INT st S1[s] holds
( S1[g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))] & S1[g . s,(i leq n)] )
proof
let s be
Element of
Funcs X,
INT ;
:: thesis: ( S1[s] implies ( S1[g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))] & S1[g . s,(i leq n)] ) )
given N being
Element of
NAT such that Q0:
(
N = (s . i) - 1 &
s . x = Fib N &
s . y = Fib (N + 1) )
;
:: thesis: ( S1[g . s,((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))] & S1[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 ;
Q1:
(
s1 . x = s . y &
s1 . y = (s . x) + (s . y) &
s1 . i = s . i )
by Si;
Q2:
(
s2 . x = s1 . x &
s2 . y = s1 . y &
s2 . i = (s1 . i) + 1 )
by D0, Th012;
thus
S1[
g . s,
((((z := x) \; (x := y)) \; (y += z)) \; (i += 1))]
:: thesis: S1[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 &
N1 - 1
= N )
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 Q0, Q1, Q2, 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 Q0, A0, Th114;
:: thesis: verum
end;
C:
for s being Element of Funcs X,INT st S1[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 Si;
D:
( n <> i & n <> b & i <> b )
by A0;
E:
( S1[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(F, A, B, C, D);
E2:
( ( 0 <= N & N <= 0 ) or N >= 0 + 1 )
by NAT_1:13;
a . s2 = 1
by FUNCOP_1:13;
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 A1, S0, D0, Th011, S2, E, E2; :: thesis: verum