:: Two Programs for {\bf SCM}. Part I - Preliminaries
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users
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 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 :: PRE_FF:1
theorem :: PRE_FF:2
theorem :: PRE_FF:3
theorem :: PRE_FF:4
theorem :: PRE_FF:5
theorem :: PRE_FF:6
theorem :: PRE_FF:7
theorem :: PRE_FF:8
canceled;
theorem :: PRE_FF:9
canceled;
theorem Th10: :: PRE_FF:10
theorem Th11: :: PRE_FF:11
theorem Th12: :: PRE_FF:12
theorem Th13: :: PRE_FF:13
theorem Th14: :: PRE_FF:14
theorem Th15: :: PRE_FF:15
theorem :: PRE_FF:16
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: :: PRE_FF:17
theorem :: PRE_FF:18
for
nn,
nn' being
Nat st
nn <> 0 &
nn = 2
* nn' holds
nn' < nn
theorem :: PRE_FF:19
for
nn,
nn' being
Nat st
nn = (2 * nn') + 1 holds
nn' < nn
theorem :: PRE_FF:20
theorem :: PRE_FF:21
theorem :: PRE_FF:22