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; :: thesis: ( 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; :: thesis: for n being Nat holds
( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) )
let n be Nat; :: thesis: ( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) )
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: ( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) )
hence ( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) ) by A1; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: ( 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]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
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) ; :: thesis: S3[n + 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 ( n + 2 = 2 * ((n + 2) div 2) or n + 2 = (2 * ((n + 2) div 2)) + 1 ) by A7;
suppose n + 2 = 2 * ((n + 2) div 2) ; :: thesis: S3[n + 1]
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; :: thesis: for k being Element of NAT st k <= n + 1 holds
(fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
let k be Element of NAT ; :: thesis: ( k <= n + 1 implies (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1) )
A10: now :: thesis: ( k <= n implies (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1) )
assume A11: k <= n ; :: thesis: (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
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 ;
:: thesis: verum
end;
assume k <= n + 1 ; :: thesis: (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
then ( k = n + 1 or k <= n ) by NAT_1:8;
hence (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1) by A10, Def2, Lm3, Lm4; :: thesis: verum
end;
suppose n + 2 = (2 * ((n + 2) div 2)) + 1 ; :: thesis: S3[n + 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; :: thesis: for k being Element of NAT st k <= n + 1 holds
(fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
let k be Element of NAT ; :: thesis: ( k <= n + 1 implies (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1) )
A13: now :: thesis: ( k <= n implies (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1) )
assume A14: k <= n ; :: thesis: (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
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 ;
:: thesis: verum
end;
assume k <= n + 1 ; :: thesis: (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
then ( k = n + 1 or k <= n ) by NAT_1:8;
hence (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1) by A13, Def2, Lm3, Lm4; :: thesis: verum
end;
end;
end;
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 ]
proof
thus len (fusc . 0) = 0 + 1 by Lm3, FINSEQ_1:40; :: thesis: for k being Element of NAT st k <= 0 holds
(fusc . 0) /. (k + 1) = Fusc (k + 1)
let k be Element of NAT ; :: thesis: ( k <= 0 implies (fusc . 0) /. (k + 1) = Fusc (k + 1) )
assume k <= 0 ; :: thesis: (fusc . 0) /. (k + 1) = Fusc (k + 1)
then k = 0 ;
hence (fusc . 0) /. (k + 1) = Fusc (k + 1) by Def2, Lm3, Lm4; :: thesis: verum
end;
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 ;
:: thesis: 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 ; :: thesis: verum
end;
end;