:: PRE_FF semantic presentation

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Subset of c₁;
let c₄ be non empty Subset of c₂;
let c₅ be Element of [:c₃,c₄:];
redefine func `1 as c₅ `1 -> Element of a₃;
coherence

proof end;

redefine func `2 as c₅ `2 -> Element of a₄;
coherence

proof end;

end;

definition

let c₁ be Nat;
func Fib c₁ -> Nat means :Def1: :: PRE_FF:def 1
ex b₁ being Function of NAT ,[:NAT ,NAT :] st
( a₂ = (b₁ . a₁) `1 & b₁ . 0 = [0,1] & ( for b₂ being Nat holds b₁ . (b₂ + 1) = [((b₁ . b₂) `2 ),(((b₁ . b₂) `1 ) + ((b₁ . b₂) `2 ))] ) );
existence

proof end;

proof end;

end;

:: deftheorem Def1 defines Fib PRE_FF:def 1 :

theorem Th1: :: PRE_FF:1

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

proof end;

theorem Th2: :: PRE_FF:2

for b₁ being Integer holds b₁ div 1 = b₁

proof end;

theorem Th3: :: PRE_FF:3

for b₁, b₂ being Integer st b₂ > 0 & b₁ div b₂ = 0 holds
b₁ < b₂

proof end;

theorem Th4: :: PRE_FF:4

for b₁, b₂ being Integer st 0 <= b₁ & b₁ < b₂ holds
b₁ div b₂ = 0

proof end;

theorem Th5: :: PRE_FF:5

for b₁, b₂, b₃ being Integer st b₂ > 0 & b₃ > 0 holds
(b₁ div b₂) div b₃ = b₁ div (b₂ * b₃)

proof end;

theorem Th6: :: PRE_FF:6

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

proof end;

theorem Th7: :: PRE_FF:7

for b₁ being Integer st b₁ is Nat holds
b₁ div 2 is Nat

proof end;

theorem Th8: :: PRE_FF:8

canceled;

theorem Th9: :: PRE_FF:9

canceled;

theorem Th10: :: PRE_FF:10

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₃ > 1 holds
b₃ to_power b₁ <= b₃ to_power b₂

proof end;

theorem Th11: :: PRE_FF:11

for b₁, b₂ being real number st b₁ >= b₂ holds
[\b₁/] >= [\b₂/]

proof end;

theorem Th12: :: PRE_FF:12

for b₁, b₂, b₃ being real number st b₁ > 1 & b₂ > 0 & b₃ >= b₂ holds
log b₁,b₃ >= log b₁,b₂

proof end;

theorem Th13: :: PRE_FF:13

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

proof end;

theorem Th14: :: PRE_FF:14

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

proof end;

theorem Th15: :: PRE_FF:15

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

proof end;

theorem Th16: :: PRE_FF:16

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

proof end;

definition

let c₁ be Function of NAT ,NAT * ;
let c₂ be Nat;
redefine func . as c₁ . c₂ -> FinSequence of NAT ;
coherence

proof end;

end;

defpred S₁[ Nat, FinSequence of NAT , set ] means ( ( for b₁ being Nat st a₁ + 2 = 2 * b₁ holds
a₃ = a₂ ^ <*(a₂ /. b₁)*> ) & ( for b₁ being Nat st a₁ + 2 = (2 * b₁) + 1 holds
a₃ = a₂ ^ <*((a₂ /. b₁) + (a₂ /. (b₁ + 1)))*> ) );

Lemma8: for b₁ being Nat
for b₂ being Element of NAT * ex b₃ being Element of NAT * st S₁[b₁,b₂,b₃]

proof end;

defpred S₂[ Nat, FinSequence of NAT , set ] means ( ( for b₁ being Nat st a₁ + 2 = 2 * b₁ holds
a₃ = a₂ ^ <*(a₂ /. b₁)*> ) & ( for b₁ being Nat st a₁ + 2 = (2 * b₁) + 1 holds
a₃ = a₂ ^ <*((a₂ /. b₁) + (a₂ /. (b₁ + 1)))*> ) );

Lemma9: for b₁ being Nat
for b₂, b₃, b₄ being Element of NAT * st S₂[b₁,b₂,b₃] & S₂[b₁,b₂,b₄] holds
b₃ = b₄

proof end;

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

consider c₂ being Function of NAT ,NAT * such that
Lemma10: c₂ . 0 = c₁ and
Lemma11: for b₁ being Nat holds S₁[b₁,c₂ . b₁,c₂ . (b₁ + 1)] from RECDEF_1:sch 2(Lemma8);

definition

let c₃ be Nat;
func Fusc c₁ -> Nat means :Def2: :: PRE_FF:def 2
a₂ = 0 if a₁ = 0
otherwise ex b₁ being Natex b₂ being Function of NAT ,NAT * st
( b₁ + 1 = a₁ & a₂ = (b₂ . b₁) /. a₁ & b₂ . 0 = <*1*> & ( for b₃ being Nat holds
( ( for b₄ being Nat st b₃ + 2 = 2 * b₄ holds
b₂ . (b₃ + 1) = (b₂ . b₃) ^ <*((b₂ . b₃) /. b₄)*> ) & ( for b₄ being Nat st b₃ + 2 = (2 * b₄) + 1 holds
b₂ . (b₃ + 1) = (b₂ . b₃) ^ <*(((b₂ . b₃) /. b₄) + ((b₂ . b₃) /. (b₄ + 1)))*> ) ) ) );
consistency ;
existence

proof end;

proof end;

end;

:: deftheorem Def2 defines Fusc PRE_FF:def 2 :

theorem Th17: :: PRE_FF:17

( Fusc 0 = 0 & Fusc 1 = 1 & ( for b₁ being Nat holds
( Fusc (2 * b₁) = Fusc b₁ & Fusc ((2 * b₁) + 1) = (Fusc b₁) + (Fusc (b₁ + 1)) ) ) )

proof end;

theorem Th18: :: PRE_FF:18

for b₁, b₂ being Nat st b₁ <> 0 & b₁ = 2 * b₂ holds
b₂ < b₁

proof end;

theorem Th19: :: PRE_FF:19

for b₁, b₂ being Nat st b₁ = (2 * b₂) + 1 holds
b₂ < b₁

proof end;

theorem Th20: :: PRE_FF:20

for b₁, b₂ being Nat holds b₂ = (b₁ * (Fusc 0)) + (b₂ * (Fusc (0 + 1))) by Th17;

theorem Th21: :: PRE_FF:21

for b₁, b₂, b₃, b₄, b₅ being Nat st b₁ = (2 * b₂) + 1 & Fusc b₅ = (b₃ * (Fusc b₁)) + (b₄ * (Fusc (b₁ + 1))) holds
Fusc b₅ = (b₃ * (Fusc b₂)) + ((b₄ + b₃) * (Fusc (b₂ + 1)))

proof end;

theorem Th22: :: PRE_FF:22

for b₁, b₂, b₃, b₄, b₅ being Nat st b₁ = 2 * b₂ & Fusc b₅ = (b₃ * (Fusc b₁)) + (b₄ * (Fusc (b₁ + 1))) holds
Fusc b₅ = ((b₃ + b₄) * (Fusc b₂)) + (b₄ * (Fusc (b₂ + 1)))

proof end;