:: by Grzegorz Bancerek and Piotr Rudnicki

::

:: Received October 8, 1993

:: Copyright (c) 1993-2012 Association of Mizar Users

begin

:: Definition of fib

definition

let n be Nat;

ex b_{1} being Element of NAT ex fib being Function of NAT,[:NAT,NAT:] st

( b_{1} = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) )

for b_{1}, b_{2} being Element of NAT st ex fib being Function of NAT,[:NAT,NAT:] st

( b_{1} = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) & ex fib being Function of NAT,[:NAT,NAT:] st

( b_{2} = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) holds

b_{1} = b_{2}

end;
func Fib n -> Element of NAT means :Def1: :: PRE_FF:def 1

ex fib being Function of NAT,[:NAT,NAT:] st

( it = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) );

existence ex fib being Function of NAT,[:NAT,NAT:] st

( it = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def1 defines Fib PRE_FF:def 1 :

for n being Nat

for b_{2} being Element of NAT holds

( b_{2} = Fib n iff ex fib being Function of NAT,[:NAT,NAT:] st

( b_{2} = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) );

for n being Nat

for b

( b

( b

:: Fusc function auxiliaries

:: Fusc sequence

definition

let f be Function of NAT,(NAT *);

let n be Element of NAT ;

:: original: .

redefine func f . n -> FinSequence of NAT ;

coherence

f . n is FinSequence of NAT

end;
let n be Element of NAT ;

:: original: .

redefine func f . n -> FinSequence of NAT ;

coherence

f . n is FinSequence of NAT

proof end;

defpred S

$3 = $2 ^ <*($2 /. k)*> ) & ( for k being Nat st $1 + 2 = (2 * k) + 1 holds

$3 = $2 ^ <*(($2 /. k) + ($2 /. (k + 1)))*> ) );

Lm1: for n being Element of NAT

for x being Element of NAT * ex y being Element of NAT * st S

proof end;

defpred S

$3 = $2 ^ <*($2 /. k)*> ) & ( for k being Element of NAT st $1 + 2 = (2 * k) + 1 holds

$3 = $2 ^ <*(($2 /. k) + ($2 /. (k + 1)))*> ) );

Lm2: for n being Nat

for x, y1, y2 being Element of NAT * st S

y1 = y2

proof end;

reconsider single1 = <*1*> as Element of NAT * by FINSEQ_1:def 11;

consider fusc being Function of NAT,(NAT *) such that

Lm3: fusc . 0 = single1 and

Lm4: for n being Element of NAT holds S

Lm5: for n being Nat holds S

proof end;

definition

let n be Nat;

for b_{1} being Element of NAT holds verum
;

existence

( ( n = 0 implies ex b_{1} being Element of NAT st b_{1} = 0 ) & ( not n = 0 implies ex b_{1}, l being Element of NAT ex fusc being Function of NAT,(NAT *) st

( l + 1 = n & b_{1} = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds

( ( for k being Nat st n + 2 = 2 * k holds

fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds

fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) ) )

for b_{1}, b_{2} being Element of NAT holds

( ( n = 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) & ( not n = 0 & ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st

( l + 1 = n & b_{1} = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds

( ( for k being Nat st n + 2 = 2 * k holds

fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds

fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) & ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st

( l + 1 = n & b_{2} = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds

( ( for k being Nat st n + 2 = 2 * k holds

fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds

fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) implies b_{1} = b_{2} ) )

end;
func Fusc n -> Element of NAT means :Def2: :: PRE_FF:def 2

it = 0 if n = 0

otherwise ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st

( l + 1 = n & it = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds

( ( for k being Nat st n + 2 = 2 * k holds

fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds

fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) );

consistency it = 0 if n = 0

otherwise ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st

( l + 1 = n & it = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds

( ( for k being Nat st n + 2 = 2 * k holds

fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds

fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) );

for b

existence

( ( n = 0 implies ex b

( l + 1 = n & b

( ( for k being Nat st n + 2 = 2 * k holds

fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds

fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) ) )

proof end;

uniqueness for b

( ( n = 0 & b

( l + 1 = n & b

( ( for k being Nat st n + 2 = 2 * k holds

fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds

fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) & ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st

( l + 1 = n & b

( ( for k being Nat st n + 2 = 2 * k holds

fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds

fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) implies b

proof end;

:: deftheorem Def2 defines Fusc PRE_FF:def 2 :

for n being Nat

for b_{2} being Element of NAT holds

( ( n = 0 implies ( b_{2} = Fusc n iff b_{2} = 0 ) ) & ( not n = 0 implies ( b_{2} = Fusc n iff ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st

( l + 1 = n & b_{2} = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds

( ( for k being Nat st n + 2 = 2 * k holds

fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds

fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) ) ) );

for n being Nat

for b

( ( n = 0 implies ( b

( l + 1 = n & b

( ( for k being Nat st n + 2 = 2 * k holds

fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds

fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) ) ) );

theorem Th15: :: PRE_FF:15

( Fusc 0 = 0 & Fusc 1 = 1 & ( for n being Nat holds

( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) ) ) )

( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) ) ) )

proof end;

:: Auxiliary functions specific for Fib and Fusc of little general interest

theorem :: PRE_FF:19

for n, A, B, N being Nat st Fusc N = (A * (Fusc ((2 * n) + 1))) + (B * (Fusc (((2 * n) + 1) + 1))) holds

Fusc N = (A * (Fusc n)) + ((B + A) * (Fusc (n + 1)))

Fusc N = (A * (Fusc n)) + ((B + A) * (Fusc (n + 1)))

proof end;

theorem :: PRE_FF:20

for n, A, B, N being Nat st Fusc N = (A * (Fusc (2 * n))) + (B * (Fusc ((2 * n) + 1))) holds

Fusc N = ((A + B) * (Fusc n)) + (B * (Fusc (n + 1)))

Fusc N = ((A + B) * (Fusc n)) + (B * (Fusc (n + 1)))

proof end;