:: PRE_FF semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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
proof end;
:: original: `2
redefine func x `2 -> Element of Y2;
coherence
x `2 is Element of Y2
proof end;
end;

definition
let n be Nat;
func Fib n -> 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 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 ))] ) )
proof end;
uniqueness
for b1, b2 being 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
proof end;
end;

:: deftheorem Def1 defines Fib PRE_FF:def 1 :
for n, b2 being Nat holds
( b2 = Fib n iff 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 ))] ) ) );

theorem :: PRE_FF:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer holds i div 1 = i
proof end;

theorem :: PRE_FF:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Integer st j > 0 & i div j = 0 holds
i < j
proof end;

theorem :: PRE_FF:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Integer st 0 <= i & i < j holds
i div j = 0
proof end;

theorem :: PRE_FF:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, k being Integer st j > 0 & k > 0 holds
(i div j) div k = i div (j * k)
proof end;

theorem :: PRE_FF:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer holds
( i mod 2 = 0 or i mod 2 = 1 )
proof end;

theorem :: PRE_FF:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer st i is Nat holds
i div 2 is Nat
proof end;

theorem :: PRE_FF:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PRE_FF:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th10: :: PRE_FF:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a <= b & c > 1 holds
c to_power a <= c to_power b
proof end;

theorem Th11: :: PRE_FF:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being real number st r >= s holds
[\r/] >= [\s/]
proof end;

theorem Th12: :: PRE_FF:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 1 & b > 0 & c >= b holds
log a,c >= log a,b
proof end;

theorem Th13: :: PRE_FF:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n > 0 holds
[\(log 2,(2 * n))/] + 1 <> [\(log 2,((2 * n) + 1))/]
proof end;

theorem Th14: :: PRE_FF:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n > 0 holds
[\(log 2,(2 * n))/] + 1 >= [\(log 2,((2 * n) + 1))/]
proof end;

theorem Th15: :: PRE_FF:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n > 0 holds
[\(log 2,(2 * n))/] = [\(log 2,((2 * n) + 1))/]
proof end;

theorem :: PRE_FF:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n > 0 holds
[\(log 2,n)/] + 1 = [\(log 2,((2 * n) + 1))/]
proof end;

definition
let f be Function of NAT ,NAT * ;
let n be Nat;
:: original: .
redefine func f . n -> FinSequence of NAT ;
coherence
f . n is FinSequence of NAT
proof end;
end;

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 Nat
for x being Element of NAT * ex y being Element of NAT * st S1[n,x,y]
proof end;

defpred S2[ 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)))*> ) );

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
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 Nat holds S1[n,fusc . n,fusc . (n + 1)] from RECDEF_1:sch 2( NAT * single1 , Lm1);

definition
let n be Nat;
func Fusc n -> Nat means :Def2: :: PRE_FF:def 2
it = 0 if n = 0
otherwise ex l being 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 b1 being Nat holds verum ;
existence
( ( n = 0 implies ex b1 being Nat st b1 = 0 ) & ( not n = 0 implies ex b1, l being Nat ex fusc being Function of NAT ,NAT * st
( l + 1 = n & b1 = (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)))*> ) ) ) ) ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( n = 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not n = 0 & ex l being Nat ex fusc being Function of NAT ,NAT * st
( l + 1 = n & b1 = (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 Nat ex fusc being Function of NAT ,NAT * st
( l + 1 = n & b2 = (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 b1 = b2 ) )
proof end;
end;

:: deftheorem Def2 defines Fusc PRE_FF:def 2 :
for n, b2 being Nat holds
( ( n = 0 implies ( b2 = Fusc n iff b2 = 0 ) ) & ( not n = 0 implies ( b2 = Fusc n iff ex l being Nat ex fusc being Function of NAT ,NAT * st
( l + 1 = n & b2 = (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)))*> ) ) ) ) ) ) );

theorem Th17: :: PRE_FF:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for nn, nn' being Nat st nn <> 0 & nn = 2 * nn' holds
nn' < nn
proof end;

theorem :: PRE_FF:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for nn, nn' being Nat st nn = (2 * nn') + 1 holds
nn' < nn
proof end;

theorem :: PRE_FF:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Nat holds B = (A * (Fusc 0)) + (B * (Fusc (0 + 1))) by Th17;

theorem :: PRE_FF:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for nn, nn', A, B, N being Nat st nn = (2 * nn') + 1 & Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) holds
Fusc N = (A * (Fusc nn')) + ((B + A) * (Fusc (nn' + 1)))
proof end;

theorem :: PRE_FF:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for nn, nn', A, B, N being Nat st nn = 2 * nn' & Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) holds
Fusc N = ((A + B) * (Fusc nn')) + (B * (Fusc (nn' + 1)))
proof end;