PRE_FF: Two Programs for {\bf SCM}. Part I

definition

func Fib -> sequence of [:NAT,NAT:] means :Def1: :: PRE_FF:def 1
( it . 0 = [0,1] & ( for n being Nat holds it . (n + 1) = [((it . n) `2),(((it . n) `1) + ((it . n) `2))] ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Fib PRE_FF:def 1 :

definition

let n be Nat;

func Fib n -> Element of NAT equals :: PRE_FF:def 2
(Fib . n) `1 ;

coherence ;

end;

:: deftheorem defines Fib PRE_FF:def 2 :

theorem :: PRE_FF:1

( Fib 0 = 0 & Fib 1 = 1 & ( for n being Nat holds Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1)) ) )

proof end;

theorem :: PRE_FF:2

for i being Integer holds i div 1 = i

proof end;

theorem :: PRE_FF:3

for i, j being Integer st j > 0 & i div j = 0 holds
i < j

proof end;

theorem :: PRE_FF:4

for i, j being Integer st 0 <= i & i < j holds
i div j = 0

proof end;

theorem :: PRE_FF:5

for i, j, k being Integer st k > 0 holds
(i div j) div k = i div (j * k)

proof end;

theorem :: PRE_FF:6

for i being Integer holds
( i mod 2 = 0 or i mod 2 = 1 )

proof end;

theorem :: PRE_FF:7

for i being Integer st i is Element of NAT holds
i div 2 is Element of NAT

proof end;

theorem Th8: :: PRE_FF:8

for a, b, c being Real st a <= b & c >= 1 holds
c to_power a <= c to_power b

proof end;

theorem Th9: :: PRE_FF:9

for r, s being Real st r >= s holds
[\r/] >= [\s/]

proof end;

theorem Th10: :: PRE_FF:10

for a, b, c being Real st a > 1 & b > 0 & c >= b holds
log (a,c) >= log (a,b)

proof end;

theorem Th11: :: PRE_FF:11

for n being Nat st n > 0 holds
[\(log (2,(2 * n)))/] + 1 <> [\(log (2,((2 * n) + 1)))/]

proof end;

theorem Th12: :: PRE_FF:12

for n being Nat st n > 0 holds
[\(log (2,(2 * n)))/] + 1 >= [\(log (2,((2 * n) + 1)))/]

proof end;

theorem Th13: :: PRE_FF:13

for n being Nat st n > 0 holds
[\(log (2,(2 * n)))/] = [\(log (2,((2 * n) + 1)))/]

proof end;

theorem :: PRE_FF:14

for n being Nat st n > 0 holds
[\(log (2,n))/] + 1 = [\(log (2,((2 * n) + 1)))/]

proof end;

definition

let n be Nat;

func Fusc n -> Element of NAT means :Def2: :: PRE_FF:def 3
it = 0 if n = 0
otherwise ex l being Element of NAT ex fusc being sequence of (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 ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Fusc PRE_FF:def 3 :

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

proof end;

theorem :: PRE_FF:16

for n being Nat st n <> 0 holds
n < 2 * n

proof end;

theorem :: PRE_FF:17

for n being Nat holds n < (2 * n) + 1

proof end;

theorem :: PRE_FF:18

for A, B being Nat holds B = (A * (Fusc 0)) + (B * (Fusc 1)) by Th15;

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

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

proof end;