:: Two Programs for {\bf SCM}. Part I - Preliminaries
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, ZFMISC_1, MCART_1, NAT_1, FUNCT_1, CARD_1,
ARYTM_3, INT_1, XXREAL_0, ARYTM_1, RELAT_1, POWER, NEWTON, FINSEQ_1,
ORDINAL4, PARTFUN1, PRE_FF, REAL_1, FUNCT_7;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
XXREAL_0, XCMPLX_0, XREAL_0, INT_1, NAT_D, MCART_1, DOMAIN_1, POWER,
FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, NEWTON, FINSEQ_1, FINSEQ_2;
constructors DOMAIN_1, XXREAL_0, REAL_1, NAT_1, NAT_D, MEMBERED, PARTFUN1,
NEWTON, POWER, RELSET_1, FINSEQ_2;
registrations SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
FINSEQ_1, XCMPLX_0, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems TARSKI, AXIOMS, NAT_1, INT_1, POWER, NEWTON, FINSEQ_1, FINSEQ_4,
FINSEQ_3, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, CARD_1, SUBSET_1,
ZFMISC_1;
schemes NAT_1, RECDEF_1;
begin :: Fibonacci sequence
:: Definition of fib
deffunc F(set,Element of [:NAT,NAT:]) = In([$2`2, $2`1+$2`2],[:NAT,NAT:]);
definition
func Fib -> sequence of [:NAT, NAT:] means :Def1:
it.0 = [0,1] &
for n being Nat holds it.(n+1) = [ (it.n)`2, (it.n)`1 + (it.n)`2 ];
existence
proof
consider fib being sequence of [: NAT, NAT :] such that
A1: fib.0 = [0,1] & for n being Nat holds fib.(n+1) = F(n,(fib.n))
from NAT_1:sch 12;
take fib;
thus fib.0 = [0,1] by A1;
let n be Nat;
fib.(n+1) = F(n,(fib.n)) by A1;
hence thesis;
end;
uniqueness
proof
let fib1,fib2 be sequence of [:NAT, NAT:] such that
A3: fib1.0 = [0,1] and
A4: for n being Nat holds fib1.(n+1) =[(fib1.n)`2, (fib1.n)`1 + (fib1.n)`2];
A5: for n being Nat holds fib1.(n+1) = F(n,fib1.n) by A4;
assume that
A7: fib2.0 = [0,1] and
A8: for n being Nat holds fib2.(n+1) = [(fib2.n)`2, (fib2.n)`1 + (fib2.n)`2];
A9: for n being Nat holds fib2.(n+1) = F(n,(fib2.n)) by A8;
thus fib1 = fib2 from NAT_1:sch 16(A3,A5,A7,A9);
end;
end;
definition
let n be Nat;
func Fib n -> Element of NAT equals
(Fib.n)`1;
coherence;
end;
theorem
Fib(0) = 0 & Fib(1) = 1 &
for n being Nat holds Fib((n+1)+1) = Fib(n) + Fib(n+1)
proof
A1: Fib.0 = [0,1] by Def1;
A3: for n being Nat holds Fib.(n+1) = [(Fib.n)`2, (Fib.n)`1 + (Fib.n)`2]
by Def1;
thus Fib (0) = [0, 1]`1 by Def1
.= 0;
thus Fib (1) = (Fib.(0+1))`1
.= ([ (Fib.0)`2, (Fib.0)`1 + (Fib.0)`2 ])`1 by A3
.= 1 by A1;
let n be Nat;
A4: (Fib.(n+1))`1 = [ (Fib.n)`2, (Fib.n)`1 + (Fib.n)`2 ]`1 by A3
.= (Fib.n)`2;
thus Fib((n+1)+1) = [ (Fib.(n+1))`2, (Fib.(n+1))`1 + (Fib.(n+1))`2 ]`1 by A3
.= [ (Fib.n)`2, (Fib.n)`1 + (Fib.n)`2 ]`2 by A3
.= Fib(n) + Fib(n+1) by A4;
end;
:: Fusc function auxiliaries
theorem
for i being Integer holds i div 1 = i;
theorem
for i, j being Integer st j > 0 & i div j = 0 holds i < j
proof
let i, j be Integer;
assume that
A1: j > 0 and
A2: i div j = 0;
[\ i / j /] = 0 by A2,INT_1:def 9;
then i/j - 1 < 0 by INT_1:def 6;
then i/j < 0+1 by XREAL_1:19;
then i/j*j < 1*j by A1,XREAL_1:68;
hence thesis by A1,XCMPLX_1:87;
end;
theorem
for i, j being Integer st 0<=i & i<j holds i div j = 0
proof
let i, j be Integer;
assume
A1: 0 <= i & i < j;
then i / j < j / j by XREAL_1:74;
then i / j < 0+1 by A1,XCMPLX_1:60;
then i/j - 1 < 0 by XREAL_1:19;
then [\ i / j /] = 0 by A1,INT_1:def 6;
hence thesis by INT_1:def 9;
end;
theorem
for i, j, k being Integer st k >= 0 holds
(i div j) div k = i div (j*k)
proof
let i, j, k be Integer;
set A = [\ [\ i / j /] / k /];
set D = [\ i/(j*k) /];
A = [\ i / j /] div k by INT_1:def 9;
then
A1: A = (i div j) div k by INT_1:def 9;
assume k >= 0; then
per cases;
suppose A2: k > 0;
A3: now
[\ i / j /] / k - 1 < A by INT_1:def 6;
then
A4: [\ i / j /] / k < A+1 by XREAL_1:19;
assume A < D;
then A+1 <= D by INT_1:7;
then [\ i / j /] / k < D by A4,XXREAL_0:2;
then ([\ i / j /] / k) * k < D * k by A2,XREAL_1:68;
then [\ i / j /] < D * k by A2,XCMPLX_1:87;
then
A5: [\ i / j /] + 1 <= D * k by INT_1:7;
[\ i/(j*k) /] <= i/(j*k) by INT_1:def 6;
then [\ i/(j*k) /] * k <= i/(j*k) * k by A2,XREAL_1:64;
then [\ i/(j*k) /] * k <= i/j/k * k by XCMPLX_1:78;
then
A6: [\ i/(j*k) /] * k <= i/j by A2,XCMPLX_1:87;
i/j - 1 < [\ i/j /] by INT_1:def 6;
then i/j < [\ i/j /] + 1 by XREAL_1:19;
hence contradiction by A6,A5,XXREAL_0:2;
end;
A7: now
[\ i/j /] <= i/j by INT_1:def 6;
then [\ i/j /] / k <= (i/j) / k by A2,XREAL_1:72;
then A <= [\ i / j /] / k & [\ i/j /] / k <= i/(j * k)
by INT_1:def 6,XCMPLX_1:78;
then
A8: A <= i/(j * k) by XXREAL_0:2;
i/(j*k)-1 < D by INT_1:def 6;
then
A9: i/(j*k) < D+1 by XREAL_1:19;
assume D < A;
then D+1 <= A by INT_1:7;
hence contradiction by A9,A8,XXREAL_0:2;
end;
D = i div (j*k) by INT_1:def 9;
hence thesis by A3,A7,A1,XXREAL_0:1;
end;
suppose k = 0;
hence thesis;
end;
end;
theorem
for i being Integer holds i mod 2 = 0 or i mod 2 = 1
proof
let i be Integer;
set A = (i div 2)*2;
set M = i mod 2;
i div 2 = [\ i / 2 /] by INT_1:def 9;
then i/2-1<i div 2 by INT_1:def 6;
then (i/2-1)*2 < A by XREAL_1:68;
then -(i-2) > -A by XREAL_1:24;
then i+(2-i) > i+-A by XREAL_1:6;
then 2 > i-A;
then
A2: 2 > M by INT_1:def 10;
reconsider M as Element of NAT by INT_1:3;
M in { k where k is Nat : k < 2 } by A2;
then M in 2 by AXIOMS:4;
hence thesis by CARD_1:50,TARSKI:def 2;
end;
theorem
for i being Integer st i is Element of NAT holds i div 2 is Element of NAT
proof
let i be Integer;
assume i is Element of NAT;
then reconsider n = i as Element of NAT;
n >= 0;
then i/2 >= 0/2;
then [\i/2/] is Element of NAT by INT_1:3;
hence thesis by INT_1:def 9;
end;
theorem Th8:
for a, b, c being Real st a <= b & c >= 1 holds
c to_power a <= c to_power b
proof
let a, b, c be Real;
assume a <= b;
then
A1: a < b or a = b by XXREAL_0:1;
assume c >= 1;
then per cases by XXREAL_0:1;
suppose c > 1;
hence thesis by A1,POWER:39;
end;
suppose
A2: c = 1;
1 to_power a = 1 & 1 to_power b = 1 by POWER:26;
hence thesis by A2;
end;
end;
theorem Th9:
for r,s be Real st
r >= s holds [\r/] >= [\s/] & [/r\] >= [/s\]
proof
let r,s be Real;
assume
A1: r >= s;
A2: [\r/] <= r & r - 1 < [\r/] &
[\s/] <= s & s - 1 < [\s/] by INT_1:def 6;
A3: [/r\] >= r & r + 1 > [/r\] &
[/s\] >= s & s + 1 > [/s\] by INT_1:def 7;
assume not thesis; then
per cases;
suppose
[\r/] < [\s/]; then
B2: [\r/] + 1 <= [\s/] by INT_1:7;
(r - 1) + 1 < [\r/] + 1 by A2,XREAL_1:6; then
r < [\s/] & [\s/] <= s by INT_1:def 6,B2,XXREAL_0:2;
hence contradiction by A1,XXREAL_0:2;
end;
suppose
[/r\] < [/s\]; then
B2: [/r\] + 1 <= [/s\] by INT_1:7;
r + 1 <= [/r\] + 1 by A3,XREAL_1:6; then
r + 1 <= [/s\] & [/s\] < s + 1 by B2,INT_1:def 7,XXREAL_0:2; then
r + 1 < s + 1 by XXREAL_0:2;
hence contradiction by A1,XREAL_1:6;
end;
end;
theorem Th10:
for a, b, c being Real st a > 1 & b > 0 & c >= b holds
log (a, c) >= log (a, b)
proof
let a, b, c be Real;
assume that
A1: a > 1 & b > 0 and
A2: c >= b;
c > b or c = b by A2,XXREAL_0:1;
hence thesis by A1,POWER:57;
end;
theorem Th11:
for n being Nat st n > 0 holds
[\ log (2, 2*n) /] +1 <> [\ log (2, 2*n + 1) /]
proof
let n be Nat;
set l22n = log (2, 2*n);
set l22np1 = log (2, 2*n + 1);
set k = [\ l22n + 1 /];
l22n+1-1 < k by INT_1:def 6;
then
A1: 2 to_power l22n < 2 to_power k by POWER:39;
assume
A2: n > 0;
then
A3: 2*n < 2 to_power k by A1,POWER:def 3;
assume [\ log (2, 2*n) /] +1 = [\ log (2, 2*n + 1) /];
then
A4: [\l22n+1/] = [\l22np1/] by INT_1:28;
then k <= l22np1 by INT_1:def 6;
then 2 to_power k <= 2 to_power l22np1 by Th8;
then
A5: 2 to_power k <= 2*n + 1 by POWER:def 3;
0+1 <= 2*n + 1 by XREAL_1:7;
then log (2, 1) <= l22np1 by Th10;
then 0 <= l22np1 by POWER:51;
then [\ 0 /] <= k by A4;
then reconsider k as Element of NAT by INT_1:3;
reconsider T2tpk = 2 |^ k as Element of NAT;
2*n < T2tpk by A3,POWER:41;
then
A6: 2*n + 1 <= T2tpk by NAT_1:13;
T2tpk <= 2*n + 1 by A5,POWER:41;
then
A7: T2tpk = 2*n+1 by A6,XXREAL_0:1;
per cases by NAT_1:6;
suppose
k = 0;
then 1-1 = 2*n+1-1 by A7,NEWTON:4;
hence contradiction by A2;
end;
suppose
ex m being Nat st k = m + 1;
then consider m being Nat such that
A8: k = m + 1;
reconsider m as Element of NAT by ORDINAL1:def 12;
2*2|^m + 0 = 2*n+1 by A7,A8,NEWTON:6;
then 0 = (2*n+1) mod 2;
hence contradiction by NAT_D:def 2;
end;
end;
theorem Th12:
for n being Nat st n > 0 holds
[\ log (2, 2*n) /] +1 >= [\ log (2, 2*n + 1) /]
proof
let n be Nat;
set l22n = log (2, 2*n);
set l22np1 = log (2, 2*n + 1);
assume
A1: n > 0;
then 0+1 <= n by NAT_1:13;
then 1 < 1 * n + n by XREAL_1:8;
then 2 * n + 1 < 2 * n + 2 * n by XREAL_1:8;
then
A2: log (2, 2*n+1) <= log (2, 2*(2*n)) by Th10;
log (2,2*(2*n)) = log (2,2)+l22n by A1,POWER:53
.= l22n + 1 by POWER:52;
then [\l22np1/] <= [\l22n+1/] by A2,Th9;
hence thesis by INT_1:28;
end;
theorem Th13:
for n being Nat st n > 0 holds [\ log(2, 2*n) /] = [\ log(2, 2*n + 1) /]
proof
let n be Nat;
set l22n = log (2, 2*n);
set l22np1 = log (2, 2*n + 1);
assume
A1: n > 0;
then [\l22np1/] <> [\l22n/] + 1 & [\l22np1/] <= [\l22n/] + 1 by Th11,Th12;
then [\l22np1/] < [\l22n/] + 1 by XXREAL_0:1;
then
A2: [\l22np1/] <= [\l22n/]+1-1 by INT_1:7;
l22n <= l22np1 by A1,Th10,NAT_1:11;
then [\l22n/] <= [\l22np1/] by Th9;
hence thesis by A2,XXREAL_0:1;
end;
theorem
for n being Nat st n > 0 holds [\ log(2, n) /] + 1 = [\ log(2, 2*n + 1 ) /]
proof
let n be Nat;
assume
A1: n > 0;
then [\ log(2, 2*n + 1) /] = [\ log(2, 2*n) /] by Th13
.= [\ log (2, 2) + log(2, n) /] by A1,POWER:53
.= [\ log(2, n) + 1 /] by POWER:52
.= [\ log(2, n) /] + 1 by INT_1:28;
hence thesis;
end;
:: Fusc sequence
defpred P[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 be Nat for x be Element of NAT* ex y be Element of NAT*
st P[n,x,y]
proof
let n be Nat, x be Element of NAT*;
n+2 mod 2 = 0 or n+2 mod 2 <> 0;
then consider y being FinSequence of NAT such that
A1: n+2 mod 2 = 0 & y = x^<*x/.(n+2 div 2)*> or n+2 mod 2 <> 0 & y = x^
<*(x/.(n+2 div 2))+(x/.((n+2 div 2) + 1))*>;
reconsider y as Element of NAT* by FINSEQ_1:def 11;
take y;
hereby
let k be Nat;
assume n+2 = 2*k;
hence y = x^<*x/.k*> by A1;
end;
hereby
let k be Nat;
assume
A2: n+2 = 2*k+1;
then n+2 div 2 = k by NAT_D:def 1;
hence y = x^<*(x/.k)+(x/.(k+1))*> by A1,A2,NAT_D:def 2;
end;
end;
defpred Q[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 be Nat,x,y1,y2 be Element of NAT* st Q[n,x,y1] & Q[n,x,y2] holds y1
= y2
proof
let n be Nat, x, y1, y2 be Element of NAT*;
assume
A1: ( for k being Element of NAT st n+2 = 2*k holds y1 = x^<*x/.k*>)&
for k being Element of NAT st n+2 = 2*k+1 holds y1 = x^<*(x/.k)+(x /.(k+1))*>;
n+2 = 2*(n+2 div 2)+(n+2 mod 2) by NAT_D:2;
then
A2: n+2 = 2*(n+2 div 2)+0 or n+2 = 2*(n+2 div 2)+1 by NAT_D:12;
assume ( for k being Element of NAT st n+2 = 2*k holds y2 = x^<*x/.k*>)&
for k being Element of NAT st n+2 = 2*k+1 holds y2 = x^<*(x/.k)+(x /.(k+1))*>;
then
y1 = x^<*x/.(n+2 div 2)*> & y2 = x^<*x/.(n+2 div 2)*> or y1 = x^<*(x/.(n
+2 div 2))+(x/.(n+2 div 2+1))*> & y2 = x^<*(x/.(n+2 div 2))+(x/.(n+2 div 2+1))
*> by A1,A2;
hence thesis;
end;
definition
let n be Nat;
func Fusc n -> Element of NAT means
:Def2:
it = 0 if n = 0 otherwise
ex l being Element of NAT, 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
reconsider single1 = <*1*> as Element of NAT* by FINSEQ_1:def 11;
consider fusc being sequence of NAT* such that
Lm3: fusc.0 = single1 and
Lm4: for n being Nat holds P[n,fusc.n,fusc.(n+1)] from RECDEF_1:sch 2(Lm1);
thus n = 0 implies ex k being Element of NAT st k = 0;
assume n <> 0;
then consider l being Nat such that
A1: n = l+1 by NAT_1:6;
reconsider IT = ((fusc.l)/.n) as Element of NAT;
reconsider l9 = l as Element of NAT by ORDINAL1:def 12;
take IT, l9;
thus thesis by A1,Lm3,Lm4;
end;
uniqueness
proof
reconsider single1 = <*1*> as Element of NAT* by FINSEQ_1:def 11;
let n1, n2 be Element of NAT;
thus n = 0 & n1 = 0 & n2 = 0 implies n1 = n2;
assume n <> 0;
given l1 being Element of NAT, fusc1 being sequence of NAT* such that
A2: l1+1 = n & n1 = (fusc1.l1)/.n and
A3: fusc1.0 = <*1*> and
A4: for n being Nat holds (for k being Nat st n+2 = 2*k holds fusc1.(
n+1) = (fusc1.n)^ <*(fusc1.n)/.k*>) &
for k being Nat st n+2 = 2*k+1 holds fusc1.(n+1) = (fusc1.n
)^<*((fusc1.n)/.k)+ ((fusc1.n)/.(k+1))
*>;
A5: fusc1.0 = single1 by A3;
A6: for n being Nat holds Q[n,fusc1.n,fusc1.(n+1)] by A4;
given l2 being Element of NAT, fusc2 being sequence of NAT* such that
A7: l2+1 = n & n2 = (fusc2.l2)/.n and
A8: fusc2.0 = <*1*> and
A9: for n being Nat holds (for k being Nat st n+2 = 2*k holds fusc2.(
n+1) = (fusc2.n)^ <*(fusc2.n)/.k*>) &
for k being Nat st n+2 = 2*k+1 holds fusc2.(n+1) = (fusc2.n
)^<*((fusc2.n)/.k)+ ((fusc2.n)/.(k+1))
*>;
A10: for n being Nat holds Q[n,fusc2.n,fusc2.(n+1)] by A9;
A11: fusc2.0 = single1 by A8;
fusc1 = fusc2 from NAT_1:sch 14(A5,A6,A11,A10,Lm2);
hence thesis by A2,A7;
end;
end;
theorem Th15:
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
reconsider single1 = <*1*> as Element of NAT* by FINSEQ_1:def 11;
consider fusc being sequence of NAT* such that
Lm3: fusc.0 = single1 and
Lm4: for n being Nat holds P[n,fusc.n,fusc.(n+1)] from RECDEF_1:sch 2(Lm1);
thus
A1: Fusc 0 = 0 by Def2;
0+1 = 1 & 1 = (<*1*>)/.1 by FINSEQ_4:16;
hence Fusc 1 = 1 by Def2,Lm3,Lm4;
let n be Nat;
per cases;
suppose n = 0;
hence thesis by A1;
end;
suppose n <> 0;
then consider l being Nat such that
A2: n = l+1 by NAT_1:6;
defpred P[Nat] means len (fusc.$1) = $1+1 & for k being Element
of NAT st k <= $1 holds (fusc.$1)/.(k+1) = Fusc (k+1);
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume that
A4: len (fusc.n) = n+1 and
A5: for k being Element of NAT st k <= n holds (fusc.n)/.(k+1) = Fusc ( k+1);
A6: len <*((fusc.n)/.(n+2 div 2))+((fusc.n)/.(n+2 div 2+1))*> = 1 by
FINSEQ_1:40;
n+2 = 2*(n+2 div 2)+(n+2 mod 2) by NAT_D:2;
then
A7: n+2=2*(n+2 div 2)+0 or n+2=2*(n+2 div 2)+1 by NAT_D:12;
A8: len <*((fusc.n)/.(n+2 div 2))*> = 1 by FINSEQ_1:40;
per cases by A7;
suppose
n+2 = 2*(n+2 div 2);
then
A9: fusc.(n+1) = fusc.n^<*(fusc.n)/.(n+2 div 2)*> by Lm4;
hence len (fusc.(n+1)) = n+1+1 by A4,A8,FINSEQ_1:22;
let k be Element of NAT;
A10: now
assume
A11: k <= n;
then 0+1 <= k+1 & k+1 <= n+1 by XREAL_1:7;
then k+1 in dom (fusc.n) by A4,FINSEQ_3:25;
hence (fusc.(n+1))/.(k+1) = (fusc.n)/.(k+1) by A9,FINSEQ_4:68
.= Fusc (k+1) by A5,A11;
end;
assume k <= n+1;
then k = n+1 or k <= n by NAT_1:8;
hence thesis by A10,Def2,Lm3,Lm4;
end;
suppose
n+2 = 2*(n+2 div 2)+1;
then
A12: fusc.(n+1)=fusc.n^<*((fusc.n)/.(n+2 div 2))+((fusc.n)/.(n+ 2 div
2+1) )*> by Lm4;
hence len (fusc.(n+1)) = n+1+1 by A4,A6,FINSEQ_1:22;
let k be Element of NAT;
A13: now
assume
A14: k <= n;
then 0+1 <= k+1 & k+1 <= n+1 by XREAL_1:7;
then k+1 in dom (fusc.n) by A4,FINSEQ_3:25;
hence (fusc.(n+1))/.(k+1) = (fusc.n)/.(k+1) by A12,FINSEQ_4:68
.= Fusc (k+1) by A5,A14;
end;
assume k <= n+1;
then k = n+1 or k <= n by NAT_1:8;
hence thesis by A13,Def2,Lm3,Lm4;
end;
end;
reconsider l,n1=n as Element of NAT by ORDINAL1:def 12;
2*l+1+(1+1) = 2*l+1+1+1;
then
A15: fusc.(2*n1) = fusc.(2*l+1)^ <*((fusc.(2*l+1))/.n1)+((fusc.(2*l+1))/.(
n1+1))*> by A2,Lm4;
A16: P[0]
proof
thus len (fusc.0) = 0+1 by Lm3,FINSEQ_1:40;
let k be Element of NAT;
assume k <= 0;
then k = 0;
hence thesis by Def2,Lm3,Lm4;
end;
A17: for n being Nat holds P[n] from NAT_1:sch 2(A16,A3);
then
A18: len (fusc.(2*l+1)) = 2*l+1+1;
A19: l+l = (1+1)*l;
then
A20: l <= 2*l by NAT_1:11;
then
A21: Fusc (n+1) = (fusc.(2*l+1))/.(n+1) by A2,A17,XREAL_1:7;
A22: len (fusc.(2*l)) = 2*l+1 by A17;
2*l <= 2*l+1 by NAT_1:11;
then
A23: Fusc n = (fusc.(2*l+1))/.n by A2,A17,A20,XXREAL_0:2;
reconsider nn=2*n as Element of NAT by ORDINAL1:def 12;
2*n = 2*l+2*1 by A2;
then fusc.(2*l+1) = fusc.(2*l)^<*(fusc.(2*l))/.n1*> by Lm4;
hence Fusc (2*n) = (fusc.(2*l)^<*(fusc.(2*l))/.n*>)/.(2*l+1+1) by A2,Def2
,Lm3,Lm4
.= (fusc.(2*l))/.n by A22,FINSEQ_4:67
.= Fusc n by A2,A17,A19,NAT_1:11;
thus Fusc (2*n+1) = (fusc.nn)/.(2*n+1) by Def2,Lm3,Lm4
.= Fusc n + Fusc (n+1) by A2,A18,A15,A23,A21,FINSEQ_4:67;
end;
end;
:: Auxiliary functions specific for Fib and Fusc of little general interest
theorem
for n being Nat st n <> 0 holds n < 2*n
proof
let n be Nat;
assume that
A1: n <> 0 and
A2: 2*n <= n;
per cases by A2,XXREAL_0:1;
suppose 2*n = n;
hence contradiction by A1;
end;
suppose 2*n < n;
then 2*n+-(1*n) < 1*n+-(1*n) by XREAL_1:6;
hence contradiction by NAT_1:2;
end;
end;
theorem
for n being Nat holds n < 2*n+1
proof
let n be Nat;
assume 2*n+1 <= n;
then 2*n+1 <= n + n by NAT_1:12;
hence contradiction by NAT_1:13;
end;
theorem
for A, B being Nat holds B = A * Fusc 0 + B * Fusc 1 by Th15;
theorem
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
let n, A, B, N be Nat such that
A1: Fusc N = A * Fusc (2*n+1) + B * Fusc (2*n+1+1);
2*n+1+1 = 2* (n + 1) & Fusc (2*n+1) = Fusc n+Fusc(n+1) by Th15;
hence Fusc N = A*Fusc n+A*Fusc (n+1)+B*Fusc (n+1) by A1,Th15
.= A * Fusc n + (B+A) * Fusc (n+1);
end;
theorem
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
let n, A, B, N be Nat such that
A1: Fusc N = A * Fusc (2*n) + B * Fusc (2*n+1);
Fusc (2*n+1) = Fusc n + Fusc (n+1) by Th15;
hence Fusc N = A*Fusc n+(B*Fusc n +B*Fusc (n+1)) by A1,Th15
.= (A+B)*Fusc n + B*Fusc (n+1);
end;