begin
definition
let n be
Nat;
func Fib n -> Element of
NAT means :
Def1:
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 b1 being Element of NAT ex fib being Function of NAT ,[:NAT ,NAT :] st
( b1 = (fib . n) `1 & fib . 0 = [0 ,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2 ),(((fib . n) `1 ) + ((fib . n) `2 ))] ) )
uniqueness
for b1, b2 being Element of NAT st ex fib being Function of NAT ,[:NAT ,NAT :] st
( b1 = (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
( b2 = (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
b1 = b2
end;
:: deftheorem Def1 defines Fib PRE_FF:def 1 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
defpred S1[ Nat, FinSequence of NAT , set ] means ( ( for k being Nat st $1 + 2 = 2 * k holds
$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 S1[n,x,y]
defpred S2[ Nat, FinSequence of NAT , set ] means ( ( for k being Element of NAT st $1 + 2 = 2 * k holds
$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 S2[n,x,y1] & S2[n,x,y2] holds
y1 = y2
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 S1[n,fusc . n,fusc . (n + 1)]
from RECDEF_1:sch 2(Lm1);
Lm5:
for n being Nat holds S1[n,fusc . n,fusc . (n + 1)]
:: deftheorem Def2 defines Fusc PRE_FF:def 2 :
theorem Th17:
theorem
for
nn,
nn9 being
Nat st
nn <> 0 &
nn = 2
* nn9 holds
nn9 < nn
theorem
for
nn,
nn9 being
Nat st
nn = (2 * nn9) + 1 holds
nn9 < nn
theorem
theorem
theorem