ntalgo_2.miz



    begin

    definition

      let F be Element of ( BOOLEAN * );

      let x be object;

      :: original: .

      redefine

      func F . x -> Nat ;

      correctness ;

    end

    definition

      let n,m be Nat;

      :: original: to_power

      redefine

      func n to_power m -> Nat ;

      coherence ;

    end

    definition

      let a,b be object, c be Nat;

      :: NTALGO_2:def1

      func BinBranch (a,b,c) equals

      : defBB: a if c = 0

      otherwise b;

      correctness ;

    end

    definition

      let a,b,c be Nat;

      :: original: BinBranch

      redefine

      func BinBranch (a,b,c) -> Nat ;

      coherence by defBB;

    end

    

     Lm1: for a,n,m be Element of NAT holds ex A,B be sequence of NAT st (A . 0 ) = (a mod m) & (B . 0 ) = 1 & for i be Nat holds (A . (i + 1)) = (((A . i) * (A . i)) mod m) & (B . (i + 1)) = ( BinBranch ((B . i),(((B . i) * (A . i)) mod m),(( Nat2BL . n) . (i + 1))))

    proof

      let a,n,m be Element of NAT ;

      defpred P1[ Nat, Nat, Nat, Nat, Nat] means $4 = (($2 * $2) mod m) & $5 = ( BinBranch ($3,(($3 * $2) mod m),(( Nat2BL . n) . ($1 + 1))));

      

       A1: for i be Nat, x,y be Element of NAT holds ex x1,y1 be Element of NAT st P1[i, x, y, x1, y1]

      proof

        let i be Nat, x,y be Element of NAT ;

        set x1 = ((x * x) mod m);

        set y1 = ( BinBranch (y,((y * x) mod m),(( Nat2BL . n) . (i + 1))));

        x1 is Element of NAT & y1 is Element of NAT by ORDINAL1:def 12;

        hence thesis;

      end;

      consider A be sequence of NAT , B be sequence of NAT such that

       A2: (A . 0 ) = (a mod m) & (B . 0 ) = 1 & for n be Nat holds P1[n, (A . n), (B . n), (A . (n + 1)), (B . (n + 1))] from RECDEF_2:sch 3( A1);

      take A, B;

      thus thesis by A2;

    end;

    

     Lm2: for a,n,m be Element of NAT , A1,B1,A2,B2 be sequence of NAT st ((A1 . 0 ) = a & (B1 . 0 ) = 1 & for i be Nat holds (A1 . (i + 1)) = (((A1 . i) * (A1 . i)) mod m) & (B1 . (i + 1)) = ( BinBranch ((B1 . i),(((B1 . i) * (A1 . i)) mod m),(( Nat2BL . n) . (i + 1))))) & ((A2 . 0 ) = a & (B2 . 0 ) = 1 & for i be Nat holds (A2 . (i + 1)) = (((A2 . i) * (A2 . i)) mod m) & (B2 . (i + 1)) = ( BinBranch ((B2 . i),(((B2 . i) * (A2 . i)) mod m),(( Nat2BL . n) . (i + 1))))) holds A1 = A2 & B1 = B2

    proof

      let a,n,m be Element of NAT ;

      let A1,B1,A2,B2 be sequence of NAT ;

      assume

       A1: (A1 . 0 ) = a & (B1 . 0 ) = 1 & for i be Nat holds (A1 . (i + 1)) = (((A1 . i) * (A1 . i)) mod m) & (B1 . (i + 1)) = ( BinBranch ((B1 . i),(((B1 . i) * (A1 . i)) mod m),(( Nat2BL . n) . (i + 1))));

      assume

       A2: (A2 . 0 ) = a & (B2 . 0 ) = 1 & for i be Nat holds (A2 . (i + 1)) = (((A2 . i) * (A2 . i)) mod m) & (B2 . (i + 1)) = ( BinBranch ((B2 . i),(((B2 . i) * (A2 . i)) mod m),(( Nat2BL . n) . (i + 1))));

      defpred P[ Nat] means (A1 . $1) = (A2 . $1) & (B1 . $1) = (B2 . $1);

      

       A3: P[ 0 ] by A1, A2;

      

       A4: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A5: P[i];

        

         A6: (A1 . (i + 1)) = (((A1 . i) * (A1 . i)) mod m) by A1

        .= (A2 . (i + 1)) by A2, A5;

        (B1 . (i + 1)) = ( BinBranch ((B1 . i),(((B1 . i) * (A1 . i)) mod m),(( Nat2BL . n) . (i + 1)))) by A1

        .= (B2 . (i + 1)) by A2, A5;

        hence P[(i + 1)] by A6;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A3, A4);

      hence thesis;

    end;

    definition

      let a,n,m be Element of NAT ;

      :: NTALGO_2:def2

      func ALGO_BPOW (a,n,m) -> Element of NAT means

      : Def1: ex A,B be sequence of NAT st it = (B . ( LenBSeq n)) & (A . 0 ) = (a mod m) & (B . 0 ) = 1 & (for i be Nat holds (A . (i + 1)) = (((A . i) * (A . i)) mod m) & (B . (i + 1)) = ( BinBranch ((B . i),(((B . i) * (A . i)) mod m),(( Nat2BL . n) . (i + 1)))));

      existence

      proof

        consider A,B be sequence of NAT such that

         A1: (A . 0 ) = (a mod m) & (B . 0 ) = 1 & for i be Nat holds (A . (i + 1)) = (((A . i) * (A . i)) mod m) & (B . (i + 1)) = ( BinBranch ((B . i),(((B . i) * (A . i)) mod m),(( Nat2BL . n) . (i + 1)))) by Lm1;

        set K = (B . ( LenBSeq n));

        K is Element of NAT ;

        hence thesis by A1;

      end;

      uniqueness by Lm2;

    end

    theorem :: NTALGO_2:1

    

     CBPOW1: for a,m,i be Nat, A be sequence of NAT st (A . 0 ) = (a mod m) & (for j be Nat holds (A . (j + 1)) = (((A . j) * (A . j)) mod m)) holds (A . i) = ((a to_power (2 to_power i)) mod m)

    proof

      let a,m,i be Nat, A be sequence of NAT ;

      assume

       AS0: (A . 0 ) = (a mod m) & (for i be Nat holds (A . (i + 1)) = (((A . i) * (A . i)) mod m));

      defpred P[ Nat] means (A . $1) = ((a to_power (2 to_power $1)) mod m);

      ((a to_power (2 to_power 0 )) mod m) = ((a to_power 1) mod m) by POWER: 24

      .= (a mod m);

      then

       L1: P[ 0 ] by AS0;

      

       L2: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume P[i];

        

        then (((A . i) * (A . i)) mod m) = ((a |^ ((2 to_power 1) * (2 to_power i))) mod m) by NAT_4: 11

        .= ((a to_power (2 to_power (i + 1))) mod m) by POWER: 27;

        hence thesis by AS0;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( L1, L2);

      hence thesis;

    end;

    

     CBPOW2: for a,m,i,n be Nat, A be sequence of NAT st a <> 0 & (A . 0 ) = (a mod m) & (for j be Nat holds (A . (j + 1)) = (((A . j) * (A . j)) mod m)) holds ((((a to_power n) mod m) * (A . i)) mod m) = ((a to_power (n + (2 to_power i))) mod m)

    proof

      let a,m,i,n be Nat, A be sequence of NAT ;

      assume

       AS0: a <> 0 & (A . 0 ) = (a mod m) & (for i be Nat holds (A . (i + 1)) = (((A . i) * (A . i)) mod m));

      then (A . i) = ((a to_power (2 to_power i)) mod m) by CBPOW1;

      

      then ((((a to_power n) mod m) * (A . i)) mod m) = (((a to_power n) * (a to_power (2 to_power i))) mod m) by NAT_D: 67

      .= ((a to_power (n + (2 to_power i))) mod m) by POWER: 27, AS0;

      hence thesis;

    end;

    theorem :: NTALGO_2:2

    ( LenBSeq 0 ) = 1 by BINARI_6:def 1;

    theorem :: NTALGO_2:3

    

     EXL1: ( LenBSeq 1) = 1

    proof

      

       X1: (2 to_power 0 ) <= 1 by POWER: 24;

      1 < (2 to_power ( 0 + 1));

      hence thesis by BINARI_6:def 1, X1;

    end;

    theorem :: NTALGO_2:4

    for x be Nat st 2 <= x holds 1 < ( LenBSeq x)

    proof

      let x be Nat;

      assume

       AS0: 2 <= x;

      then

      consider n be Nat such that

       P3: (2 to_power n) <= x & x < (2 to_power (n + 1)) & ( LenBSeq x) = (n + 1) by BINARI_6:def 1;

      n <> 0 by AS0, P3;

      then ( 0 + 1) < (n + 1) by XREAL_1: 8;

      hence thesis by P3;

    end;

    theorem :: NTALGO_2:5

    

     EXL2: for n be Nat st 0 < n holds ( LenBSeq n) = ( [\( log (2,n))/] + 1)

    proof

      let n be Nat;

      assume 0 < n;

      then

      consider x be Nat such that

       LCX: (2 to_power x) <= n & n < (2 to_power (x + 1)) & ( LenBSeq n) = (x + 1) by BINARI_6:def 1;

      ( log (2,(2 to_power x))) = x by POWER:def 3;

      then

       LT1: x <= ( log (2,n)) by LCX, ASYMPT_2: 7;

      ( log (2,(2 to_power (x + 1)))) = (x + 1) by POWER:def 3;

      then ( log (2,n)) < (x + 1) by LCX, POWER: 57;

      then (( log (2,n)) - 1) < ((x + 1) - 1) by XREAL_1: 14;

      hence thesis by LCX, LT1, INT_1:def 6;

    end;

    theorem :: NTALGO_2:6

    

     zerobs: ( Nat2BL . 0 ) = <* 0 *>

    proof

      ( LenBSeq 0 ) = 1 by BINARI_6:def 1;

      

      then ( Nat2BL . 0 ) = (1 -BinarySequence 0 ) by BINARI_6:def 2

      .= <* 0 *> by BINARI_3: 25, BINARI_6: 4;

      hence thesis;

    end;

    theorem :: NTALGO_2:7

    ( Nat2BL . 1) = <*1*>

    proof

      

       X1: 1 = (2 to_power 0 ) by POWER: 24;

      ( Nat2BL . 1) = (1 -BinarySequence 1) by BINARI_6:def 2, EXL1

      .= (( 0* 0 ) ^ <*1*>) by X1, BINARI_3: 28

      .= <*1*> by FINSEQ_1: 34;

      hence thesis;

    end;

    theorem :: NTALGO_2:8

    

     MMS1: for n be Element of NAT st 0 < n holds (( Nat2BL . n) . ( LenBSeq n)) = 1

    proof

      let n be Element of NAT ;

      assume

       AS: 0 < n;

      assume

       AC: (( Nat2BL . n) . ( LenBSeq n)) <> 1;

      

       L1: ( Nat2BL . n) = (( LenBSeq n) -BinarySequence n) by BINARI_6:def 2;

      reconsider x = ( Nat2BL . n) as Element of ( BOOLEAN * );

      

       LAC: not x in { y where y be Element of ( BOOLEAN * ) : (y . ( len y)) = 1 }

      proof

        assume x in { y where y be Element of ( BOOLEAN * ) : (y . ( len y)) = 1 };

        then ex y be Element of ( BOOLEAN * ) st x = y & (y . ( len y)) = 1;

        hence contradiction by AC, L1, FINSEQ_3: 153;

      end;

       0 in NAT ;

      then

       PO: 0 in ( dom Nat2BL ) by FUNCT_2:def 1;

      n in NAT ;

      then

       TLL: n in ( dom Nat2BL ) by FUNCT_2:def 1;

      then x in ( rng Nat2BL ) by FUNCT_1: 3;

      then x in { y where y be Element of ( BOOLEAN * ) : (y . ( len y)) = 1 } or x in { <* 0 *>} by BINARI_6: 11, XBOOLE_0:def 3;

      then ( Nat2BL . n) = <* 0 *> by TARSKI:def 1, LAC;

      hence contradiction by AS, TLL, PO, zerobs, BINARI_6: 12;

    end;

    theorem :: NTALGO_2:9

    ( Nat2BL . 2) = <* 0 , 1*>

    proof

      

       X1: 2 = (2 to_power 1);

      ( LenBSeq 2) = ( [\( log (2,2))/] + 1) by EXL2

      .= ( [\1/] + 1) by POWER: 52

      .= (1 + 1) by INT_1: 25;

      

      then ( Nat2BL . 2) = (2 -BinarySequence 2) by BINARI_6:def 2

      .= <* 0 , 1*> by BINARI_6: 4, X1, BINARI_3: 28;

      hence thesis;

    end;

    theorem :: NTALGO_2:10

    ( Nat2BL . 3) = <*1, 1*>

    proof

      

       X0: (2 + 1) < (2 to_power 2) by POWER: 60;

      

       X1: 2 = (2 to_power 1);

      ( log (2,3)) < ( log (2,4)) by POWER: 57;

      then ( log (2,3)) < 2 by POWER: 60, POWER:def 3;

      then

       X4: (( log (2,3)) - 1) < (2 - 1) by XREAL_1: 14;

      ( log (2,2)) < ( log (2,3)) by POWER: 57;

      then 1 < ( log (2,3)) by POWER: 52;

      then

       X5: [\( log (2,3))/] = 1 by INT_1:def 6, X4;

      ( LenBSeq 3) = ( [\( log (2,3))/] + 1) by EXL2

      .= 2 by X5;

      

      then

       X2: ( Nat2BL . 3) = (2 -BinarySequence 3) by BINARI_6:def 2

      .= ((2 -BinarySequence 2) + ( Bin1 2)) by BINARI_3: 33, X0;

      

       X3: (2 -BinarySequence 2) = ( <* FALSE *> ^ <* TRUE *>) by XBOOLEAN:def 1, XBOOLEAN:def 2, BINARI_6: 4, X1, BINARI_3: 28;

      

       X5: ( Bin1 2) = ( <* TRUE *> ^ <* FALSE *>) by BINARI_3: 10, BINARI_2: 7;

      set z1 = <* FALSE *>;

      set z2 = <* TRUE *>;

      

       X7: (( carry (z1,z2)) /. 1) = FALSE by BINARITH:def 2;

      

       X70: (z1 /. 1) = FALSE by FINSEQ_4: 16;

      

       X71: (z2 /. 1) = TRUE by FINSEQ_4: 16;

      

      then

       X6: ( add_ovfl ( <* FALSE *>, <* TRUE *>)) = (( FALSE 'or' ( FALSE '&' FALSE )) 'or' ( TRUE '&' FALSE )) by MARGREL1: 13, X7, X70

      .= FALSE by MARGREL1: 13;

      ((2 -BinarySequence 2) + ( Bin1 2)) = (( <* FALSE *> + <* TRUE *>) ^ <*(( TRUE 'xor' FALSE ) 'xor' ( add_ovfl ( <* FALSE *>, <* TRUE *>)))*>) by BINARITH: 19, X3, X5

      .= ( <* TRUE *> ^ <*( TRUE 'xor' ( add_ovfl ( <* FALSE *>, <* TRUE *>)))*>) by BINARITH: 8, BINARI_3: 17

      .= ( <* TRUE *> ^ <* TRUE *>) by X6, BINARITH: 8;

      hence thesis by X2, XBOOLEAN:def 2;

    end;

    theorem :: NTALGO_2:11

    ( Nat2BL . 4) = <* 0 , 0 , 1*>

    proof

      ( LenBSeq 4) = ( [\( log (2,4))/] + 1) by EXL2

      .= ( [\2/] + 1) by POWER:def 3, POWER: 60

      .= (2 + 1) by INT_1: 25

      .= 3;

      

      then ( Nat2BL . 4) = (3 -BinarySequence 4) by BINARI_6:def 2

      .= (( 0* 2) ^ <*1*>) by BINARI_3: 28, POWER: 60

      .= <* 0 , 0 , 1*> by BINARI_6: 5, BINARI_6: 4;

      hence thesis;

    end;

    theorem :: NTALGO_2:12

    for n be Nat holds ( Nat2BL . (2 |^ n)) = (( 0* n) ^ <*1*>)

    proof

      let n be Nat;

      

       X1: (2 |^ n) = (2 to_power n);

      

       X3: ( LenBSeq (2 |^ n)) = ( [\( log (2,(2 |^ n)))/] + 1) by EXL2

      .= ( [\n/] + 1) by X1, POWER:def 3

      .= (n + 1) by INT_1: 25;

      (2 |^ n) is Element of NAT by ORDINAL1:def 12;

      

      then ( Nat2BL . (2 |^ n)) = ((n + 1) -BinarySequence (2 |^ n)) by X3, BINARI_6:def 2

      .= (( 0* n) ^ <*1*>) by BINARI_3: 28, X1;

      hence thesis;

    end;

    theorem :: NTALGO_2:13

    for m be Element of NAT holds ( ALGO_BPOW ( 0 , 0 ,m)) = 1

    proof

      let m be Element of NAT ;

      consider A,B be sequence of NAT such that

       ASC: ( ALGO_BPOW ( 0 , 0 ,m)) = (B . ( LenBSeq 0 )) & (A . 0 ) = ( 0 mod m) & (B . 0 ) = 1 & (for i be Nat holds (A . (i + 1)) = (((A . i) * (A . i)) mod m) & (B . (i + 1)) = ( BinBranch ((B . i),(((B . i) * (A . i)) mod m),(( Nat2BL . 0 ) . (i + 1))))) by Def1;

      ( ALGO_BPOW ( 0 , 0 ,m)) = (B . 1) by ASC, BINARI_6:def 1

      .= ( BinBranch ((B . 0 ),(((B . 0 ) * (A . 0 )) mod m),(( Nat2BL . 0 ) . ( 0 + 1)))) by ASC

      .= 1 by ASC, defBB, zerobs;

      hence thesis;

    end;

    theorem :: NTALGO_2:14

    for n,m be Element of NAT st 0 < n holds ( ALGO_BPOW ( 0 ,n,m)) = 0

    proof

      let n,m be Element of NAT ;

      assume

       AS: 0 < n;

      consider A,B be sequence of NAT such that

       ASC: ( ALGO_BPOW ( 0 ,n,m)) = (B . ( LenBSeq n)) & (A . 0 ) = ( 0 mod m) & (B . 0 ) = 1 & (for i be Nat holds (A . (i + 1)) = (((A . i) * (A . i)) mod m) & (B . (i + 1)) = ( BinBranch ((B . i),(((B . i) * (A . i)) mod m),(( Nat2BL . n) . (i + 1))))) by Def1;

      (( LenBSeq n) - 1) in NAT by INT_1: 5, NAT_1: 14;

      then

      reconsider fs = (( LenBSeq n) - 1) as Nat;

      

       QW: (A . fs) = (( 0 to_power (2 to_power fs)) mod m) by CBPOW1, ASC

      .= ( 0 mod m) by POWER: 42;

      ( ALGO_BPOW ( 0 ,n,m)) = ( BinBranch ((B . fs),(((B . fs) * (A . fs)) mod m),(( Nat2BL . n) . (fs + 1)))) by ASC

      .= ( BinBranch ((B . fs),(((B . fs) * (A . fs)) mod m),1)) by MMS1, AS

      .= 0 by QW, defBB;

      hence thesis;

    end;

    theorem :: NTALGO_2:15

    for a,n,m be Element of NAT st 0 < n & m <= 1 holds ( ALGO_BPOW (a,n,m)) = 0

    proof

      let a,n,m be Element of NAT ;

      assume

       AS: 0 < n & m <= 1;

      consider A,B be sequence of NAT such that

       ASC: ( ALGO_BPOW (a,n,m)) = (B . ( LenBSeq n)) & (A . 0 ) = (a mod m) & (B . 0 ) = 1 & (for i be Nat holds (A . (i + 1)) = (((A . i) * (A . i)) mod m) & (B . (i + 1)) = ( BinBranch ((B . i),(((B . i) * (A . i)) mod m),(( Nat2BL . n) . (i + 1))))) by Def1;

      (( LenBSeq n) - 1) in NAT by INT_1: 5, NAT_1: 14;

      then

      reconsider fs = (( LenBSeq n) - 1) as Nat;

      m = 0 or m = 1 by NAT_1: 25, AS;

      then

       LZEROM: (((B . fs) * (A . fs)) mod m) = 0 by RADIX_2: 1;

      ( ALGO_BPOW (a,n,m)) = ( BinBranch ((B . fs),(((B . fs) * (A . fs)) mod m),(( Nat2BL . n) . (fs + 1)))) by ASC

      .= ( BinBranch ((B . fs),(((B . fs) * (A . fs)) mod m),1)) by MMS1, AS

      .= 0 by LZEROM, defBB;

      hence thesis;

    end;

    theorem :: NTALGO_2:16

    for a,n,m be Element of NAT st a <> 0 & 1 < m holds ( ALGO_BPOW (a,n,m)) = ((a to_power n) mod m)

    proof

      let a,n,m be Element of NAT ;

      assume

       AS: a <> 0 & 1 < m;

      consider A,B be sequence of NAT such that

       ASC: ( ALGO_BPOW (a,n,m)) = (B . ( LenBSeq n)) & (A . 0 ) = (a mod m) & (B . 0 ) = 1 & (for i be Nat holds (A . (i + 1)) = (((A . i) * (A . i)) mod m) & (B . (i + 1)) = ( BinBranch ((B . i),(((B . i) * (A . i)) mod m),(( Nat2BL . n) . (i + 1))))) by Def1;

      set NBS = ( Nat2BL . n);

      NBS = (( LenBSeq n) -BinarySequence n) by BINARI_6:def 2;

      then

      reconsider NBS as Tuple of ( LenBSeq n), BOOLEAN ;

      defpred P[ Nat] means $1 < ( LenBSeq n) implies (ex SUBBS be Tuple of ($1 + 1), BOOLEAN st SUBBS = (( Nat2BL . n) | ($1 + 1)) & (B . ($1 + 1)) = ((a to_power ( Absval SUBBS)) mod m));

      

       LC1: P[ 0 ]

      proof

        (NBS | ( 0 + 1)) = <*(NBS . 1)*> by FINSEQ_5: 20;

        reconsider NBS0 = (NBS | ( 0 + 1)) as Tuple of 1, BOOLEAN ;

        

         PCJJ: (B . ( 0 + 1)) = ( BinBranch ((B . 0 ),(((B . 0 ) * (A . 0 )) mod m),(( Nat2BL . n) . ( 0 + 1)))) by ASC;

        then

         PCC0: (B . 1) = ( BinBranch (1,(a mod m),(( Nat2BL . n) . 1))) by EULER_2: 5, ASC;

        per cases by BINARITH: 14;

          suppose

           LCT: NBS0 = <* TRUE *>;

          then

           LCT1: ( Absval NBS0) = 1 by BINARITH: 16;

          ( <*(NBS . 1)*> . 1) = ( <* TRUE *> . 1) by FINSEQ_5: 20, LCT;

          then (B . 1) = ((a to_power 1) mod m) by defBB, PCC0, XBOOLEAN:def 2;

          hence thesis by LCT1;

        end;

          suppose

           LCF: NBS0 = <* FALSE *>;

          then

           LCF1: ( Absval NBS0) = 0 by BINARITH: 15;

          ( <*(NBS . 1)*> . 1) = ( <* FALSE *> . 1) by FINSEQ_5: 20, LCF;

          

          then (B . 1) = 1 by defBB, ASC, PCJJ, XBOOLEAN:def 1

          .= (1 mod m) by NAT_D: 14, AS

          .= ((a to_power 0 ) mod m) by POWER: 24;

          hence thesis by LCF1;

        end;

      end;

      

       LC2: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         ASPi: P[i];

        assume

         I1: (i + 1) < ( LenBSeq n);

        i < ( LenBSeq n)

        proof

          assume

           COV: i >= ( LenBSeq n);

          ((i + 1) - 1) < (( LenBSeq n) - 0 ) by I1, XREAL_1: 14;

          hence contradiction by COV;

        end;

        then

        consider SUBBS be Tuple of (i + 1), BOOLEAN such that

         CLa: SUBBS = (( Nat2BL . n) | (i + 1)) & (B . (i + 1)) = ((a to_power ( Absval SUBBS)) mod m) by ASPi;

        set j = (i + 1);

        thus ex SUBBS1 be Tuple of (j + 1), BOOLEAN st SUBBS1 = (( Nat2BL . n) | (j + 1)) & (B . (j + 1)) = ((a to_power ( Absval SUBBS1)) mod m)

        proof

          

           LINT: (j + 1) <= ( LenBSeq n) by INT_1: 7, I1;

          1 <= (j + 1) by NAT_1: 11;

          then (j + 1) in ( Seg ( LenBSeq n)) by LINT;

          then

           CHO: (j + 1) in ( dom NBS) by FINSEQ_1: 89;

          set SUBBS1 = (( Nat2BL . n) | (j + 1));

          

           Lhyo: (j + 1) <= ( len NBS) by FINSEQ_3: 153, LINT;

          

           Sho: SUBBS1 is Element of ( BOOLEAN * ) by FINSEQ_1:def 11;

          ( len SUBBS1) = ( min ((j + 1),( len NBS))) by FINSEQ_2: 21;

          then ( len SUBBS1) = (j + 1) by Lhyo, XXREAL_0:def 9;

          then SUBBS1 in ((j + 1) -tuples_on BOOLEAN ) by Sho;

          then

          reconsider SUBBS1 as Tuple of (j + 1), BOOLEAN ;

          set BC = ( IFEQ ((NBS . (j + 1)), FALSE , 0 ,(2 to_power j)));

          

           CCL2: SUBBS1 = (SUBBS ^ <*(NBS . (j + 1))*>) by FINSEQ_5: 10, CLa, CHO;

          

           PO: (NBS . (j + 1)) is Element of BOOLEAN by FINSEQ_1: 84, CHO;

          reconsider X = (NBS . (j + 1)) as Nat;

          

           ZZ: ( Absval SUBBS1) = (( Absval SUBBS) + BC) by BINARITH: 20, CCL2, PO;

          

           LMT1: (B . (j + 1)) = ( BinBranch ((B . j),(((B . j) * (A . j)) mod m),X)) by ASC;

          take SUBBS1;

          thus SUBBS1 = (( Nat2BL . n) | (j + 1));

          thus (B . (j + 1)) = ((a to_power ( Absval SUBBS1)) mod m)

          proof

            per cases ;

              suppose

               LPP: X = 0 ;

              then BC = 0 by FUNCOP_1:def 8, XBOOLEAN:def 1;

              hence thesis by ZZ, CLa, LMT1, defBB, LPP;

            end;

              suppose

               LPP1: X <> 0 ;

              

              then (B . (j + 1)) = (((B . j) * (A . j)) mod m) by LMT1, defBB

              .= ((a to_power (( Absval SUBBS) + (2 to_power j))) mod m) by CBPOW2, ASC, AS, CLa;

              hence thesis by FUNCOP_1:def 8, XBOOLEAN:def 1, LPP1, ZZ;

            end;

          end;

        end;

      end;

      

       LC3: for i be Nat holds P[i] from NAT_1:sch 2( LC1, LC2);

      (( LenBSeq n) - 1) in NAT by INT_1: 5, NAT_1: 14;

      then

      reconsider fs = (( LenBSeq n) - 1) as Nat;

      consider FSBS be Tuple of (fs + 1), BOOLEAN such that

       Lcfs: FSBS = (( Nat2BL . n) | (fs + 1)) & (B . (fs + 1)) = ((a to_power ( Absval FSBS)) mod m) by LC3, XREAL_1: 44;

      reconsider FSBS as Tuple of ( LenBSeq n), BOOLEAN ;

      ( dom NBS) = ( Seg ( LenBSeq n)) by FINSEQ_1: 89;

      hence thesis by ASC, BINARI_6: 10, Lcfs;

    end;

    begin

    theorem :: NTALGO_2:17

    

     LFIB5: ( Fib 5) = 5

    proof

      ( Fib 5) = ( Fib ((3 + 1) + 1))

      .= (( Fib 3) + ( Fib (3 + 1))) by PRE_FF: 1

      .= 5 by FIB_NUM2: 22, FIB_NUM2: 23;

      hence thesis;

    end;

    theorem :: NTALGO_2:18

    

     THTU: 1 < tau

    proof

      ( tau - 1) = ( - tau_bar );

      then ( 0 + 1) < (( tau - 1) + 1) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: NTALGO_2:19

    

     THTU2: tau < 2

    proof

       |. tau_bar .| = ( - tau_bar ) by ABSVALUE:def 1;

      then (( - tau_bar ) - 1) < 0 by XREAL_1: 49, FIB_NUM4: 5;

      then (( tau - 2) + 2) < ( 0 + 2) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: NTALGO_2:20

    

     THTU3: ( log ( tau ,10)) < 5

    proof

       [\((( tau to_power 5) / ( sqrt 5)) + (1 / 2))/] = 5 by FIB_NUM4: 18, LFIB5;

      then (5 - (1 / 2)) <= (((( tau to_power 5) / ( sqrt 5)) + (1 / 2)) - (1 / 2)) by XREAL_1: 9, INT_1:def 6;

      then ((9 / 2) * ( sqrt 5)) <= ((( tau to_power 5) / ( sqrt 5)) * ( sqrt 5)) by XREAL_1: 64;

      then ((9 / 2) * ( sqrt 5)) <= (( tau to_power 5) / (( sqrt 5) / ( sqrt 5))) by XCMPLX_1: 81;

      then

       WEQ: ((9 / 2) * ( sqrt 5)) <= (( tau to_power 5) / 1) by XCMPLX_1: 60;

      (((9 / 2) * ( sqrt 5)) - 10) = ((((9 * ( sqrt 5)) - 20) / 2) / (((9 * ( sqrt 5)) + 20) / ((9 * ( sqrt 5)) + 20))) by XCMPLX_1: 51

      .= ((((9 * ( sqrt 5)) - 20) / (((9 * ( sqrt 5)) + 20) / ((9 * ( sqrt 5)) + 20))) / 2) by XCMPLX_1: 48

      .= (((((9 * ( sqrt 5)) - 20) * ((9 * ( sqrt 5)) + 20)) / ((9 * ( sqrt 5)) + 20)) / 2) by XCMPLX_1: 77

      .= ((((81 * (( sqrt 5) ^2 )) - 400) / ((9 * ( sqrt 5)) + 20)) / 2)

      .= ((((81 * 5) - 400) / ((9 * ( sqrt 5)) + 20)) / 2) by SQUARE_1:def 2

      .= ((5 / ((9 * ( sqrt 5)) + 20)) / 2);

      then 10 < ((((9 / 2) * ( sqrt 5)) - 10) + 10) by XREAL_1: 29;

      then 10 < ( tau to_power 5) by WEQ, XXREAL_0: 2;

      then ( log ( tau ,10)) < ( log ( tau ,( tau to_power 5))) by POWER: 57, THTU;

      then ( log ( tau ,10)) < (5 * ( log ( tau , tau ))) by POWER: 55, THTU;

      then ( log ( tau ,10)) < (5 * 1) by POWER: 52, THTU;

      hence thesis;

    end;

    theorem :: NTALGO_2:21

    

     LTAUPOW: for n be Nat st 3 <= n holds ( tau to_power (n - 2)) < ( Fib n)

    proof

      let n be Nat;

      defpred P[ Nat] means ( tau to_power ($1 - 2)) < ( Fib $1);

      

       A1: for k be Nat st k >= 3 holds (for i be Nat st i >= 3 holds i < k implies P[i]) implies P[k]

      proof

        let k be Nat;

        assume

         A2: k >= 3;

        assume

         A3: for i be Nat st i >= 3 holds i < k implies P[i];

        

         LL: (3 <= k & k <= (3 + 1)) or 4 < k by A2;

        now

          per cases by LL, NAT_1: 9;

            case k = 3;

            ( tau to_power 1) = tau ;

            hence P[3] by FIB_NUM2: 22, THTU2;

          end;

            case k = 4;

            ( tau to_power (4 - 2)) = ( tau to_power ( 0 + 2))

            .= (( tau to_power 0 ) + ( tau to_power ( 0 + 1))) by FIB_NUM3: 9

            .= (1 + tau ) by POWER: 24;

            then ( tau to_power (4 - 2)) < (1 + 2) by THTU2, XREAL_1: 6;

            hence P[4] by FIB_NUM2: 23;

          end;

            case

             LC4A: 4 < k;

            then (k - 4) in NAT by INT_1: 5;

            then

            reconsider z = (k - 4) as Nat;

            (4 - 3) < (k - 0 ) by XREAL_1: 14, LC4A;

            then (k - 1) in NAT by INT_1: 5;

            then

            reconsider x = (k - 1) as Nat;

            (4 - 2) < (k - 0 ) by XREAL_1: 14, LC4A;

            then (k - 2) in NAT by INT_1: 5;

            then

            reconsider y = (k - 2) as Nat;

            (4 + 1) <= k by INT_1: 7, LC4A;

            then (5 - 2) <= (k - 2) & (5 - 2) <= (k - 1) by XREAL_1: 13;

            then 3 <= x & 3 <= y & x < k & y < k by XREAL_1: 44;

            then ( tau to_power (x - 2)) < ( Fib x) & ( tau to_power (y - 2)) < ( Fib y) by A3;

            then (( tau to_power z) + ( tau to_power (z + 1))) < (( Fib x) + ( Fib y)) by XREAL_1: 8;

            then ( tau to_power (z + 2)) < (( Fib x) + ( Fib y)) by FIB_NUM3: 9;

            then ( tau to_power (k - 2)) < ( Fib ((y + 1) + 1)) by PRE_FF: 1;

            hence P[k];

          end;

        end;

        hence thesis;

      end;

      for k be Nat st k >= 3 holds P[k] from NAT_1:sch 9( A1);

      hence thesis;

    end;

    theorem :: NTALGO_2:22

    for a,b be Element of INT st |.a.| > |.b.| & b > 1 holds ex A,B be sequence of NAT , C be Real_Sequence, n be Element of NAT st (A . 0 ) = |.a.| & (B . 0 ) = |.b.| & (for i be Nat holds (A . (i + 1)) = (B . i) & (B . (i + 1)) = ((A . i) mod (B . i))) & n = ( min* { i where i be Nat : (B . i) = 0 }) & (a gcd b) = (A . n) & ( Fib (n + 1)) <= |.b.| & n <= (5 * [/( log (10, |.b.|))\]) & n <= (C . |.b.|) & C is polynomially-bounded

    proof

      let a,b be Element of INT ;

      assume

       ASKARI: |.a.| > |.b.| & b > 1;

      consider A,B be sequence of NAT such that

       L1: (A . 0 ) = |.a.| & (B . 0 ) = |.b.| & (for i be Nat holds (A . (i + 1)) = (B . i) & (B . (i + 1)) = ((A . i) mod (B . i))) & ( ALGO_GCD (a,b)) = (A . ( min* { i where i be Nat : (B . i) = 0 })) by NTALGO_1:def 1;

      consider n be Element of NAT such that

       CC1: n = ( min* { i where i be Nat : (B . i) = 0 }) & ( ALGO_GCD (a,b)) = (A . n) by L1;

      

       Lm5: for a,b be Element of INT , A,B be sequence of NAT st ((A . 0 ) = |.a.| & (B . 0 ) = |.b.| & (for i be Nat holds (A . (i + 1)) = (B . i) & (B . (i + 1)) = ((A . i) mod (B . i)))) holds { i where i be Nat : (B . i) = 0 } is non empty Subset of NAT

      proof

        let a,b be Element of INT , A,B be sequence of NAT ;

        assume

         A1: (A . 0 ) = |.a.| & (B . 0 ) = |.b.| & (for i be Nat holds (A . (i + 1)) = (B . i) & (B . (i + 1)) = ((A . i) mod (B . i)));

        

         A2: for x be object st x in { i where i be Nat : (B . i) = 0 } holds x in NAT

        proof

          let x be object;

          assume x in { i where i be Nat : (B . i) = 0 };

          then ex i be Nat st x = i & (B . i) = 0 ;

          hence x in NAT by ORDINAL1:def 12;

        end;

        ex m0 be Nat st (B . m0) = 0

        proof

          assume

           A3: not ex m0 be Nat st (B . m0) = 0 ;

          

           A4: for i be Nat holds (B . (i + 1)) <= ((B . i) - 1)

          proof

            let i be Nat;

            

             A5: (B . i) <> 0 by A3;

            (B . (i + 1)) = ((A . i) mod (B . i)) by A1;

            then ((B . (i + 1)) + 1) <= (B . i) by NAT_1: 13, A5, INT_1: 58;

            then (((B . (i + 1)) + 1) - 1) <= ((B . i) - 1) by XREAL_1: 9;

            hence (B . (i + 1)) <= ((B . i) - 1);

          end;

          defpred P[ Nat] means (B . $1) <= ((B . 0 ) - $1);

          

           A6: P[ 0 ];

          

           A7: for i be Nat st P[i] holds P[(i + 1)]

          proof

            let i be Nat;

            assume

             A8: P[i];

            

             A9: (B . (i + 1)) <= ((B . i) - 1) by A4;

            ((B . i) - 1) <= (((B . 0 ) - i) - 1) by A8, XREAL_1: 9;

            hence P[(i + 1)] by A9, XXREAL_0: 2;

          end;

          

           A10: for i be Nat holds P[i] from NAT_1:sch 2( A6, A7);

          then (B . (B . 0 )) <= ((B . 0 ) - (B . 0 ));

          hence contradiction by A3, NAT_1: 14;

        end;

        then

        consider m0 be Nat such that

         A11: (B . m0) = 0 ;

        m0 in { i where i be Nat : (B . i) = 0 } by A11;

        hence thesis by A2, TARSKI:def 3;

      end;

      

       KL11: { i where i be Nat : (B . i) = 0 } is non empty Subset of NAT by L1, Lm5;

      then n in { i where i be Nat : (B . i) = 0 } by NAT_1:def 1, CC1;

      then ex i be Nat st n = i & (B . i) = 0 ;

      then

       LNNZ: n <> 0 by ASKARI, L1;

      then

       NIZ: (n - 1) is Nat by NAT_1: 20;

      

       LX1: (B . (n - 1)) <> 0

      proof

        assume (B . (n - 1)) = 0 ;

        then (n - 1) in { i where i be Nat : (B . i) = 0 } by NIZ;

        then n <= (n - 1) by CC1, NAT_1:def 1, KL11;

        then n < ((n - 1) + 1) by XREAL_1: 145;

        hence contradiction;

      end;

      

       B11: for i be Nat st i < n holds (B . i) > 0

      proof

        let i be Nat;

        assume

         WHHO: i < n;

        assume 0 >= (B . i);

        then (B . i) = 0 ;

        then i in { i where i be Nat : (B . i) = 0 };

        hence contradiction by WHHO, CC1, NAT_1:def 1, KL11;

      end;

      

       A4: for i be Nat st i < n holds (B . (i + 1)) <= ((B . i) - 1)

      proof

        let i be Nat;

        assume i < n;

        then

         A5: (B . i) <> 0 by B11;

        (B . (i + 1)) = ((A . i) mod (B . i)) by L1;

        then ((B . (i + 1)) + 1) <= (B . i) by NAT_1: 13, A5, INT_1: 58;

        then (((B . (i + 1)) + 1) - 1) <= ((B . i) - 1) by XREAL_1: 9;

        hence (B . (i + 1)) <= ((B . i) - 1);

      end;

      defpred P[ Nat] means $1 <= n implies (B . $1) <= ((B . 0 ) - $1);

      

       A6: P[ 0 ];

      

       A7: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A8: P[i];

        assume

         B8: (i + 1) <= n;

        then i < n by XXREAL_0: 2, NAT_1: 16;

        then

         A9: (B . (i + 1)) <= ((B . i) - 1) by A4;

        ((B . i) - 1) <= (((B . 0 ) - i) - 1) by A8, B8, XXREAL_0: 2, NAT_1: 16, XREAL_1: 9;

        hence thesis by A9, XXREAL_0: 2;

      end;

      

       A70: for i be Nat holds P[i] from NAT_1:sch 2( A6, A7);

      

       LC0P: n <= (B . 0 )

      proof

        assume

         H1P: n > (B . 0 );

        

         H2: (B . n) <= ((B . 0 ) - n) by A70;

        ((B . 0 ) - n) < (n - n) by H1P, XREAL_1: 9;

        hence contradiction by H2;

      end;

      (A . n) = (A . ((n - 1) + 1))

      .= (B . (n - 1)) by L1, NIZ;

      then

       ASTS: ( 0 + 1) <= (A . n) by INT_1: 7, LX1;

      

       LKA1: for j be Nat st j < n holds (A . (j + 1)) < (A . j)

      proof

        let j be Nat;

        assume

         CCC1: j < n;

        now

          per cases ;

            case 0 < j;

            then ( 0 + 1) <= j by INT_1: 7;

            then (j - 1) in NAT by INT_1: 5;

            then

            reconsider k = (j - 1) as Nat;

            

             AME1: (A . (k + 1)) = (B . k) & (A . ((k + 1) + 1)) = (B . (k + 1)) by L1;

            (j - 1) < n by CCC1, XREAL_1: 51;

            then (B . (k + 1)) <= ((B . k) - 1) by A4;

            then ((B . (k + 1)) + 1) <= (((B . k) - 1) + 1) by XREAL_1: 6;

            hence thesis by AME1, NAT_1: 13;

          end;

            case j = 0 ;

            hence thesis by L1, ASKARI;

          end;

        end;

        hence thesis;

      end;

      

       ZM: 1 < n implies ( Fib 3) <= (A . (n - 1))

      proof

        assume 1 < n;

        then (1 - 1) < (n - 1) by XREAL_1: 9;

        then

         PZ1: 0 < (n - 1) & (n - 1) is Nat by LNNZ, NAT_1: 20;

        (n - 1) < (n - 0 ) by XREAL_1: 15;

        then (A . ((n - 1) + 1)) < (A . (n - 1)) by LKA1, PZ1;

        then 1 < (A . (n - 1)) by ASTS, XXREAL_0: 2;

        then (1 + 1) <= (A . (n - 1)) by INT_1: 7;

        hence thesis by FIB_NUM2: 22;

      end;

      

       TRMT: for i be Nat st 0 < i & i < n holds ((A . (i + 2)) + (A . (i + 1))) <= (A . i)

      proof

        let i be Nat;

        assume

         LP11: 0 < i & i < n;

        then (B . (i + 1)) <= ((B . i) - 1) by A4;

        then

         LK1: (B . (i + 1)) <= ((A . (i + 1)) - 1) by L1;

        

         LX: (A . (i + 1)) <= (A . i) by LP11, LKA1;

        ((A . i) mod (B . i)) <= ((A . (i + 1)) - 1) by L1, LK1;

        then ((A . i) mod (A . (i + 1))) <= ((A . (i + 1)) - 1) by L1;

        then

         CLL1: (((A . i) mod (A . (i + 1))) + 0 ) < (((A . (i + 1)) - 1) + 1) by XREAL_1: 8;

        then ((A . i) div (A . (i + 1))) >= 1 by NAT_2: 13, LX;

        then

         LCP: ((A . (i + 2)) + (A . (i + 1))) <= ((A . (i + 2)) + (((A . i) div (A . (i + 1))) * (A . (i + 1)))) by XREAL_1: 6, XREAL_1: 151;

        (A . (i + 2)) = (A . ((i + 1) + 1))

        .= (B . (i + 1)) by L1

        .= ((A . i) mod (B . i)) by L1

        .= ((A . i) mod (A . (i + 1))) by L1

        .= ((A . i) - (((A . i) div (A . (i + 1))) * (A . (i + 1)))) by INT_1:def 10, CLL1;

        hence thesis by LCP;

      end;

      

       LEMM1: for i be Nat st i < n holds ( Fib (i + 2)) <= (A . (n - i))

      proof

        defpred P[ Nat] means $1 < n implies ( Fib ($1 + 2)) <= (A . (n - $1));

        ( 0 + 1) <= n by INT_1: 7, LNNZ;

        then

         HYY1: 1 < (n + 1) by NAT_1: 13;

         LLLCT:

        now

          per cases by HYY1, NAT_1: 22;

            case n = 1;

            hence P[1];

          end;

            case 1 < n;

            thus P[1] by ZM;

          end;

        end;

        

         A1: for k be Nat st k >= 2 holds (for i be Nat st i >= 2 holds i < k implies P[i]) implies P[k]

        proof

          let k be Nat;

          assume

           A2: k >= 2;

          assume

           A3: for i be Nat st i >= 2 holds i < k implies P[i];

          

           AU4: for i be Nat holds i < k implies P[i]

          proof

            let i be Nat;

            assume

             NNNH: i < k;

            now

              per cases by NAT_1: 23;

                case i = 0 ;

                hence thesis by ASTS, FIB_NUM2: 21;

              end;

                case i = 1;

                hence thesis by LLLCT;

              end;

                case 2 <= i;

                hence thesis by A3, NNNH;

              end;

            end;

            hence thesis;

          end;

          (k - 1) in NAT by INT_1: 5, A2, XXREAL_0: 2;

          then

          reconsider x = (k - 1) as Nat;

          (k - 2) in NAT by A2, INT_1: 5;

          then

          reconsider y = (k - 2) as Nat;

          

           LLZZ: x < k & y < k by XREAL_1: 44;

          

           LLZ: P[x] & P[y] by AU4, XREAL_1: 44;

          now

            per cases ;

              case

               LLAQ: k < n;

              then (n - k) in NAT by INT_1: 5;

              then

              reconsider z = (n - k) as Nat;

              

               ZEE: z < n by XREAL_1: 231, A2;

              now

                per cases ;

                  case z = 0 ;

                  hence P[k];

                end;

                  case 0 < z;

                  then

                   SDD: ((A . (z + 2)) + (A . (z + 1))) <= (A . z) by TRMT, ZEE;

                  

                   LYY: (( Fib (x + 2)) + ( Fib (y + 2))) <= ((A . (z + 2)) + (A . (z + 1))) by XREAL_1: 7, LLAQ, LLZ, LLZZ, XXREAL_0: 2;

                  (( Fib (x + 2)) + ( Fib (y + 2))) = ( Fib (((y + 2) + 1) + 1)) by PRE_FF: 1

                  .= ( Fib (k + 2));

                  hence P[k] by SDD, XXREAL_0: 2, LYY;

                end;

              end;

              hence P[k];

            end;

              case n <= k;

              hence P[k];

            end;

          end;

          hence P[k];

        end;

        

         A10: for k be Nat st k >= 2 holds P[k] from NAT_1:sch 9( A1);

        for i be Nat st i <= n holds P[i]

        proof

          let i be Nat;

          i < (1 + 1) or 2 <= i;

          then

           LLP1: i <= 1 or 2 <= i by INT_1: 7;

          now

            per cases by LLP1, NAT_1: 25;

              case i = 0 ;

              thus P[ 0 ] by ASTS, FIB_NUM2: 21;

            end;

              case i = 1;

              thus P[1] by LLLCT;

            end;

              case 2 <= i;

              hence thesis by A10;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      reconsider m = (n - 1) as Nat by LNNZ, NAT_1: 20;

      (n - 1) < (n - 0 ) by XREAL_1: 15;

      then

       G1P: ( Fib (m + 2)) <= (A . (n - m)) by LEMM1;

      

       G2P: (A . 1) = (A . ( 0 + 1))

      .= |.b.| by L1;

      ( 0 + 1) <= n by INT_1: 7, LNNZ;

      then

       HYY1: 1 < (n + 1) by NAT_1: 13;

      

       CLAME: n <= (5 * [/( log (10, |.b.|))\])

      proof

        now

          per cases by HYY1, NAT_1: 22;

            case

             TKK: n = 1;

            b <= |.b.| by ABSVALUE: 4;

            then 1 < |.b.| by XXREAL_0: 2, ASKARI;

            then ( log (10,1)) < ( log (10, |.b.|)) by POWER: 57;

            then 0 < ( log (10, |.b.|)) by POWER: 51;

            then 0 < [/( log (10, |.b.|))\] by INT_1:def 7;

            then ( 0 + 1) <= (5 * [/( log (10, |.b.|))\]) by INT_1: 7;

            hence thesis by TKK;

          end;

            case

             GF: 1 < n;

            then (1 + 1) <= n by INT_1: 7;

            then (2 + 1) <= (n + 1) by XREAL_1: 6;

            then ( tau to_power ((n + 1) - 2)) < ( Fib (n + 1)) by LTAUPOW;

            then

             GCV: ( tau to_power (n - 1)) < |.b.| by XXREAL_0: 2, G2P, G1P;

            (1 - 1) < (n - 1) by XREAL_1: 9, GF;

            then 0 < ( tau to_power (n - 1)) by THTU, POWER: 35;

            then ( log ( tau ,( tau to_power (n - 1)))) <= ( log ( tau , |.b.|)) by ASYMPT_2: 7, GCV, THTU;

            then ((n - 1) * ( log ( tau , tau ))) <= ( log ( tau , |.b.|)) by POWER: 55, THTU;

            then ((n - 1) * 1) <= ( log ( tau , |.b.|)) by POWER: 52, THTU;

            then

             FAW: (n - 1) <= (( log ( tau ,10)) * ( log (10, |.b.|))) by POWER: 56, THTU, ASKARI;

            b <= |.b.| by ABSVALUE: 4;

            then 1 < |.b.| by XXREAL_0: 2, ASKARI;

            then ( log (10,1)) < ( log (10, |.b.|)) by POWER: 57;

            then 0 < ( log (10, |.b.|)) by POWER: 51;

            then (( log ( tau ,10)) * ( log (10, |.b.|))) < (5 * ( log (10, |.b.|))) by XREAL_1: 68, THTU3;

            then

             MB3: (n - 1) < (5 * ( log (10, |.b.|))) by FAW, XXREAL_0: 2;

            ( log (10, |.b.|)) <= [/( log (10, |.b.|))\] by INT_1:def 7;

            then (5 * ( log (10, |.b.|))) <= (5 * [/( log (10, |.b.|))\]) by XREAL_1: 64;

            then (n - 1) < (5 * [/( log (10, |.b.|))\]) by XXREAL_0: 2, MB3;

            then ((n - 1) + 1) <= (5 * [/( log (10, |.b.|))\]) by INT_1: 7;

            hence n <= (5 * [/( log (10, |.b.|))\]);

          end;

        end;

        hence thesis;

      end;

      reconsider C = ( seq_n^ 1) as Real_Sequence;

      set nb = |.b.|;

      

       LC2P: (C . |.b.|) = ( |.b.| to_power 1) by ASYMPT_1:def 3, ASKARI;

      

       LC1P: ( seq_n^ 1) in ( Big_Oh ( seq_n^ 1)) by ASYMPT_0: 10;

      take A, B, C, n;

      thus (A . 0 ) = |.a.| & (B . 0 ) = |.b.| & (for i be Nat holds (A . (i + 1)) = (B . i) & (B . (i + 1)) = ((A . i) mod (B . i))) & n = ( min* { i where i be Nat : (B . i) = 0 }) & (a gcd b) = (A . n) & ( Fib (n + 1)) <= |.b.| & n <= (5 * [/( log (10, |.b.|))\]) & n <= (C . |.b.|) & C is polynomially-bounded by L1, LC1P, LC2P, CC1, NTALGO_1: 2, CLAME, G2P, G1P, LC0P;

    end;