:: PRE_FF semantic presentation

begin

definition
let n be Nat;
func Fib n ->  Element of 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 Element of 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
deffunc H1( set , Element of [:NAT,NAT:]) ->  Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
reconsider n = n as Element of NAT by ORDINAL1:def_12;
consider fib being Function of NAT,[:NAT,NAT:] such that
A1: ( fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = H1(n,fib . n) ) ) from NAT_1:sch_12();
take  (fib . n) `1 ; ::_thesis: ex fib being Function of NAT,[:NAT,NAT:] st
( (fib . n) `1 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) )
take  fib ; ::_thesis: ( (fib . n) `1 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) )
thus  ( (fib . n) `1 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of 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
deffunc H1( set , Element of [:NAT,NAT:]) ->  Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
let it1, it2 be Element of NAT ; ::_thesis: ( ex fib being Function of NAT,[:NAT,NAT:] st
( it1 = (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
( it2 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) implies it1 = it2 )
given fib1 being Function of NAT,[:NAT,NAT:] such that A2: it1 = (fib1 . n) `1 and
A3: fib1 . 0 = [0,1] and
A4: for n being Nat holds fib1 . (n + 1) = H1(n,fib1 . n) ; ::_thesis: ( for fib being Function of NAT,[:NAT,NAT:] holds
( not it2 = (fib . n) `1 or not fib . 0 = [0,1] or ex n being Nat st not fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) or it1 = it2 )
given fib2 being Function of NAT,[:NAT,NAT:] such that A5: it2 = (fib2 . n) `1 and
A6: fib2 . 0 = [0,1] and
A7: for n being Nat holds fib2 . (n + 1) = H1(n,fib2 . n) ; ::_thesis: it1 = it2
 fib1 = fib2 from NAT_1:sch_16(A3, A4, A6, A7);
hence  it1 = it2 by A2, A5; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Fib PRE_FF:def_1_:_
 for n being Nat
for b2 being Element of 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
( Fib 0 = 0 & Fib 1 = 1 & ( for n being Nat holds Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1)) ) )
proof
deffunc H1( set , Element of [:NAT,NAT:]) ->  Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
consider fib being Function of NAT,[:NAT,NAT:] such that
A1: fib . 0 = [0,1] and
A2: for n being Nat holds fib . (n + 1) = H1(n,fib . n) from NAT_1:sch_12();
thus  Fib 0 = [0,1] `1 by A1, A2, Def1
.= 0 by MCART_1:7 ; ::_thesis: ( Fib 1 = 1 & ( for n being Nat holds Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1)) ) )
thus  Fib 1 = (fib . (0 + 1)) `1 by A1, A2, Def1
.= [((fib . 0) `2),(((fib . 0) `1) + ((fib . 0) `2))] `1 by A2
.= [0,1] `2 by A1, MCART_1:7
.= 1 by MCART_1:7 ; ::_thesis: for n being Nat holds Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1))
let n be Nat; ::_thesis: Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1))
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A3: (fib . (n + 1)) `1 = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] `1 by A2
.= (fib . n) `2 by MCART_1:7 ;
Fib ((n + 1) + 1) = (fib . ((n + 1) + 1)) `1 by A1, A2, Def1
.= [((fib . (n + 1)) `2),(((fib . (n + 1)) `1) + ((fib . (n + 1)) `2))] `1 by A2
.= (fib . (n + 1)) `2 by MCART_1:7
.= [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] `2 by A2
.= ((fib . n) `1) + ((fib . (n + 1)) `1) by A3, MCART_1:7
.= (Fib n) + ((fib . (n + 1)) `1) by A1, A2, Def1
.= (Fib n) + (Fib (n + 1)) by A1, A2, Def1 ;
hence  Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1)) ; ::_thesis: verum
end;

theorem :: PRE_FF:2
for i being Integer holds i div 1 = i
proof
let i be Integer; ::_thesis: i div 1 = i
thus i div 1 = [\(i / 1)/] by INT_1:def_9
.= i by INT_1:25 ; ::_thesis: verum
end;

theorem :: PRE_FF:3
for i, j being Integer st j > 0 & i div j = 0 holds
i < j
proof
let i, j be Integer; ::_thesis: ( j > 0 & i div j = 0 implies i < j )
assume that
A1: j > 0 and
A2: i div j = 0 ; ::_thesis: i < j
 [\(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  i < j by A1, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: PRE_FF:4
for i, j being Integer st 0 <= i & i < j holds
i div j = 0
proof
let i, j be Integer; ::_thesis: ( 0 <= i & i < j implies i div j = 0 )
assume A1: ( 0 <= i & i < j ) ; ::_thesis: i div j = 0
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  i div j = 0 by INT_1:def_9; ::_thesis: verum
end;

theorem :: PRE_FF:5
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; ::_thesis: ( k > 0 implies (i div j) div k = i div (j * k) )
set A = [\([\(i / j)/] / k)/];
set D = [\(i / (j * k))/];
 [\([\(i / j)/] / k)/] = [\(i / j)/] div k by INT_1:def_9;
then A1: [\([\(i / j)/] / k)/] = (i div j) div k by INT_1:def_9;
assume A2: k > 0 ; ::_thesis: (i div j) div k = i div (j * k)
A3: now__::_thesis:_not_[\([\(i_/_j)/]_/_k)/]_<_[\(i_/_(j_*_k))/]
 ([\(i / j)/] / k) - 1 < [\([\(i / j)/] / k)/] by INT_1:def_6;
then A4: [\(i / j)/] / k < [\([\(i / j)/] / k)/] + 1 by XREAL_1:19;
assume  [\([\(i / j)/] / k)/] < [\(i / (j * k))/] ; ::_thesis: contradiction
then  [\([\(i / j)/] / k)/] + 1 <= [\(i / (j * k))/] by INT_1:7;
then  [\(i / j)/] / k < [\(i / (j * k))/] by A4, XXREAL_0:2;
then  ([\(i / j)/] / k) * k < [\(i / (j * k))/] * k by A2, XREAL_1:68;
then  [\(i / j)/] < [\(i / (j * k))/] * k by A2, XCMPLX_1:87;
then A5: [\(i / j)/] + 1 <= [\(i / (j * k))/] * 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; ::_thesis: verum
end;
A7: now__::_thesis:_not_[\(i_/_(j_*_k))/]_<_[\([\(i_/_j)/]_/_k)/]
 [\(i / j)/] <= i / j by INT_1:def_6;
then  [\(i / j)/] / k <= (i / j) / k by A2, XREAL_1:72;
then  ( [\([\(i / j)/] / k)/] <= [\(i / j)/] / k & [\(i / j)/] / k <= i / (j * k) ) by INT_1:def_6, XCMPLX_1:78;
then A8: [\([\(i / j)/] / k)/] <= i / (j * k) by XXREAL_0:2;
 (i / (j * k)) - 1 < [\(i / (j * k))/] by INT_1:def_6;
then A9: i / (j * k) < [\(i / (j * k))/] + 1 by XREAL_1:19;
assume  [\(i / (j * k))/] < [\([\(i / j)/] / k)/] ; ::_thesis: contradiction
then  [\(i / (j * k))/] + 1 <= [\([\(i / j)/] / k)/] by INT_1:7;
hence  contradiction by A9, A8, XXREAL_0:2; ::_thesis: verum
end;
 [\(i / (j * k))/] = i div (j * k) by INT_1:def_9;
hence  (i div j) div k = i div (j * k) by A3, A7, A1, XXREAL_0:1; ::_thesis: verum
end;

theorem :: PRE_FF:6
for i being Integer holds
( i mod 2 = 0 or i mod 2 = 1 )
proof
let i be Integer; ::_thesis: ( i mod 2 = 0 or i mod 2 = 1 )
set A = (i div 2) * 2;
set M = i mod 2;
A1: 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 < (i div 2) * 2 by XREAL_1:68;
then  - (i - 2) > - ((i div 2) * 2) by XREAL_1:24;
then  i + (2 - i) > i + (- ((i div 2) * 2)) by XREAL_1:6;
then  2 > i - ((i div 2) * 2) ;
then A2: 2 > i mod 2 by INT_1:def_10;
 i div 2 <= i / 2 by A1, INT_1:def_6;
then  (i div 2) * 2 <= (i / 2) * 2 by XREAL_1:64;
then  - i <= - ((i div 2) * 2) by XREAL_1:24;
then  i + (- i) <= i + (- ((i div 2) * 2)) by XREAL_1:6;
then  0 <= i - ((i div 2) * 2) ;
then  0 <= i mod 2 by INT_1:def_10;
then reconsider M = i mod 2 as Element of NAT by INT_1:3;
 M in  {  k where k is Element of NAT : k < 2  }  by A2;
then  M in 2 by AXIOMS:4;
hence  ( i mod 2 = 0 or i mod 2 = 1 ) by CARD_1:50, TARSKI:def_2; ::_thesis: verum
end;

theorem :: PRE_FF:7
for i being Integer st i is Element of NAT holds
i div 2 is Element of NAT
proof
let i be Integer; ::_thesis: ( i is Element of NAT implies i div 2 is Element of NAT )
assume  i is Element of NAT ; ::_thesis: i div 2 is Element of NAT
then reconsider n = i as Element of NAT ;
 (i / 2) - 1 < [\(i / 2)/] by INT_1:def_6;
then A1: i / 2 < [\(i / 2)/] + 1 by XREAL_1:19;
 n >= 0 ;
then  i / 2 >= 0 / 2 ;
then  [\(i / 2)/] is Element of NAT by A1, INT_1:3, INT_1:7;
hence  i div 2 is Element of NAT by INT_1:def_9; ::_thesis: verum
end;

theorem Th8: :: PRE_FF:8
for a, b, c being real number st a <= b & c > 1 holds
c to_power a <= c to_power b
proof
let a, b, c be real number ; ::_thesis: ( a <= b & c > 1 implies c to_power a <= c to_power b )
assume  a <= b ; ::_thesis: ( not c > 1 or c to_power a <= c to_power b )
then  ( a < b or a = b ) by XXREAL_0:1;
hence  ( not c > 1 or c to_power a <= c to_power b ) by POWER:39; ::_thesis: verum
end;

theorem Th9: :: PRE_FF:9
for r, s being real number st r >= s holds
[\r/] >= [\s/]
proof
let r, s be real number ; ::_thesis: ( r >= s implies [\r/] >= [\s/] )
assume A1: r >= s ; ::_thesis: [\r/] >= [\s/]
A2: [\s/] <= s by INT_1:def_6;
 r - 1 < [\r/] by INT_1:def_6;
then A3: (r - 1) + 1 < [\r/] + 1 by XREAL_1:6;
assume  [\r/] < [\s/] ; ::_thesis: contradiction
then  [\r/] + 1 <= [\s/] by INT_1:7;
then  r < [\s/] by A3, XXREAL_0:2;
hence  contradiction by A1, A2, XXREAL_0:2; ::_thesis: verum
end;

theorem Th10: :: PRE_FF:10
for a, b, c being real number st a > 1 & b > 0 & c >= b holds
log (a,c) >= log (a,b)
proof
let a, b, c be real number ; ::_thesis: ( a > 1 & b > 0 & c >= b implies log (a,c) >= log (a,b) )
assume that
A1: ( a > 1 & b > 0 ) and
A2: c >= b ; ::_thesis: log (a,c) >= log (a,b)
 ( c > b or c = b ) by A2, XXREAL_0:1;
hence  log (a,c) >= log (a,b) by A1, POWER:57; ::_thesis: verum
end;

theorem Th11: :: PRE_FF:11
for n being Nat st n > 0 holds
[\(log (2,(2 * n)))/] + 1 <> [\(log (2,((2 * n) + 1)))/]
proof
let n be Nat; ::_thesis: ( n > 0 implies [\(log (2,(2 * n)))/] + 1 <> [\(log (2,((2 * n) + 1)))/] )
set l22n = log (2,(2 * n));
set l22np1 = log (2,((2 * n) + 1));
set k = [\((log (2,(2 * n))) + 1)/];
 ((log (2,(2 * n))) + 1) - 1 < [\((log (2,(2 * n))) + 1)/] by INT_1:def_6;
then A1: 2 to_power (log (2,(2 * n))) < 2 to_power [\((log (2,(2 * n))) + 1)/] by POWER:39;
assume A2: n > 0 ; ::_thesis: [\(log (2,(2 * n)))/] + 1 <> [\(log (2,((2 * n) + 1)))/]
then  2 * 0 < 2 * n by XREAL_1:68;
then A3: 2 * n < 2 to_power [\((log (2,(2 * n))) + 1)/] by A1, POWER:def_3;
assume  [\(log (2,(2 * n)))/] + 1 = [\(log (2,((2 * n) + 1)))/] ; ::_thesis: contradiction
then A4: [\((log (2,(2 * n))) + 1)/] = [\(log (2,((2 * n) + 1)))/] by INT_1:28;
then  [\((log (2,(2 * n))) + 1)/] <= log (2,((2 * n) + 1)) by INT_1:def_6;
then  2 to_power [\((log (2,(2 * n))) + 1)/] <= 2 to_power (log (2,((2 * n) + 1))) by Th8;
then A5: 2 to_power [\((log (2,(2 * n))) + 1)/] <= (2 * n) + 1 by POWER:def_3;
 0 + 1 <= (2 * n) + 1 by XREAL_1:7;
then  log (2,1) <= log (2,((2 * n) + 1)) by Th10;
then  0 <= log (2,((2 * n) + 1)) by POWER:51;
then  [\0/] <= [\((log (2,(2 * n))) + 1)/] by A4, Th9;
then  0 <= [\((log (2,(2 * n))) + 1)/] by INT_1:25;
then reconsider k = [\((log (2,(2 * n))) + 1)/] as Element of NAT by INT_1:3;
reconsider 2tpk = 2 |^ k as Element of NAT ;
 2 * n < 2tpk by A3, POWER:41;
then A6: (2 * n) + 1 <= 2tpk by NAT_1:13;
 2tpk <= (2 * n) + 1 by A5, POWER:41;
then A7: 2tpk = (2 * n) + 1 by A6, XXREAL_0:1;
percases ( k = 0 or ex m being Nat st k = m + 1 ) by NAT_1:6;
suppose k = 0 ; ::_thesis: contradiction
then  1 - 1 = ((2 * n) + 1) - 1 by A7, NEWTON:4;
hence  contradiction by A2; ::_thesis: verum
end;
suppose ex m being Nat st k = m + 1 ; ::_thesis: contradiction
then consider m being Nat such that
A8: k = m + 1 ;
reconsider m = 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 by NAT_D:def_2;
hence  contradiction by NAT_D:def_2; ::_thesis: verum
end;
end;
end;

theorem Th12: :: PRE_FF:12
for n being Nat st n > 0 holds
[\(log (2,(2 * n)))/] + 1 >= [\(log (2,((2 * n) + 1)))/]
proof
let n be Nat; ::_thesis: ( n > 0 implies [\(log (2,(2 * n)))/] + 1 >= [\(log (2,((2 * n) + 1)))/] )
set l22n = log (2,(2 * n));
set l22np1 = log (2,((2 * n) + 1));
assume A1: n > 0 ; ::_thesis: [\(log (2,(2 * n)))/] + 1 >= [\(log (2,((2 * n) + 1)))/]
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;
 2 * 0 < 2 * n by A1, XREAL_1:68;
then  log (2,(2 * (2 * n))) = (log (2,2)) + (log (2,(2 * n))) by POWER:53
.= (log (2,(2 * n))) + 1 by POWER:52 ;
then  [\(log (2,((2 * n) + 1)))/] <= [\((log (2,(2 * n))) + 1)/] by A2, Th9;
hence  [\(log (2,(2 * n)))/] + 1 >= [\(log (2,((2 * n) + 1)))/] by INT_1:28; ::_thesis: verum
end;

theorem Th13: :: PRE_FF:13
for n being Nat st n > 0 holds
[\(log (2,(2 * n)))/] = [\(log (2,((2 * n) + 1)))/]
proof
let n be Nat; ::_thesis: ( n > 0 implies [\(log (2,(2 * n)))/] = [\(log (2,((2 * n) + 1)))/] )
set l22n = log (2,(2 * n));
set l22np1 = log (2,((2 * n) + 1));
assume A1: n > 0 ; ::_thesis: [\(log (2,(2 * n)))/] = [\(log (2,((2 * n) + 1)))/]
then  ( [\(log (2,((2 * n) + 1)))/] <> [\(log (2,(2 * n)))/] + 1 & [\(log (2,((2 * n) + 1)))/] <= [\(log (2,(2 * n)))/] + 1 ) by Th11, Th12;
then  [\(log (2,((2 * n) + 1)))/] < [\(log (2,(2 * n)))/] + 1 by XXREAL_0:1;
then A2: [\(log (2,((2 * n) + 1)))/] <= ([\(log (2,(2 * n)))/] + 1) - 1 by INT_1:7;
 2 * 0 < 2 * n by A1, XREAL_1:68;
then  log (2,(2 * n)) <= log (2,((2 * n) + 1)) by Th10, NAT_1:11;
then  [\(log (2,(2 * n)))/] <= [\(log (2,((2 * n) + 1)))/] by Th9;
hence  [\(log (2,(2 * n)))/] = [\(log (2,((2 * n) + 1)))/] by A2, XXREAL_0:1; ::_thesis: verum
end;

theorem :: PRE_FF:14
for n being Nat st n > 0 holds
[\(log (2,n))/] + 1 = [\(log (2,((2 * n) + 1)))/]
proof
let n be Nat; ::_thesis: ( n > 0 implies [\(log (2,n))/] + 1 = [\(log (2,((2 * n) + 1)))/] )
assume A1: n > 0 ; ::_thesis: [\(log (2,n))/] + 1 = [\(log (2,((2 * n) + 1)))/]
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  [\(log (2,n))/] + 1 = [\(log (2,((2 * n) + 1)))/] ; ::_thesis: verum
end;

definition
let f be Function of NAT,(NAT *);
let n be Element of NAT ;
:: original: .
redefine funcf . n ->  FinSequence of NAT ;
coherence
 f . n is FinSequence of NAT
proof
 f . n is Element of NAT * ;
hence  f . n is FinSequence of NAT ; ::_thesis: verum
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 Element of NAT
for x being Element of NAT * ex y being Element of NAT * st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of NAT * ex y being Element of NAT * st S1[n,x,y]
let x be Element of NAT * ; ::_thesis: ex y being Element of NAT * st S1[n,x,y]
 ( (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 = y as Element of NAT * by FINSEQ_1:def_11;
take  y ; ::_thesis: S1[n,x,y]
hereby  ::_thesis: for k being Nat st n + 2 = (2 * k) + 1 holds
y = x ^ <*((x /. k) + (x /. (k + 1)))*>
let k be Nat; ::_thesis: ( n + 2 = 2 * k implies y = x ^ <*(x /. k)*> )
assume  n + 2 = 2 * k ; ::_thesis: y = x ^ <*(x /. k)*>
then  n + 2 = (2 * k) + 0 ;
hence  y = x ^ <*(x /. k)*> by A1, NAT_D:def_1, NAT_D:def_2; ::_thesis: verum
end;
hereby  ::_thesis: verum
let k be Nat; ::_thesis: ( n + 2 = (2 * k) + 1 implies y = x ^ <*((x /. k) + (x /. (k + 1)))*> )
assume A2: n + 2 = (2 * k) + 1 ; ::_thesis: y = x ^ <*((x /. k) + (x /. (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; ::_thesis: verum
end;
end;

defpred S2[ 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 being Nat
for x, y1, y2 being Element of NAT * st S2[n,x,y1] & S2[n,x,y2] holds
y1 = y2
proof
let n be Nat; ::_thesis: for x, y1, y2 being Element of NAT * st S2[n,x,y1] & S2[n,x,y2] holds
y1 = y2
let x, y1, y2 be Element of NAT * ; ::_thesis: ( S2[n,x,y1] & S2[n,x,y2] implies y1 = y2 )
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)))*> ) ) ; ::_thesis: ( not S2[n,x,y2] or y1 = y2 )
 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)))*> ) ) ; ::_thesis: y1 = y2
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  y1 = y2 ; ::_thesis: verum
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 Element of NAT holds S1[n,fusc . n,fusc . (n + 1)] from RECDEF_1:sch_2(Lm1);

Lm5:  for n being Nat holds S1[n,fusc . n,fusc . (n + 1)]
proof
let n be Nat; ::_thesis: S1[n,fusc . n,fusc . (n + 1)]
 n in NAT by ORDINAL1:def_12;
hence  S1[n,fusc . n,fusc . (n + 1)] by Lm4; ::_thesis: verum
end;

definition
let n be Nat;
func Fusc n ->  Element of NAT  means :Def2: :: PRE_FF:def 2
it = 0  if n = 0
otherwise  ex l being Element of 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 Element of NAT holds verum ;
existence
 ( ( n = 0 implies ex b1 being Element of NAT st b1 = 0 ) & ( not n = 0 implies ex b1, l being Element of 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
thus  ( n = 0 implies ex k being Element of NAT st k = 0 ) ; ::_thesis: ( not n = 0 implies ex b1, l being Element of 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)))*> ) ) ) ) )
assume  n <> 0 ; ::_thesis: ex b1, l being Element of 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)))*> ) ) ) )
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 ; ::_thesis: ex l being Element of 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)))*> ) ) ) )
take  l9 ; ::_thesis: ex fusc being Function of NAT,(NAT *) st
( l9 + 1 = n & IT = (fusc . l9) /. 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)))*> ) ) ) )
thus  ex fusc being Function of NAT,(NAT *) st
( l9 + 1 = n & IT = (fusc . l9) /. 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)))*> ) ) ) ) by A1, Lm3, Lm5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT holds
( ( n = 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not n = 0 & ex l being Element of 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 Element of 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
let n1, n2 be Element of NAT ; ::_thesis: ( ( n = 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) & ( not n = 0 & ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st
( l + 1 = n & n1 = (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 Element of NAT ex fusc being Function of NAT,(NAT *) st
( l + 1 = n & n2 = (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 n1 = n2 ) )
thus  ( n = 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ; ::_thesis: ( not n = 0 & ex l being Element of NAT ex fusc being Function of NAT,(NAT *) st
( l + 1 = n & n1 = (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 Element of NAT ex fusc being Function of NAT,(NAT *) st
( l + 1 = n & n2 = (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 n1 = n2 )
assume  n <> 0 ; ::_thesis: ( for l being Element of NAT
for fusc being Function of NAT,(NAT *) holds
( not l + 1 = n or not n1 = (fusc . l) /. n or not fusc . 0 = <*1*> or ex n being Nat st
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) implies ex k being Nat st
( n + 2 = (2 * k) + 1 & not fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) or for l being Element of NAT
for fusc being Function of NAT,(NAT *) holds
( not l + 1 = n or not n2 = (fusc . l) /. n or not fusc . 0 = <*1*> or ex n being Nat st
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) implies ex k being Nat st
( n + 2 = (2 * k) + 1 & not fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) or n1 = n2 )
given l1 being Element of NAT , fusc1 being Function of NAT,(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)))*> ) ) ; ::_thesis: ( for l being Element of NAT
for fusc being Function of NAT,(NAT *) holds
( not l + 1 = n or not n2 = (fusc . l) /. n or not fusc . 0 = <*1*> or ex n being Nat st
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) implies ex k being Nat st
( n + 2 = (2 * k) + 1 & not fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) or n1 = n2 )
A5: fusc1 . 0 = single1 by A3;
A6: for n being Nat holds S2[n,fusc1 . n,fusc1 . (n + 1)] by A4;
given l2 being Element of NAT , fusc2 being Function of NAT,(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)))*> ) ) ; ::_thesis: n1 = n2
A10: for n being Nat holds S2[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  n1 = n2 by A2, A7; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Fusc PRE_FF:def_2_:_
 for n being Nat
for b2 being Element of NAT holds
( ( n = 0 implies ( b2 = Fusc n iff b2 = 0 ) ) & ( not n = 0 implies ( b2 = Fusc n iff ex l being Element of 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 Th15: :: PRE_FF:15
( 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
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, Lm5; ::_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)) )
percases ( 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[ Element of 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 Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of 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;
percases ( 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 Lm5;
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, Lm5; ::_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 Lm5;
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, Lm5; ::_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, Lm5;
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, Lm5; ::_thesis: verum
end;
A17: for n being Element of NAT holds S3[n] from NAT_1:sch_1(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;
 2 * n = (2 * l) + (2 * 1) by A2;
then  fusc . ((2 * l) + 1) = (fusc . (2 * l)) ^ <*((fusc . (2 * l)) /. n1)*> by Lm5;
hence  Fusc (2 * n) = ((fusc . (2 * l)) ^ <*((fusc . (2 * l)) /. n)*>) /. (((2 * l) + 1) + 1) by A2, Def2, Lm3, Lm5
.= (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 . (2 * n)) /. ((2 * n) + 1) by Def2, Lm3, Lm5
.= (Fusc n) + (Fusc (n + 1)) by A2, A18, A15, A23, A21, FINSEQ_4:67 ; ::_thesis: verum
end;
end;
end;

theorem :: PRE_FF:16
for n being Nat st n <> 0 holds
n < 2 * n
proof
let n be Nat; ::_thesis: ( n <> 0 implies n < 2 * n )
assume that
A1: n <> 0 and
A2: 2 * n <= n ; ::_thesis: contradiction
percases ( 2 * n = n or 2 * n < n ) by A2, XXREAL_0:1;
suppose 2 * n = n ; ::_thesis: contradiction
hence  contradiction by A1; ::_thesis: verum
end;
suppose 2 * n < n ; ::_thesis: contradiction
then  (2 * n) + (- (1 * n)) < (1 * n) + (- (1 * n)) by XREAL_1:6;
hence  contradiction by NAT_1:2; ::_thesis: verum
end;
end;
end;

theorem :: PRE_FF:17
for n being Nat holds n < (2 * n) + 1
proof
let n be Nat; ::_thesis: n < (2 * n) + 1
assume  (2 * n) + 1 <= n ; ::_thesis: contradiction
then  (2 * n) + 1 <= n + n by NAT_1:12;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;

theorem :: PRE_FF:18
for A, B being Nat holds B = (A * (Fusc 0)) + (B * (Fusc 1)) by Th15;

theorem :: PRE_FF:19
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; ::_thesis: ( Fusc N = (A * (Fusc ((2 * n) + 1))) + (B * (Fusc (((2 * n) + 1) + 1))) implies Fusc N = (A * (Fusc n)) + ((B + A) * (Fusc (n + 1))) )
assume A2: Fusc N = (A * (Fusc ((2 * n) + 1))) + (B * (Fusc (((2 * n) + 1) + 1))) ; ::_thesis: Fusc N = (A * (Fusc n)) + ((B + A) * (Fusc (n + 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 A2, Th15
.= (A * (Fusc n)) + ((B + A) * (Fusc (n + 1))) ;
::_thesis: verum
end;

theorem :: PRE_FF:20
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; ::_thesis: ( Fusc N = (A * (Fusc (2 * n))) + (B * (Fusc ((2 * n) + 1))) implies Fusc N = ((A + B) * (Fusc n)) + (B * (Fusc (n + 1))) )
assume A2: Fusc N = (A * (Fusc (2 * n))) + (B * (Fusc ((2 * n) + 1))) ; ::_thesis: Fusc N = ((A + B) * (Fusc n)) + (B * (Fusc (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 A2, Th15
.= ((A + B) * (Fusc n)) + (B * (Fusc (n + 1))) ;
::_thesis: verum
end;