:: by Grzegorz Bancerek and Piotr Rudnicki

::

:: Received October 8, 1993

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

begin

definition

let X1, X2 be non empty set ;

let Y1 be non empty Subset of X1;

let Y2 be non empty Subset of X2;

let x be Element of [:Y1,Y2:];

:: original: `1

redefine func x `1 -> Element of Y1;

coherence

x `1 is Element of Y1

redefine func x `2 -> Element of Y2;

coherence

x `2 is Element of Y2

end;
let Y1 be non empty Subset of X1;

let Y2 be non empty Subset of X2;

let x be Element of [:Y1,Y2:];

:: original: `1

redefine func x `1 -> Element of Y1;

coherence

x `1 is Element of Y1

proof end;

:: original: `2redefine func x `2 -> Element of Y2;

coherence

x `2 is Element of Y2

proof end;

definition

let n be Nat;

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

( b

( b

theorem :: PRE_FF:1

proof end;

theorem :: PRE_FF:2

proof end;

theorem :: PRE_FF:3

proof end;

theorem :: PRE_FF:4

proof end;

theorem :: PRE_FF:5

proof end;

theorem :: PRE_FF:6

proof end;

theorem :: PRE_FF:7

proof end;

theorem :: PRE_FF:8

canceled;

theorem :: PRE_FF:9

canceled;

theorem Th10: :: PRE_FF:10

proof end;

theorem Th11: :: PRE_FF:11

proof end;

theorem Th12: :: PRE_FF:12

proof end;

theorem Th13: :: PRE_FF:13

proof end;

theorem Th14: :: PRE_FF:14

proof end;

theorem Th15: :: PRE_FF:15

proof end;

theorem :: PRE_FF:16

proof end;

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;

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

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

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

( ( 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 Th17: :: PRE_FF:17

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

theorem :: PRE_FF:18

proof end;

theorem :: PRE_FF:19

proof end;

theorem :: PRE_FF:20

theorem :: PRE_FF:21

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

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

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

proof end;

theorem :: PRE_FF:22

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

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

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

proof end;