:: Two Programs for {\bf SCM}. Part I - Preliminaries
::  by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993-2012 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, XBOOLE_0, SUBSET_1, ZFMISC_1, MCART_1, NAT_1, FUNCT_1,
      CARD_1, ARYTM_3, INT_1, XXREAL_0, ARYTM_1, RELAT_1, XREAL_0, ORDINAL1,
      POWER, NEWTON, FINSEQ_1, ORDINAL4, PARTFUN1, PRE_FF;
 notations XBOOLE_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, FINSEQ_1, FINSEQ_2, NAT_1, NEWTON;
 constructors DOMAIN_1, XXREAL_0, REAL_1, NAT_1, NAT_D, MEMBERED, PARTFUN1,
      NEWTON, POWER, SEQ_1, RELSET_1, FINSEQ_2;
 registrations SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
      MEMBERED, XBOOLE_0, FINSEQ_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems TARSKI, AXIOMS, NAT_1, INT_1, MCART_1, POWER, NEWTON, FINSEQ_1,
      FINSEQ_4, FINSEQ_3, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, CARD_1;
 schemes NAT_1, RECDEF_1;

begin :: Fibonacci sequence

:: Definition of fib

definition
  let n be Nat;
  func Fib (n) -> Element of NAT means
  :Def1:
  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
  proof
    deffunc F(set,Element of [: NAT, NAT :]) = [ $2`2, $2`1 + $2`2 ];
    reconsider 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) = F(n,(fib.n))
    from NAT_1:sch 12;
    take (fib.n)`1, fib;
    thus thesis by A1;
  end;
  uniqueness
  proof
    deffunc F(set,Element of [:NAT,NAT:]) = [$2`2, $2`1+$2`2];
    let it1, it2 be Element of NAT;
    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) = F(n,(fib1.n));
    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) = F(n,(fib2.n));
    fib1 = fib2 from NAT_1:sch 16(A3,A4,A6,A7);
    hence thesis by A2,A5;
  end;
end;

theorem
  Fib(0) = 0 & Fib(1) = 1 &
  for n being Nat holds Fib((n+1)+1) = Fib(n) + Fib(n+1)
proof
  deffunc F(set,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) = F(n,(fib.n)) from NAT_1:sch 12;
  thus Fib (0) = [0, 1]`1 by A1,A2,Def1
    .= 0 by MCART_1:7;
  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;
  let n be Nat;
  reconsider 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 thesis;
end;

:: Fusc function auxiliaries

theorem
  for i being Integer holds i div 1 = i
proof
  let i be Integer;
  thus i div 1 = [\ i / 1 /] by INT_1:def 9
    .= i by INT_1:25;
end;

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
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;

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;
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 < 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;
  i div 2<=i/2 by A1,INT_1:def 6;
  then A <= (i/2)*2 by XREAL_1:64;
  then -i <= -A by XREAL_1:24;
  then i+-i <= i+-A by XREAL_1:6;
  then 0 <= i-A;
  then 0 <= M by INT_1:def 10;
  then reconsider M 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 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;
  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,7;
  hence thesis by INT_1:def 9;
end;

theorem Th8:
  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;
  assume a <= b;
  then a < b or a = b by XXREAL_0:1;
  hence thesis by POWER:39;
end;

theorem Th9:
  for r, s being real number st r>=s holds [\r/] >= [\s/]
proof
  let r, s be real number;
  assume
A1: 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 /];
  then [\ r /] + 1 <= [\ s /] by INT_1:7;
  then r < [\ s /] by A3,XXREAL_0:2;
  hence contradiction by A1,A2,XXREAL_0:2;
end;

theorem Th10:
  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;
  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 2*0 < 2*n by XREAL_1:68;
  then
A3: 2*n < 2 to_power k by A1,POWER:def 3;
  assume [\ l22n /] +1 = [\ l22np1 /];
  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,Th9;
  then 0 <= k by INT_1:25;
  then reconsider k 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;
  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 by NAT_D:def 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;
  2*0 < 2*n by A1,XREAL_1:68;
  then log (2,2*(2*n)) = log (2,2)+l22n by 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;
  2*0 < 2*n by A1,XREAL_1:68;
  then l22n <= l22np1 by 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

definition
  let f be Function of NAT, NAT*, n be Element of NAT;
  redefine func f.n -> FinSequence of NAT;
  coherence
  proof
    f.n is Element of NAT*;
    hence thesis;
  end;
end;

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 Element of NAT for x be Element of NAT* ex y be Element of NAT*
st P[n,x,y]
proof
  let n be Element of 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;
    then n+2 = 2*k+0;
    hence y = x^<*x/.k*> by A1,NAT_D:def 1,def 2;
  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;

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 P[n,fusc.n,fusc.(n+1)] from RECDEF_1
:sch 2(Lm1);

Lm5: for n being Nat holds P[n,fusc.n qua Element of NAT*,fusc.(n+1)]
proof
  let n be Nat;
  n in NAT by ORDINAL1:def 12;
  hence thesis by Lm4;
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 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 qua Element of NAT*)^ <*(fusc.n qua Element of NAT*)
/.k*>) & for k being Nat st n+2 = 2*k+1 holds fusc.(n+1) = (fusc.n qua Element
of NAT*)^<*((fusc.n qua Element of NAT*)/.k)+ ((fusc.n qua Element of NAT*)/.(k
  +1))*>;
  consistency;
  existence
  proof
    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 qua Element of NAT*)/.n) as Element of NAT;
    reconsider l9 = l as Element of NAT by ORDINAL1:def 12;
    take IT, l9;
    thus thesis by A1,Lm3,Lm5;
  end;
  uniqueness
  proof
    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 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 qua Element of NAT*)^ <*(fusc1.n qua Element of NAT*)/.k*>) &
for k being Nat st n+2 = 2*k+1 holds fusc1.(n+1) = (fusc1.n qua Element of NAT*
)^<*((fusc1.n qua Element of NAT*)/.k)+ ((fusc1.n qua Element of NAT*)/.(k+1))
    *>;
A5: fusc1.0 = single1 by A3;
A6: for n being Nat holds Q[n,fusc1.n qua Element of NAT*,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 qua Element of NAT*)^ <*(fusc2.n qua Element of NAT*)/.k*>) &
for k being Nat st n+2 = 2*k+1 holds fusc2.(n+1) = (fusc2.n qua Element of NAT*
)^<*((fusc2.n qua Element of NAT*)/.k)+ ((fusc2.n qua Element of NAT*)/.(k+1))
    *>;
A10: for n being Nat holds Q[n,fusc2.n qua Element of NAT*,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
  thus
A1: Fusc 0 = 0 by Def2;
  0+1 = 1 & 1 = (<*1*>)/.1 by FINSEQ_4:16;
  hence Fusc 1 = 1 by Def2,Lm3,Lm5;
  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[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 be Element of NAT st P[n] holds P[n+1]
    proof
      let n be Element of 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 Lm5;
        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,Lm5;
      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 Lm5;
        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,Lm5;
      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,Lm5;
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,Lm5;
    end;
A17: for n being Element of NAT holds P[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;
    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;
  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
A2: 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 A2,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
A2: 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 A2,Th15
    .= (A+B)*Fusc n + B*Fusc (n+1);
end;