pre_ff.miz



    begin

    registration

      let n,k be Nat;

      reduce ( In ( [n, k], [: NAT , NAT :])) to [n, k];

      reducibility

      proof

        n in NAT & k in NAT by ORDINAL1:def 12;

        then [n, k] in [: NAT , NAT :] by ZFMISC_1: 87;

        hence thesis by SUBSET_1:def 8;

      end;

    end

    deffunc F( set, Element of [: NAT , NAT :]) = ( In ( [($2 `2 ), (($2 `1 ) + ($2 `2 ))], [: NAT , NAT :]));

    definition

      :: PRE_FF:def1

      func Fib -> sequence of [: NAT , NAT :] means

      : Def1: (it . 0 ) = [ 0 , 1] & for n be Nat holds (it . (n + 1)) = [((it . n) `2 ), (((it . n) `1 ) + ((it . n) `2 ))];

      existence

      proof

        consider fib be sequence of [: NAT , NAT :] such that

         A1: (fib . 0 ) = [ 0 , 1] & for n be Nat holds (fib . (n + 1)) = F(n,.) from NAT_1:sch 12;

        take fib;

        thus (fib . 0 ) = [ 0 , 1] by A1;

        let n be Nat;

        (fib . (n + 1)) = F(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 be Nat holds (fib1 . (n + 1)) = [((fib1 . n) `2 ), (((fib1 . n) `1 ) + ((fib1 . n) `2 ))];

        

         A5: for n be Nat holds (fib1 . (n + 1)) = F(n,.) by A4;

        assume that

         A7: (fib2 . 0 ) = [ 0 , 1] and

         A8: for n be Nat holds (fib2 . (n + 1)) = [((fib2 . n) `2 ), (((fib2 . n) `1 ) + ((fib2 . n) `2 ))];

        

         A9: for n be Nat holds (fib2 . (n + 1)) = F(n,.) by A8;

        thus fib1 = fib2 from NAT_1:sch 16( A3, A5, A7, A9);

      end;

    end

    definition

      let n be Nat;

      :: PRE_FF:def2

      func Fib n -> Element of NAT equals (( Fib . n) `1 );

      coherence ;

    end

    theorem :: PRE_FF:1

    ( Fib 0 ) = 0 & ( Fib 1) = 1 & for n be Nat holds ( Fib ((n + 1) + 1)) = (( Fib n) + ( Fib (n + 1)))

    proof

      

       A1: ( Fib . 0 ) = [ 0 , 1] by Def1;

      

       A3: for n be Nat holds ( Fib . (n + 1)) = [(( Fib . n) `2 ), ((( Fib . n) `1 ) + (( Fib . n) `2 ))]

      proof

        let n be Nat;

        set i = (( Fib . n) `2 ), j = ((( Fib . n) `1 ) + (( Fib . n) `2 ));

        

        thus ( Fib . (n + 1)) = F(n,.) by Def1

        .= [i, j];

      end;

      

      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;

    theorem :: PRE_FF:2

    for i be 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 :: PRE_FF:3

    for i,j be 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 :: PRE_FF:4

    for i,j be 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 :: PRE_FF:5

    for i,j,k be 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 :: PRE_FF:6

    for i be 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 be Nat : k < 2 } by A2;

      then M in 2 by AXIOMS: 4;

      hence thesis by CARD_1: 50, TARSKI:def 2;

    end;

    theorem :: PRE_FF:7

    for i be 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, INT_1: 7;

      hence thesis by INT_1:def 9;

    end;

    theorem :: PRE_FF:8

    

     Th8: for a,b,c be 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;

      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 :: PRE_FF:9

    

     Th9: for r,s be Real st r >= s holds [\r/] >= [\s/]

    proof

      let r,s be Real;

      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 :: PRE_FF:10

    

     Th10: for a,b,c be 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 :: PRE_FF:11

    

     Th11: for n be 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, Th9;

      then 0 <= k by INT_1: 25;

      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 be Nat st k = (m + 1);

        then

        consider m be 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 :: PRE_FF:12

    

     Th12: for n be 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 :: PRE_FF:13

    

     Th13: for n be 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 :: PRE_FF:14

    for n be 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;

    defpred P[ Nat, FinSequence of NAT , set] means (for k be Nat st ($1 + 2) = (2 * k) holds $3 = ($2 ^ <*($2 /. k)*>)) & (for k be Nat st ($1 + 2) = ((2 * k) + 1) holds $3 = ($2 ^ <*(($2 /. k) + ($2 /. (k + 1)))*>));

    

     Lm1: for n be Nat holds for x be Element of ( NAT * ) holds 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 be 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, NAT_D: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 be Element of NAT st ($1 + 2) = (2 * k) holds $3 = ($2 ^ <*($2 /. k)*>)) & (for k be 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 be Element of NAT st (n + 2) = (2 * k) holds y1 = (x ^ <*(x /. k)*>)) & for k be 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 be Element of NAT st (n + 2) = (2 * k) holds y2 = (x ^ <*(x /. k)*>)) & for k be 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;

      :: PRE_FF:def3

      func Fusc n -> Element of NAT means

      : Def2: it = 0 if n = 0

      otherwise ex l be Element of NAT , fusc be sequence of ( NAT * ) st (l + 1) = n & it = ((fusc . l) /. n) & (fusc . 0 ) = <*1*> & for n be Nat holds (for k be Nat st (n + 2) = (2 * k) holds (fusc . (n + 1)) = ((fusc . n) ^ <*((fusc . n) /. k)*>)) & for k be 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 be sequence of ( NAT * ) such that

         Lm3: (fusc . 0 ) = single1 and

         Lm4: for n be Nat holds P[n, (fusc . n), (fusc . (n + 1))] from RECDEF_1:sch 2( Lm1);

        thus n = 0 implies ex k be Element of NAT st k = 0 ;

        assume n <> 0 ;

        then

        consider l be 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;

        consider fusc be sequence of ( NAT * ) such that (fusc . 0 ) = single1 and for n be Nat holds P[n, (fusc . n), (fusc . (n + 1))] from RECDEF_1:sch 2( Lm1);

        let n1,n2 be Element of NAT ;

        thus n = 0 & n1 = 0 & n2 = 0 implies n1 = n2;

        assume n <> 0 ;

        given l1 be Element of NAT , fusc1 be sequence of ( NAT * ) such that

         A2: (l1 + 1) = n & n1 = ((fusc1 . l1) /. n) and

         A3: (fusc1 . 0 ) = <*1*> and

         A4: for n be Nat holds (for k be Nat st (n + 2) = (2 * k) holds (fusc1 . (n + 1)) = ((fusc1 . n) ^ <*((fusc1 . n) /. k)*>)) & for k be 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 be Nat holds Q[n, (fusc1 . n), (fusc1 . (n + 1))] by A4;

        given l2 be Element of NAT , fusc2 be sequence of ( NAT * ) such that

         A7: (l2 + 1) = n & n2 = ((fusc2 . l2) /. n) and

         A8: (fusc2 . 0 ) = <*1*> and

         A9: for n be Nat holds (for k be Nat st (n + 2) = (2 * k) holds (fusc2 . (n + 1)) = ((fusc2 . n) ^ <*((fusc2 . n) /. k)*>)) & for k be Nat st (n + 2) = ((2 * k) + 1) holds (fusc2 . (n + 1)) = ((fusc2 . n) ^ <*(((fusc2 . n) /. k) + ((fusc2 . n) /. (k + 1)))*>);

        

         A10: for n be 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 :: PRE_FF:15

    

     Th15: ( Fusc 0 ) = 0 & ( Fusc 1) = 1 & for n be 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 be sequence of ( NAT * ) such that

       Lm3: (fusc . 0 ) = single1 and

       Lm4: for n be 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 be Nat such that

         A2: n = (l + 1) by NAT_1: 6;

        defpred P[ Nat] means ( len (fusc . $1)) = ($1 + 1) & for k be 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 be 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 be 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;

    theorem :: PRE_FF:16

    for n be 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 :: PRE_FF:17

    for n be 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 :: PRE_FF:18

    for A,B be Nat holds B = ((A * ( Fusc 0 )) + (B * ( Fusc 1))) by Th15;

    theorem :: PRE_FF:19

    for n,A,B,N be 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 :: PRE_FF:20

    for n,A,B,N be 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;