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 S1[n,fusc . n,fusc . (n + 1)]
from RECDEF_1:sch 2(Lm1);
thus A1:
Fusc 0 = 0
by Def2; ( Fusc 1 = 1 & ( for n being Nat holds
( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) ) ) )
( 0 + 1 = 1 & 1 = <*1*> /. 1 )
by FINSEQ_4:16;
hence
Fusc 1 = 1
by Def2, Lm3, Lm4; for n being Nat holds
( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) )
let n be Nat; ( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) )
per cases
( n = 0 or n <> 0 )
;
suppose
n <> 0
;
( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) )then consider l being
Nat such that A2:
n = l + 1
by NAT_1:6;
defpred S3[
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 being
Nat st
S3[
n] holds
S3[
n + 1]
reconsider l =
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:
S3[
0 ]
A17:
for
n being
Nat holds
S3[
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
;
Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1))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
;
verum end; end;