binari_6.miz



    begin

    theorem :: BINARI_6:1

    

     LM000: for x be Nat holds ex m be Nat st x < (2 to_power m)

    proof

      let x be Nat;

      per cases ;

        suppose

         C1: x = 0 ;

        take m = 0 ;

        thus x < (2 to_power m) by C1, POWER: 24;

      end;

        suppose x <> 0 ;

        then 0 < x;

        then

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

        

         X1: ( log (2,x)) <= |.( log (2,x)).| by COMPLEX1: 76;

         0 < ( [/ |.( log (2,x)).|\] + 1) by INT_1: 32;

        then

        reconsider m = ( [/ |.( log (2,x)).|\] + 1) as Nat by INT_1: 3, ORDINAL1:def 12;

        

         P3: ( log (2,x)) < m by X1, INT_1: 32, XXREAL_0: 2;

        take m;

        thus x < (2 to_power m) by P2, P3, POWER: 39;

      end;

    end;

    theorem :: BINARI_6:2

    

     LM001: for x be Nat st x <> 0 holds ex n be Nat st (2 to_power n) <= x & x < (2 to_power (n + 1))

    proof

      let x be Nat;

      assume x <> 0 ;

      then

       P1: 1 <= x by NAT_1: 25;

      defpred P1[ Nat] means x < (2 to_power $1);

      

       A2: ex m be Nat st P1[m] by LM000;

      consider k be Nat such that

       A3: P1[k] & (for n be Nat st P1[n] holds k <= n) from NAT_1:sch 5( A2);

      k <> 0 by P1, POWER: 24, A3;

      then 1 <= k by NAT_1: 25;

      then 0 <= (k - 1) by XREAL_1: 48;

      then

      reconsider k1 = (k - 1) as Nat by INT_1: 3, ORDINAL1:def 12;

      take k1;

      thus (2 to_power k1) <= x

      proof

        assume

         ASP1: not (2 to_power k1) <= x;

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

        hence contradiction by A3, ASP1;

      end;

      thus x < (2 to_power (k1 + 1)) by A3;

    end;

    theorem :: BINARI_6:3

    

     LM002: for x be Nat, n1,n2 be Nat st (2 to_power n1) <= x & x < (2 to_power (n1 + 1)) & (2 to_power n2) <= x & x < (2 to_power (n2 + 1)) holds n1 = n2

    proof

      let x be Nat, n1,n2 be Nat;

      assume that

       AS1: (2 to_power n1) <= x & x < (2 to_power (n1 + 1)) and

       AS2: (2 to_power n2) <= x & x < (2 to_power (n2 + 1));

      assume n1 <> n2;

      per cases by XXREAL_0: 1;

        suppose n1 < n2;

        then

         P1: (n1 + 1) <= n2 by NAT_1: 13;

        (2 to_power (n1 + 1)) <= (2 to_power n2)

        proof

          per cases by P1, XXREAL_0: 1;

            suppose (n1 + 1) = n2;

            hence (2 to_power (n1 + 1)) <= (2 to_power n2);

          end;

            suppose (n1 + 1) < n2;

            hence (2 to_power (n1 + 1)) <= (2 to_power n2) by POWER: 39;

          end;

        end;

        hence contradiction by AS2, AS1, XXREAL_0: 2;

      end;

        suppose n2 < n1;

        then

         P1: (n2 + 1) <= n1 by NAT_1: 13;

        (2 to_power (n2 + 1)) <= (2 to_power n1)

        proof

          per cases by P1, XXREAL_0: 1;

            suppose (n2 + 1) = n1;

            hence (2 to_power (n2 + 1)) <= (2 to_power n1);

          end;

            suppose (n2 + 1) < n1;

            hence (2 to_power (n2 + 1)) <= (2 to_power n1) by POWER: 39;

          end;

        end;

        hence contradiction by AS1, AS2, XXREAL_0: 2;

      end;

    end;

    theorem :: BINARI_6:4

    

     LM0020: <* 0 *> = ( 0* 1) by FINSEQ_2: 59;

    theorem :: BINARI_6:5

    for n1,n2 be Nat holds (( 0* n1) ^ ( 0* n2)) = ( 0* (n1 + n2)) by FINSEQ_2: 123;

    begin

    definition

      let x be Nat;

      :: BINARI_6:def1

      func LenBSeq x -> non zero Nat means

      : Def1: it = 1 if x = 0

      otherwise ex n be Nat st (2 to_power n) <= x & x < (2 to_power (n + 1)) & it = (n + 1);

      existence

      proof

        thus x = 0 implies ex y be non zero Nat st y = 1;

        thus not x = 0 implies ex y be non zero Nat st ex n be Nat st (2 to_power n) <= x & x < (2 to_power (n + 1)) & y = (n + 1)

        proof

          assume x <> 0 ;

          then

          consider n be Nat such that

           A1: (2 to_power n) <= x & x < (2 to_power (n + 1)) by LM001;

          take y = (n + 1);

          thus thesis by A1;

        end;

      end;

      uniqueness by LM002;

      consistency ;

    end

    theorem :: BINARI_6:6

    

     LM006: for x be Nat holds x < (2 to_power ( LenBSeq x))

    proof

      let x be Nat;

      per cases ;

        suppose

         C1: x = 0 ;

        then ( LenBSeq x) = 1 by Def1;

        hence x < (2 to_power ( LenBSeq x)) by POWER: 25, C1;

      end;

        suppose x <> 0 ;

        then

        consider n be Nat such that

         C2: (2 to_power n) <= x & x < (2 to_power (n + 1)) & ( LenBSeq x) = (n + 1) by Def1;

        thus x < (2 to_power ( LenBSeq x)) by C2;

      end;

    end;

    theorem :: BINARI_6:7

    

     LM007: for x be Nat holds x = ( Absval (( LenBSeq x) -BinarySequence x))

    proof

      let x be Nat;

      x < (2 to_power ( LenBSeq x)) by LM006;

      hence x = ( Absval (( LenBSeq x) -BinarySequence x)) by BINARI_3: 35;

    end;

    theorem :: BINARI_6:8

    

     LM0071: for n be Nat, x be Tuple of (n + 1), BOOLEAN st (x . (n + 1)) = 1 holds (2 to_power n) <= ( Absval x) & ( Absval x) < (2 to_power (n + 1))

    proof

      let n be Nat, x be Tuple of (n + 1), BOOLEAN ;

      assume

       AS: (x . (n + 1)) = 1;

      ( len x) = (n + 1) by CARD_1:def 7;

      then (n + 1) in ( Seg ( len x)) by FINSEQ_1: 4;

      then (n + 1) in ( dom x) by FINSEQ_1:def 3;

      then

       P3: (x /. (n + 1)) = 1 by AS, PARTFUN1:def 6;

       0 <= ((n + 1) - 1);

      then ((n + 1) -' 1) = n by XREAL_0:def 2;

      hence (2 to_power n) <= ( Absval x) by BINARI_4: 12, P3;

      thus ( Absval x) < (2 to_power (n + 1)) by BINARI_3: 1;

    end;

    theorem :: BINARI_6:9

    ex F be Function of ( BOOLEAN * ), NAT st for x be Element of ( BOOLEAN * ) holds ex x0 be Tuple of ( len x), BOOLEAN st x = x0 & (F . x) = ( Absval x0)

    proof

      defpred P[ Element of ( BOOLEAN * ), object] means ex x0 be Tuple of ( len $1), BOOLEAN st $1 = x0 & $2 = ( Absval x0);

      

       A1: for x be Element of ( BOOLEAN * ) holds ex y be Element of NAT st P[x, y]

      proof

        let x be Element of ( BOOLEAN * );

        x is Element of (( len x) -tuples_on BOOLEAN ) by FINSEQ_2: 92;

        then

        reconsider x0 = x as Tuple of ( len x), BOOLEAN ;

        reconsider n = ( Absval x0) as Element of NAT ;

        take n;

        thus ex x0 be Tuple of ( len x), BOOLEAN st x = x0 & n = ( Absval x0);

      end;

      consider f be Function of ( BOOLEAN * ), NAT such that

       A2: for x be Element of ( BOOLEAN * ) holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      take f;

      thus thesis by A2;

    end;

    

     LM020: ex F be Function of NAT , ( BOOLEAN * ) st for x be Element of NAT holds (F . x) = (( LenBSeq x) -BinarySequence x)

    proof

      defpred P[ Element of NAT , object] means $2 = (( LenBSeq $1) -BinarySequence $1);

      

       A1: for x be Element of NAT holds ex y be Element of ( BOOLEAN * ) st P[x, y]

      proof

        let x be Element of NAT ;

        set y = (( LenBSeq x) -BinarySequence x);

        reconsider y as Element of ( BOOLEAN * ) by FINSEQ_1:def 11;

        take y;

        thus thesis;

      end;

      consider f be Function of NAT , ( BOOLEAN * ) such that

       A2: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      take f;

      thus thesis by A2;

    end;

    

     LM030: for F be Function of NAT , ( BOOLEAN * ) st for x be Element of NAT holds (F . x) = (( LenBSeq x) -BinarySequence x) holds F is one-to-one

    proof

      let f be Function of NAT , ( BOOLEAN * );

      assume

       AS1: for x be Element of NAT holds (f . x) = (( LenBSeq x) -BinarySequence x);

      for x1,x2 be object st x1 in NAT & x2 in NAT & (f . x1) = (f . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A0: x1 in NAT & x2 in NAT & (f . x1) = (f . x2);

        then

        reconsider k1 = x1, k2 = x2 as Element of NAT ;

        

         A3: (( LenBSeq k1) -BinarySequence k1) = (f . k1) by AS1

        .= (( LenBSeq k2) -BinarySequence k2) by AS1, A0;

        

         NN: ( LenBSeq k1) is Element of NAT & ( LenBSeq k2) is Element of NAT by ORDINAL1:def 12;

        (( LenBSeq k1) -BinarySequence k1) in (( LenBSeq k1) -tuples_on BOOLEAN ) by FINSEQ_2: 131;

        then

         A4: ( len (( LenBSeq k1) -BinarySequence k1)) = ( LenBSeq k1) by NN, FINSEQ_2: 132;

        (( LenBSeq k2) -BinarySequence k2) in (( LenBSeq k2) -tuples_on BOOLEAN ) by FINSEQ_2: 131;

        then

         A5: ( LenBSeq k1) = ( LenBSeq k2) by A4, A3, NN, FINSEQ_2: 132;

        

        thus x1 = ( Absval (( LenBSeq k1) -BinarySequence k1)) by LM007

        .= x2 by LM007, A3, A5;

      end;

      hence thesis by FUNCT_2: 19;

    end;

    definition

      :: BINARI_6:def2

      func Nat2BL -> Function of NAT , ( BOOLEAN * ) means

      : Def2: for x be Element of NAT holds (it . x) = (( LenBSeq x) -BinarySequence x);

      existence by LM020;

      uniqueness

      proof

        let f1,f2 be Function of NAT , ( BOOLEAN * );

        assume

         AS1: for x be Element of NAT holds (f1 . x) = (( LenBSeq x) -BinarySequence x);

        assume

         AS2: for x be Element of NAT holds (f2 . x) = (( LenBSeq x) -BinarySequence x);

        for x be Element of NAT holds (f1 . x) = (f2 . x)

        proof

          let x be Element of NAT ;

          

          thus (f1 . x) = (( LenBSeq x) -BinarySequence x) by AS1

          .= (f2 . x) by AS2;

        end;

        hence f1 = f2 by FUNCT_2:def 8;

      end;

    end

    theorem :: BINARI_6:10

    for x be Element of NAT , y be Tuple of ( LenBSeq x), BOOLEAN st ( Nat2BL . x) = y holds ( Absval y) = x

    proof

      let x be Element of NAT , y be Tuple of ( LenBSeq x), BOOLEAN ;

      assume

       AS: ( Nat2BL . x) = y;

      ( Nat2BL . x) = (( LenBSeq x) -BinarySequence x) by Def2;

      hence thesis by AS, LM007;

    end;

    theorem :: BINARI_6:11

    

     LM031: ( rng Nat2BL ) = ({ x where x be Element of ( BOOLEAN * ) : (x . ( len x)) = 1 } \/ { <* 0 *>})

    proof

      for z be object holds z in ( rng Nat2BL ) iff z in ({ x where x be Element of ( BOOLEAN * ) : (x . ( len x)) = 1 } \/ { <* 0 *>})

      proof

        let z be object;

        hereby

          assume z in ( rng Nat2BL );

          then

          consider x be object such that

           A2: x in NAT & z = ( Nat2BL . x) by FUNCT_2: 11;

          reconsider x as Element of NAT by A2;

          

           A3: ( Nat2BL . x) = (( LenBSeq x) -BinarySequence x) by Def2;

          set y = (( LenBSeq x) -BinarySequence x);

          per cases ;

            suppose

             C1: x = 0 ;

            then ( LenBSeq x) = 1 by Def1;

            then ( Nat2BL . x) = <* 0 *> by LM0020, C1, BINARI_3: 25, A3;

            then z in { <* 0 *>} by A2, TARSKI:def 1;

            hence z in ({ x where x be Element of ( BOOLEAN * ) : (x . ( len x)) = 1 } \/ { <* 0 *>}) by XBOOLE_0:def 3;

          end;

            suppose x <> 0 ;

            then

            consider n be Nat such that

             P1: (2 to_power n) <= x & x < (2 to_power (n + 1)) & ( LenBSeq x) = (n + 1) by Def1;

            

             P2: y in ( BOOLEAN * ) by A3, FUNCT_2: 5;

            per cases ;

              suppose n <> 0 ;

              then ((( LenBSeq x) -BinarySequence x) . ( LenBSeq x)) = 1 by P1, BINARI_3: 29;

              then (y . ( len y)) = 1 by CARD_1:def 7;

              then z in { x where x be Element of ( BOOLEAN * ) : (x . ( len x)) = 1 } by P2, A2, A3;

              hence z in ({ x where x be Element of ( BOOLEAN * ) : (x . ( len x)) = 1 } \/ { <* 0 *>}) by XBOOLE_0:def 3;

            end;

              suppose

               C1: n = 0 ;

              then 1 <= x & x < (1 + 1) by POWER: 24, POWER: 25, P1;

              then 1 <= x & x <= 1 by NAT_1: 13;

              then x = 1 by XXREAL_0: 1;

              then

               C2: x = (2 to_power n) by C1, POWER: 24;

              ((n + 1) -BinarySequence (2 to_power n)) = (( 0* n) ^ <*1*>) by BINARI_3: 28

              .= ( {} ^ <*1*>) by C1

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

              then ( len y) = 1 & (y . 1) = 1 by FINSEQ_1: 40, P1, C2;

              then z in { x where x be Element of ( BOOLEAN * ) : (x . ( len x)) = 1 } by P2, A2, A3;

              hence z in ({ x where x be Element of ( BOOLEAN * ) : (x . ( len x)) = 1 } \/ { <* 0 *>}) by XBOOLE_0:def 3;

            end;

          end;

        end;

        assume z in ({ x where x be Element of ( BOOLEAN * ) : (x . ( len x)) = 1 } \/ { <* 0 *>});

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

        per cases by TARSKI:def 1;

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

          then

          consider x be Element of ( BOOLEAN * ) such that

           A3: z = x & (x . ( len x)) = 1;

          set n = ( len x);

          x is Element of (( len x) -tuples_on BOOLEAN ) by FINSEQ_2: 92;

          then

          reconsider x as Tuple of n, BOOLEAN ;

          set L = ( Absval x);

          

           A4: ( Nat2BL . L) = (( LenBSeq L) -BinarySequence L) by Def2;

          L < (2 to_power ( LenBSeq L)) by LM006;

          then

           A5: ( Absval (( LenBSeq L) -BinarySequence L)) = ( Absval x) by BINARI_3: 35;

          ( len x) <> 0 by A3;

          then 0 < ( len x);

          then ( 0 + 1) <= ( len x) by NAT_1: 13;

          then

          reconsider n1 = (n - 1) as Element of NAT by INT_1: 5;

          (x . (n1 + 1)) = 1 by A3;

          then

           X3: (2 to_power n1) <= L & L < (2 to_power (n1 + 1)) by LM0071;

          then 0 < L by POWER: 34;

          then ( LenBSeq L) = n by Def1, X3;

          then z = ( Nat2BL . L) by A4, A3, BINARI_3: 2, A5;

          hence z in ( rng Nat2BL ) by FUNCT_2: 4;

        end;

          suppose

           C1: z = <* 0 *>;

          ( LenBSeq 0 ) = 1 by Def1;

          

          then ( Nat2BL . 0 ) = (1 -BinarySequence 0 ) by Def2

          .= z by C1, BINARI_3: 25, LM0020;

          hence z in ( rng Nat2BL ) by FUNCT_2: 4;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: BINARI_6:12

     Nat2BL is one-to-one

    proof

      for x be Element of NAT holds ( Nat2BL . x) = (( LenBSeq x) -BinarySequence x) by Def2;

      hence Nat2BL is one-to-one by LM030;

    end;

    definition

      let x,y be Element of ( BOOLEAN * );

      assume

       AS: ( len x) <> 0 & ( len y) <> 0 ;

      :: BINARI_6:def3

      func LenMax (x,y) -> non zero Nat equals

      : Def15: ( max (( len x),( len y)));

      correctness by XXREAL_0: 16, AS;

    end

    definition

      let K be Nat, x be Element of ( BOOLEAN * );

      :: BINARI_6:def4

      func ExtBit (x,K) -> Tuple of K, BOOLEAN equals

      : Def20: (x ^ ( 0* (K -' ( len x)))) if ( len x) <= K

      otherwise (x | K);

      coherence

      proof

        thus ( len x) <= K implies (x ^ ( 0* (K -' ( len x)))) is Tuple of K, BOOLEAN

        proof

          assume ( len x) <= K;

          then

           A2: (K -' ( len x)) = (K - ( len x)) by XREAL_0:def 2, XREAL_1: 48;

          ( 0* (K -' ( len x))) in ( BOOLEAN * ) by BINARI_3: 4;

          then

          reconsider z = ( 0* (K -' ( len x))) as Tuple of (K -' ( len x)), BOOLEAN by FINSEQ_1:def 11;

          x is Element of (( len x) -tuples_on BOOLEAN ) by FINSEQ_2: 92;

          then

          reconsider y = x as Tuple of ( len x), BOOLEAN ;

          (y ^ z) is Tuple of K, BOOLEAN by A2;

          hence thesis;

        end;

        thus not ( len x) <= K implies (x | K) is Tuple of K, BOOLEAN

        proof

          assume not ( len x) <= K;

          then

           A1: ( len (x | K)) = K by FINSEQ_1: 59;

          (x | K) is Element of (( len (x | K)) -tuples_on BOOLEAN ) by FINSEQ_2: 92;

          hence thesis by A1;

        end;

      end;

      consistency ;

    end

    theorem :: BINARI_6:13

    

     LMExtBit1: for K be Nat, x be Element of ( BOOLEAN * ) st ( len x) <= K holds ( ExtBit (x,(K + 1))) = (( ExtBit (x,K)) ^ <* 0 *>)

    proof

      let K be Nat, x be Element of ( BOOLEAN * );

      assume

       AS: ( len x) <= K;

      

       A1: (K + 0 ) <= (K + 1) by XREAL_1: 7;

      then

       AA1: ( len x) <= (K + 1) by AS, XXREAL_0: 2;

      

       A2: ( ExtBit (x,K)) = (x ^ ( 0* (K -' ( len x)))) by AS, Def20;

      

       A3: ( ExtBit (x,(K + 1))) = (x ^ ( 0* ((K + 1) -' ( len x)))) by A1, Def20, AS, XXREAL_0: 2;

      

       B1: (K -' ( len x)) = (K - ( len x)) by XREAL_0:def 2, AS, XREAL_1: 48;

      ((K + 1) -' ( len x)) = ((K + 1) - ( len x)) by XREAL_0:def 2, AA1, XREAL_1: 48;

      then ((K + 1) -' ( len x)) = ((K -' ( len x)) + 1) by B1;

      then ( 0* ((K + 1) -' ( len x))) = (( 0* (K -' ( len x))) ^ <* 0 *>) by FINSEQ_2: 60;

      hence ( ExtBit (x,(K + 1))) = (( ExtBit (x,K)) ^ <* 0 *>) by A2, FINSEQ_1: 32, A3;

    end;

    theorem :: BINARI_6:14

    

     LMExtBit8: for K be non zero Nat, x be Element of ( BOOLEAN * ) st ( len x) = K holds ( ExtBit (x,K)) = x

    proof

      let K be non zero Nat, x be Element of ( BOOLEAN * );

      assume

       PA1: ( len x) = K;

      then

       A1: (K - ( len x)) = 0 ;

      

      thus ( ExtBit (x,K)) = (x ^ ( 0* (K -' ( len x)))) by PA1, Def20

      .= (x ^ ( 0* 0 )) by XREAL_0:def 2, A1

      .= x by FINSEQ_1: 34;

    end;

    theorem :: BINARI_6:15

    

     LMExtBit2: for K be non zero Nat, x,y be Tuple of K, BOOLEAN , x1,y1 be Tuple of (K + 1), BOOLEAN st x1 = (x ^ <* 0 *>) & y1 = (y ^ <* 0 *>) holds (x1,y1) are_summable

    proof

      let K be non zero Nat, x,y be Tuple of K, BOOLEAN , x1,y1 be Tuple of (K + 1), BOOLEAN ;

      set K1 = (K + 1);

      assume

       A1: x1 = (x ^ <* 0 *>) & y1 = (y ^ <* 0 *>);

      

       A5: ( len x) = K & ( len y) = K by CARD_1:def 7;

      

       A6: ( len x1) = (K + 1) & ( len y1) = (K + 1) by CARD_1:def 7;

      

       A7: K1 in ( Seg K1) by FINSEQ_1: 4;

      then K1 in ( dom x1) by FINSEQ_1:def 3, A6;

      then (x1 /. K1) = (x1 . K1) by PARTFUN1:def 6;

      then

       A3: (x1 /. K1) = 0 by FINSEQ_1: 42, A1, A5;

      K1 in ( dom y1) by FINSEQ_1:def 3, A6, A7;

      then (y1 /. K1) = (y1 . K1) by PARTFUN1:def 6;

      then ((((x1 /. K1) '&' (y1 /. K1)) 'or' ((x1 /. K1) '&' (( carry (x1,y1)) /. K1))) 'or' ((y1 /. K1) '&' (( carry (x1,y1)) /. K1))) = 0 by A3, FINSEQ_1: 42, A1, A5;

      then ( add_ovfl (x1,y1)) = FALSE by BINARITH:def 6;

      hence thesis by BINARITH:def 7;

    end;

    theorem :: BINARI_6:16

    

     LMExtBit4: for K be non zero Nat, y be Tuple of K, BOOLEAN st y = ( 0* K) holds for n be non zero Nat st n <= K holds (y /. n) = 0

    proof

      let K be non zero Nat, y be Tuple of K, BOOLEAN ;

      assume

       AS1: y = ( 0* K);

      let n be non zero Nat;

      assume

       AS2: n <= K;

      

       A1: ( len y) = K by CARD_1:def 7;

       0 < n;

      then (1 + 0 ) <= n by NAT_1: 13;

      then n in ( Seg K) by FINSEQ_1: 1, AS2;

      then n in ( dom y) by A1, FINSEQ_1:def 3;

      

      hence (y /. n) = (y . n) by PARTFUN1:def 6

      .= 0 by AS1;

    end;

    theorem :: BINARI_6:17

    

     LMExtBit501: for K be non zero Nat, x,y be Tuple of K, BOOLEAN holds ( carry (x,y)) = ( carry (y,x))

    proof

      let K be non zero Nat, x,y be Tuple of K, BOOLEAN ;

      

       A1: (( carry (x,y)) /. 1) = FALSE & (for i be Nat st 1 <= i & i < K holds (( carry (x,y)) /. (i + 1)) = ((((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (( carry (x,y)) /. i))) 'or' ((y /. i) '&' (( carry (x,y)) /. i)))) by BINARITH:def 2;

      for i be Nat st 1 <= i & i < K holds (( carry (x,y)) /. (i + 1)) = ((((y /. i) '&' (x /. i)) 'or' ((y /. i) '&' (( carry (x,y)) /. i))) 'or' ((x /. i) '&' (( carry (x,y)) /. i)))

      proof

        let i be Nat;

        assume 1 <= i & i < K;

        

        hence (( carry (x,y)) /. (i + 1)) = ((((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (( carry (x,y)) /. i))) 'or' ((y /. i) '&' (( carry (x,y)) /. i))) by BINARITH:def 2

        .= ((((y /. i) '&' (x /. i)) 'or' ((y /. i) '&' (( carry (x,y)) /. i))) 'or' ((x /. i) '&' (( carry (x,y)) /. i)));

      end;

      hence ( carry (x,y)) = ( carry (y,x)) by A1, BINARITH:def 2;

    end;

    theorem :: BINARI_6:18

    

     LMExtBit3: for K be non zero Nat, x,y be Tuple of K, BOOLEAN st y = ( 0* K) holds for n be non zero Nat st n <= K holds (( carry (x,y)) /. n) = 0 & (( carry (y,x)) /. n) = 0

    proof

      let K be non zero Nat, x,y be Tuple of K, BOOLEAN ;

      assume

       AS: y = ( 0* K);

      defpred P[ Nat] means 1 <= $1 & $1 <= K implies (( carry (x,y)) /. $1) = 0 ;

      

       P1: P[1] by BINARITH:def 2;

      

       P2: for i be non zero Nat st P[i] holds P[(i + 1)]

      proof

        let i be non zero Nat;

        assume

         A2: P[i];

        assume 1 <= (i + 1) & (i + 1) <= K;

        then

         A4: 1 <= i & i < K by NAT_1: 25, XXREAL_0: 2, NAT_1: 16;

        

        hence (( carry (x,y)) /. (i + 1)) = ((((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (( carry (x,y)) /. i))) 'or' ((y /. i) '&' (( carry (x,y)) /. i))) by BINARITH:def 2

        .= 0 by A4, A2, AS, LMExtBit4;

      end;

      

       P3: for k be non zero Nat holds P[k] from NAT_1:sch 10( P1, P2);

      let n be non zero Nat;

      assume n <= K;

      then 1 <= n & n <= K by NAT_1: 25;

      hence (( carry (x,y)) /. n) = 0 by P3;

      hence (( carry (y,x)) /. n) = 0 by LMExtBit501;

    end;

    theorem :: BINARI_6:19

    

     LMExtBit500: for K be non zero Nat, x,y be Tuple of K, BOOLEAN holds (x + y) = (y + x)

    proof

      let K be non zero Nat, x,y be Tuple of K, BOOLEAN ;

      for i be Nat st i in ( Seg K) holds ((x + y) /. i) = (((y /. i) 'xor' (x /. i)) 'xor' (( carry (y,x)) /. i))

      proof

        let i be Nat;

        assume i in ( Seg K);

        then ((x + y) /. i) = (((x /. i) 'xor' (y /. i)) 'xor' (( carry (x,y)) /. i)) by BINARITH:def 5;

        hence ((x + y) /. i) = (((y /. i) 'xor' (x /. i)) 'xor' (( carry (y,x)) /. i)) by LMExtBit501;

      end;

      hence (x + y) = (y + x) by BINARITH:def 5;

    end;

    theorem :: BINARI_6:20

    

     LMExtBit5: for K be non zero Nat, x,y be Tuple of K, BOOLEAN st y = ( 0* K) holds (x + y) = x & (y + x) = x

    proof

      let K be non zero Nat, x,y be Tuple of K, BOOLEAN ;

      assume

       AS: y = ( 0* K);

      for i be Nat st i in ( Seg K) holds ((x + y) . i) = (x . i)

      proof

        let i be Nat;

        assume

         A1: i in ( Seg K);

        then

         A4: 1 <= i & i <= K & i <> 0 by FINSEQ_1: 1;

        

         A2: (y /. i) = 0 by AS, A4, LMExtBit4;

        

         A3: (( carry (x,y)) /. i) = 0 by AS, A4, LMExtBit3;

        ( len x) = K by CARD_1:def 7;

        then

         D1: ( dom x) = ( Seg K) by FINSEQ_1:def 3;

        ( len (x + y)) = K by CARD_1:def 7;

        then

         D2: ( dom (x + y)) = ( Seg K) by FINSEQ_1:def 3;

        

        thus ((x + y) . i) = ((x + y) /. i) by D2, A1, PARTFUN1:def 6

        .= (((x /. i) 'xor' (y /. i)) 'xor' (( carry (x,y)) /. i)) by BINARITH:def 5, A1

        .= (x . i) by D1, A1, PARTFUN1:def 6, A2, A3;

      end;

      hence (x + y) = x by FINSEQ_2: 119;

      hence (y + x) = x by LMExtBit500;

    end;

    theorem :: BINARI_6:21

    

     LMExtBit9: for K be non zero Nat, x,y be Tuple of K, BOOLEAN st (x . ( len x)) = 1 & (y . ( len y)) = 1 holds not (x,y) are_summable

    proof

      let K be non zero Nat, x,y be Tuple of K, BOOLEAN ;

      assume

       AS: (x . ( len x)) = 1 & (y . ( len y)) = 1;

      

       A5: ( len x) = K & ( len y) = K by CARD_1:def 7;

      1 <= ( len x) by NAT_1: 25;

      then ( len x) in ( dom x) by FINSEQ_3: 25;

      then

       A6: (x /. K) = 1 by AS, A5, PARTFUN1:def 6;

      1 <= ( len y) by NAT_1: 25;

      then ( len y) in ( dom y) by FINSEQ_3: 25;

      then

       A7: (y /. K) = 1 by AS, A5, PARTFUN1:def 6;

      ((((x /. K) '&' (y /. K)) 'or' ((x /. K) '&' (( carry (x,y)) /. K))) 'or' ((y /. K) '&' (( carry (x,y)) /. K))) = 1 by A6, A7;

      then ( add_ovfl (x,y)) = 1 by BINARITH:def 6;

      hence thesis by BINARITH:def 7;

    end;

    

     LMExtBit60: for K be non zero Nat, x,y be Tuple of K, BOOLEAN st (x,y) are_summable & (x . ( len x)) = 1 holds ((x + y) . ( len (x + y))) = 1

    proof

      let K be non zero Nat, x,y be Tuple of K, BOOLEAN ;

      assume

       AS: (x,y) are_summable & (x . ( len x)) = 1;

      

       L0: ( len y) = K by CARD_1:def 7;

      1 <= ( len y) by NAT_1: 25;

      then ( len y) in ( Seg K) by L0, FINSEQ_1: 1;

      then

       L1: ( len y) in ( dom y) by L0, FINSEQ_1:def 3;

      

       R0: ( len x) = K by CARD_1:def 7;

      1 <= ( len x) by NAT_1: 25;

      then

       PR2: ( len x) in ( dom x) by FINSEQ_3: 25;

      

       P1: (y . ( len y)) = 0

      proof

        assume

         A1: (y . ( len y)) <> 0 ;

        (y . ( len y)) in ( rng y) by L1, FUNCT_1: 3;

        then (y . ( len y)) in BOOLEAN by FINSEQ_1:def 4, TARSKI:def 3;

        then (y . ( len y)) = 1 by A1, MARGREL1:def 11, TARSKI:def 2;

        hence contradiction by LMExtBit9, AS;

      end;

      

       P2: ( len (x + y)) = K by CARD_1:def 7;

      1 <= ( len (x + y)) by NAT_1: 25;

      then

       P3: ( len (x + y)) in ( Seg K) by P2, FINSEQ_1: 1;

      then

       PP5: ( len (x + y)) in ( dom (x + y)) by P2, FINSEQ_1:def 3;

      

       R3: (x /. ( len (x + y))) = 1 by PR2, P2, R0, AS, PARTFUN1:def 6;

      

       L3: (y /. ( len (x + y))) = 0 by P2, L0, P1, L1, PARTFUN1:def 6;

      

       K1: (( carry (x,y)) /. ( len (x + y))) = 0

      proof

        assume

         K2: not (( carry (x,y)) /. ( len (x + y))) = 0 ;

        (( carry (x,y)) /. ( len (x + y))) = 1 by K2, MARGREL1:def 11, TARSKI:def 2;

        then ((((x /. ( len (x + y))) '&' (y /. ( len (x + y)))) 'or' ((x /. ( len (x + y))) '&' (( carry (x,y)) /. ( len (x + y))))) 'or' ((y /. ( len (x + y))) '&' (( carry (x,y)) /. ( len (x + y))))) = 1 by R3;

        then ( add_ovfl (x,y)) = 1 by P2, BINARITH:def 6;

        hence contradiction by AS, BINARITH:def 7;

      end;

      ((x + y) /. ( len (x + y))) = (((x /. ( len (x + y))) 'xor' (y /. ( len (x + y)))) 'xor' (( carry (x,y)) /. ( len (x + y)))) by P3, BINARITH:def 5

      .= 1 by L3, K1, PR2, P2, R0, AS, PARTFUN1:def 6;

      hence thesis by PP5, PARTFUN1:def 6;

    end;

    theorem :: BINARI_6:22

    

     LMExtBit61: for K be non zero Nat, x,y be Tuple of K, BOOLEAN st (x,y) are_summable holds (y,x) are_summable

    proof

      let K be non zero Nat, x,y be Tuple of K, BOOLEAN ;

      assume (x,y) are_summable ;

      then ( add_ovfl (x,y)) = 0 by BINARITH:def 7;

      then

       P1: ((((x /. K) '&' (y /. K)) 'or' ((x /. K) '&' (( carry (x,y)) /. K))) 'or' ((y /. K) '&' (( carry (x,y)) /. K))) = 0 by BINARITH:def 6;

      (( carry (x,y)) /. K) = (( carry (y,x)) /. K) by LMExtBit501;

      then ((((y /. K) '&' (x /. K)) 'or' ((y /. K) '&' (( carry (y,x)) /. K))) 'or' ((x /. K) '&' (( carry (y,x)) /. K))) = 0 by P1;

      then ( add_ovfl (y,x)) = 0 by BINARITH:def 6;

      hence thesis by BINARITH:def 7;

    end;

    theorem :: BINARI_6:23

    

     LMExtBit6: for K be non zero Nat, x,y be Tuple of K, BOOLEAN st (x,y) are_summable & ((x . ( len x)) = 1 or (y . ( len y)) = 1) holds ((x + y) . ( len (x + y))) = 1

    proof

      let K be non zero Nat, x,y be Tuple of K, BOOLEAN ;

      assume

       AS: (x,y) are_summable & ((x . ( len x)) = 1 or (y . ( len y)) = 1);

      (x + y) = (y + x) by LMExtBit500;

      hence ((x + y) . ( len (x + y))) = 1 by LMExtBit60, LMExtBit61, AS;

    end;

    theorem :: BINARI_6:24

    

     LMExtBit7: for K be non zero Nat, x,y be Tuple of K, BOOLEAN , x1,y1 be Tuple of (K + 1), BOOLEAN st not (x,y) are_summable & x1 = (x ^ <* 0 *>) & y1 = (y ^ <* 0 *>) holds ((x1 + y1) . ( len (x1 + y1))) = 1

    proof

      let K be non zero Nat, x,y be Tuple of K, BOOLEAN , x1,y1 be Tuple of (K + 1), BOOLEAN ;

      assume

       AS: not (x,y) are_summable & x1 = (x ^ <* 0 *>) & y1 = (y ^ <* 0 *>);

      then

       X0: not ( add_ovfl (x,y)) = 0 by BINARITH:def 7;

      

       PX1: ( add_ovfl (x,y)) = 1 by X0, MARGREL1:def 11, TARSKI:def 2;

      then

       X1: ((((x /. K) '&' (y /. K)) 'or' ((x /. K) '&' (( carry (x,y)) /. K))) 'or' ((y /. K) '&' (( carry (x,y)) /. K))) = 1 by BINARITH:def 6;

      set K1 = (K + 1);

      

       X3: ( len x) = K & ( len y) = K by CARD_1:def 7;

      then

       XX3: ( len x) in ( Seg K) & ( len y) in ( Seg K) by FINSEQ_1: 3;

      

       L0: ( len y1) = K1 by CARD_1:def 7;

      1 <= ( len y1) by NAT_1: 25;

      then ( len y1) in ( dom y1) by FINSEQ_3: 25;

      

      then

       L2: (y1 /. ( len y1)) = (y1 . ( len y1)) by PARTFUN1:def 6

      .= 0 by L0, AS, FINSEQ_1: 42, X3;

      

       R0: ( len x1) = K1 by CARD_1:def 7;

      1 <= ( len x1) by NAT_1: 25;

      then ( len x1) in ( dom x1) by FINSEQ_3: 25;

      

      then

       R2: (x1 /. ( len x1)) = (x1 . ( len x1)) by PARTFUN1:def 6

      .= 0 by R0, AS, FINSEQ_1: 42, X3;

      

       P2: ( len (x1 + y1)) = K1 by CARD_1:def 7;

      1 <= ( len (x1 + y1)) by NAT_1: 25;

      then

       P3: ( len (x1 + y1)) in ( Seg K1) by P2, FINSEQ_1: 1;

      then

       PP5: ( len (x1 + y1)) in ( dom (x1 + y1)) by P2, FINSEQ_1:def 3;

      

       A1: (( carry (x,y)) /. 1) = FALSE & (for i be Nat st 1 <= i & i < K holds (( carry (x,y)) /. (i + 1)) = ((((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (( carry (x,y)) /. i))) 'or' ((y /. i) '&' (( carry (x,y)) /. i)))) by BINARITH:def 2;

      

       XR0: ( len ( carry (x,y))) = K by CARD_1:def 7;

      1 <= ( len ( carry (x,y))) by NAT_1: 25;

      then

       PXR1: ( len ( carry (x,y))) in ( Seg K) by XR0, FINSEQ_1: 1;

      reconsider i1 = 1 as Element of BOOLEAN by MARGREL1:def 11, TARSKI:def 2;

      reconsider Z1 = <*i1*> as FinSequence of BOOLEAN ;

      ( len Z1) = 1 by FINSEQ_1: 40;

      then

      reconsider Z1 = <*1*> as Tuple of 1, BOOLEAN ;

      (( carry (x,y)) ^ Z1) is Tuple of (K + 1), BOOLEAN ;

      then

      reconsider S = (( carry (x,y)) ^ <*1*>) as Tuple of K1, BOOLEAN ;

      reconsider i0 = 0 as Element of BOOLEAN by MARGREL1:def 11, TARSKI:def 2;

      reconsider Z0 = <*i0*> as FinSequence of BOOLEAN ;

      ( len Z0) = 1 by FINSEQ_1: 40;

      then

      reconsider Z0 = <* 0 *> as Tuple of 1, BOOLEAN ;

      

       TT1: S = (( carry (x,y)) ^ Z1);

      

       TT2: x1 = (x ^ Z0) by AS;

      

       TT3: y1 = (y ^ Z0) by AS;

      

       A20: (S /. 1) = FALSE

      proof

        1 <= K by NAT_1: 25;

        then 1 in ( Seg K) by FINSEQ_1: 1;

        then 1 in ( dom ( carry (x,y))) by XR0, FINSEQ_1:def 3;

        hence (S /. 1) = FALSE by A1, TT1, FINSEQ_4: 68;

      end;

      K in ( dom x) by XX3, X3, FINSEQ_1:def 3;

      then

       T3: (x1 /. K) = (x /. K) by TT2, FINSEQ_4: 68;

      K in ( dom y) by XX3, X3, FINSEQ_1:def 3;

      then

       T4: (y1 /. K) = (y /. K) by TT3, FINSEQ_4: 68;

      K in ( dom ( carry (x,y))) by PXR1, XR0, FINSEQ_1:def 3;

      then

       T2: (S /. K) = (( carry (x,y)) /. K) by TT1, FINSEQ_4: 68;

      

       A2: for i be Nat st 1 <= i & i < K1 holds (S /. (i + 1)) = ((((x1 /. i) '&' (y1 /. i)) 'or' ((x1 /. i) '&' (S /. i))) 'or' ((y1 /. i) '&' (S /. i)))

      proof

        let i be Nat;

        assume

         AS11: 1 <= i & i < K1;

        per cases ;

          suppose

           SXX1: not i < K;

          i <= K by NAT_1: 13, AS11;

          then

           XX: i = K by SXX1, XXREAL_0: 1;

          

          then (S /. (i + 1)) = i1 by FINSEQ_4: 67, XR0

          .= 1;

          hence (S /. (i + 1)) = ((((x1 /. i) '&' (y1 /. i)) 'or' ((x1 /. i) '&' (S /. i))) 'or' ((y1 /. i) '&' (S /. i))) by PX1, XX, T2, T3, T4, BINARITH:def 6;

        end;

          suppose

           C1: i < K;

          then

           C2: i in ( Seg K) by AS11, FINSEQ_1: 1;

          then i in ( dom ( carry (x,y))) by XR0, FINSEQ_1:def 3;

          then

           T2: (S /. i) = (( carry (x,y)) /. i) by TT1, FINSEQ_4: 68;

          i in ( dom x) by C2, X3, FINSEQ_1:def 3;

          then

           T3: (x1 /. i) = (x /. i) by TT2, FINSEQ_4: 68;

          i in ( dom y) by C2, X3, FINSEQ_1:def 3;

          then

           T4: (y1 /. i) = (y /. i) by TT3, FINSEQ_4: 68;

          

           T5: (i + 1) <= K by C1, NAT_1: 13;

          (1 + 0 ) <= (i + 1) by XREAL_1: 7;

          then (i + 1) in ( Seg K) by T5, FINSEQ_1: 1;

          then (i + 1) in ( dom ( carry (x,y))) by XR0, FINSEQ_1:def 3;

          

          hence (S /. (i + 1)) = (( carry (x,y)) /. (i + 1)) by TT1, FINSEQ_4: 68

          .= ((((x1 /. i) '&' (y1 /. i)) 'or' ((x1 /. i) '&' (S /. i))) 'or' ((y1 /. i) '&' (S /. i))) by T2, T3, T4, C1, AS11, BINARITH:def 2;

        end;

      end;

      then

       T1: S = ( carry (x1,y1)) by A20, BINARITH:def 2;

      K in ( dom ( carry (x,y))) by PXR1, XR0, FINSEQ_1:def 3;

      then

       T2: (S /. K) = (( carry (x,y)) /. K) by TT1, FINSEQ_4: 68;

      

       T6: ( len (x1 + y1)) = K1 by CARD_1:def 7;

      

       X2: 1 <= K by NAT_1: 25;

      ((x1 + y1) /. ( len (x1 + y1))) = (((x1 /. ( len (x1 + y1))) 'xor' (y1 /. ( len (x1 + y1)))) 'xor' (( carry (x1,y1)) /. ( len (x1 + y1)))) by BINARITH:def 5, P3

      .= 1 by R2, R0, L2, L0, X2, T1, T6, NAT_1: 16, X1, T2, T3, T4, A2;

      hence thesis by PP5, PARTFUN1:def 6;

    end;

    definition

      let x,y be Element of ( BOOLEAN * );

      :: BINARI_6:def5

      func x + y -> Element of ( BOOLEAN * ) equals

      : Def3: y if ( len x) = 0 ,

x if ( len y) = 0 ,

(( ExtBit (x,( LenMax (x,y)))) + ( ExtBit (y,( LenMax (x,y))))) if (( ExtBit (x,( LenMax (x,y)))),( ExtBit (y,( LenMax (x,y))))) are_summable & ( len x) <> 0 & ( len y) <> 0

      otherwise (( ExtBit (x,(( LenMax (x,y)) + 1))) + ( ExtBit (y,(( LenMax (x,y)) + 1))));

      coherence by FINSEQ_1:def 11;

      consistency ;

    end

    definition

      let F be Function of NAT , ( BOOLEAN * );

      let x be Element of NAT ;

      :: original: .

      redefine

      func F . x -> Element of ( BOOLEAN * ) ;

      correctness by FUNCT_2: 5;

    end

    theorem :: BINARI_6:25

    

     LM0710: for x be Element of ( BOOLEAN * ) st x in ( rng Nat2BL ) holds 1 <= ( len x)

    proof

      let x be Element of ( BOOLEAN * );

      assume x in ( rng Nat2BL );

      then

      consider L be Element of NAT such that

       H5: x = ( Nat2BL . L) by FUNCT_2: 113;

      x = (( LenBSeq L) -BinarySequence L) by Def2, H5;

      then 0 <> ( len x);

      then 0 < ( len x);

      then (1 + 0 ) <= ( len x) by NAT_1: 13;

      hence thesis;

    end;

    theorem :: BINARI_6:26

    

     LM071: for x,y be Element of ( BOOLEAN * ) st x in ( rng Nat2BL ) & y in ( rng Nat2BL ) holds (x + y) in ( rng Nat2BL )

    proof

      let x,y be Element of ( BOOLEAN * );

      assume

       AS1: x in ( rng Nat2BL ) & y in ( rng Nat2BL );

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

      then

       PP1: (ex x0 be Element of ( BOOLEAN * ) st x = x0 & (x0 . ( len x0)) = 1) or x in { <* 0 *>};

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

      then (ex y0 be Element of ( BOOLEAN * ) st y = y0 & (y0 . ( len y0)) = 1) or y in { <* 0 *>};

      per cases by PP1, TARSKI:def 1;

        suppose x = <* 0 *> or y = <* 0 *>;

        per cases ;

          suppose

           C1: x = <* 0 *>;

          then

          reconsider z = x as Tuple of 1, BOOLEAN ;

          

           P1: ( len x) = 1 by FINSEQ_1: 40, C1;

          

           P2: 1 <= ( len y) by LM0710, AS1;

          

           P30: ( len x) <> 0 & ( len y) <> 0 by LM0710, AS1;

          

          then

           P3: ( LenMax (x,y)) = ( max (( len x),( len y))) by Def15

          .= ( len y) by P1, XXREAL_0:def 10, LM0710, AS1;

          

           P6: (( len y) -' ( len y)) = (( len y) - ( len y)) by XREAL_0:def 2

          .= 0 ;

          

           P7: (( len y) -' ( len x)) = (( len y) - 1) by XREAL_0:def 2, XREAL_1: 48, P1, P2;

          set x1 = ( ExtBit (x,( LenMax (x,y))));

          set y1 = ( ExtBit (y,( LenMax (x,y))));

          

           P4: x1 = (x ^ ( 0* (( len y) -' ( len x)))) by P1, P3, Def20, LM0710, AS1;

          

           P5: y1 = (y ^ ( 0* 0 )) by P6, P3, Def20

          .= y by FINSEQ_1: 34;

          set K1 = ( LenMax (x,y));

          reconsider K = (K1 - 1) as Nat by P2, P3, INT_1: 5, ORDINAL1:def 12;

          

           P6: x1 = ( 0* ((( len y) -' ( len x)) + 1)) by LM0020, P4, C1, FINSEQ_2: 123

          .= ( 0* K1) by P3, P7;

          (( carry (x1,y1)) /. K1) = 0 by P6, LMExtBit3;

          then ((((x1 /. K1) '&' (y1 /. K1)) 'or' ((x1 /. K1) '&' (( carry (x1,y1)) /. K1))) 'or' ((y1 /. K1) '&' (( carry (x1,y1)) /. K1))) = 0 by P6, LMExtBit4;

          then ( add_ovfl (x1,y1)) = FALSE by BINARITH:def 6;

          then (x + y) = (x1 + y1) by Def3, P30, BINARITH:def 7;

          hence (x + y) in ( rng Nat2BL ) by AS1, LMExtBit5, P6, P5;

        end;

          suppose

           C1: y = <* 0 *>;

          then

          reconsider z = y as Tuple of 1, BOOLEAN ;

          

           P1: ( len y) = 1 by FINSEQ_1: 40, C1;

          

           P2: 1 <= ( len x) by LM0710, AS1;

          

           P30: ( len x) <> 0 & ( len y) <> 0 by LM0710, AS1;

          

          then

           P3: ( LenMax (x,y)) = ( max (( len x),( len y))) by Def15

          .= ( len x) by P1, XXREAL_0:def 10, LM0710, AS1;

          

           P6: (( len x) -' ( len x)) = (( len x) - ( len x)) by XREAL_0:def 2

          .= 0 ;

          

           P7: (( len x) -' ( len y)) = (( len x) - 1) by XREAL_0:def 2, XREAL_1: 48, P1, P2;

          set x1 = ( ExtBit (x,( LenMax (x,y))));

          set y1 = ( ExtBit (y,( LenMax (x,y))));

          

           P4: y1 = (y ^ ( 0* (( len x) -' ( len y)))) by P1, P3, Def20, LM0710, AS1;

          

           P5: x1 = (x ^ ( 0* 0 )) by P6, P3, Def20

          .= x by FINSEQ_1: 34;

          set K1 = ( LenMax (x,y));

          reconsider K = (K1 - 1) as Nat by P2, P3, INT_1: 5, ORDINAL1:def 12;

          

           P6: y1 = ( 0* ((( len x) -' ( len y)) + 1)) by LM0020, P4, C1, FINSEQ_2: 123

          .= ( 0* K1) by P3, P7;

          (( carry (x1,y1)) /. K1) = 0 by P6, LMExtBit3;

          then ((((x1 /. K1) '&' (y1 /. K1)) 'or' ((x1 /. K1) '&' (( carry (x1,y1)) /. K1))) 'or' ((y1 /. K1) '&' (( carry (x1,y1)) /. K1))) = 0 by P6, LMExtBit4;

          then ( add_ovfl (x1,y1)) = FALSE by BINARITH:def 6;

          then (x + y) = (x1 + y1) by Def3, P30, BINARITH:def 7;

          hence (x + y) in ( rng Nat2BL ) by AS1, LMExtBit5, P6, P5;

        end;

      end;

        suppose

         Y1: (x . ( len x)) = 1 & (y . ( len y)) = 1;

        

         X1: ( len x) <> 0 & ( len y) <> 0

        proof

          assume ( len x) = 0 or ( len y) = 0 ;

          then x = {} or y = {} ;

          hence contradiction by Y1;

        end;

        ((x + y) . ( len (x + y))) = 1

        proof

          per cases ;

            suppose

             C1: (( ExtBit (x,( LenMax (x,y)))),( ExtBit (y,( LenMax (x,y))))) are_summable ;

            then

             C2: (x + y) = (( ExtBit (x,( LenMax (x,y)))) + ( ExtBit (y,( LenMax (x,y))))) by X1, Def3;

            set x1 = ( ExtBit (x,( LenMax (x,y))));

            set y1 = ( ExtBit (y,( LenMax (x,y))));

            ( len x) <> ( len y)

            proof

              assume

               C10: ( len x) = ( len y);

              

               C11: ( LenMax (x,y)) = ( max (( len x),( len y))) by X1, Def15

              .= ( len y) by C10;

              ( LenMax (x,y)) = ( max (( len x),( len y))) by X1, Def15

              .= ( len x) by C10;

              then x1 = x & y1 = y by LMExtBit8, C11;

              hence contradiction by C1, LMExtBit9, Y1;

            end;

            per cases by XXREAL_0: 1;

              suppose

               C11: ( len x) < ( len y);

              ( LenMax (x,y)) = ( max (( len x),( len y))) by X1, Def15

              .= ( len y) by C11, XXREAL_0:def 10;

              then y1 = y by LMExtBit8;

              hence ((x + y) . ( len (x + y))) = 1 by Y1, C1, LMExtBit6, C2;

            end;

              suppose

               C11: ( len y) < ( len x);

              ( LenMax (x,y)) = ( max (( len x),( len y))) by X1, Def15

              .= ( len x) by C11, XXREAL_0:def 10;

              then x1 = x by LMExtBit8;

              hence ((x + y) . ( len (x + y))) = 1 by C2, C1, LMExtBit6, Y1;

            end;

          end;

            suppose

             C12: not (( ExtBit (x,( LenMax (x,y)))),( ExtBit (y,( LenMax (x,y))))) are_summable ;

            then

             C13: (x + y) = (( ExtBit (x,(( LenMax (x,y)) + 1))) + ( ExtBit (y,(( LenMax (x,y)) + 1)))) by X1, Def3;

            set Nx = ( ExtBit (x,( LenMax (x,y))));

            set Ny = ( ExtBit (y,( LenMax (x,y))));

            set Nx1 = ( ExtBit (x,(( LenMax (x,y)) + 1)));

            set Ny1 = ( ExtBit (y,(( LenMax (x,y)) + 1)));

            

             C16: ( LenMax (x,y)) = ( max (( len x),( len y))) by X1, Def15;

            then

             C14: Nx1 = (Nx ^ <* 0 *>) by LMExtBit1, XXREAL_0: 25;

            Ny1 = (Ny ^ <* 0 *>) by C16, LMExtBit1, XXREAL_0: 25;

            hence ((x + y) . ( len (x + y))) = 1 by C13, C12, C14, LMExtBit7;

          end;

        end;

        then (x + y) in { y where y be Element of ( BOOLEAN * ) : (y . ( len y)) = 1 } or (x + y) in { <* 0 *>};

        hence (x + y) in ( rng Nat2BL ) by LM031, XBOOLE_0:def 3;

      end;

    end;

    theorem :: BINARI_6:27

    

     LM080: for n be non zero Nat, x be Tuple of n, BOOLEAN holds for m,l be Nat, y be Tuple of l, BOOLEAN st y = (x ^ ( 0* m)) holds ( Absval y) = ( Absval x)

    proof

      let n be non zero Nat;

      let x be Tuple of n, BOOLEAN ;

      defpred P[ Nat] means for l be Nat, y be Tuple of l, BOOLEAN st y = (x ^ ( 0* $1)) holds ( Absval y) = ( Absval x);

      

       A1: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume

         A2: for l be Nat, y be Tuple of l, BOOLEAN st y = (x ^ ( 0* m)) holds ( Absval y) = ( Absval x);

        let l be Nat, y be Tuple of l, BOOLEAN ;

        assume

         A3: y = (x ^ ( 0* (m + 1)));

        ( 0* m) in ( BOOLEAN * ) by BINARI_3: 4;

        then

        reconsider z = ( 0* m) as Tuple of m, BOOLEAN by FINSEQ_1:def 11;

        (x ^ z) is Tuple of (n + m), BOOLEAN ;

        then

        reconsider y1 = (x ^ ( 0* m)) as Tuple of (n + m), BOOLEAN ;

        ( 0* (m + 1)) = (( 0* m) ^ <* FALSE *>) by FINSEQ_2: 60;

        then

         A4: y = (y1 ^ <* FALSE *>) by FINSEQ_1: 32, A3;

        

         X1: ( len y) = l by CARD_1:def 7;

        ( len (y1 ^ <* FALSE *>)) = (( len y1) + ( len <* FALSE *>)) by FINSEQ_1: 22

        .= (( len y1) + 1) by FINSEQ_1: 40

        .= ((n + m) + 1) by CARD_1:def 7;

        

        hence ( Absval y) = (( Absval y1) + ( IFEQ ( FALSE , FALSE , 0 ,(2 to_power (n + m))))) by X1, BINARITH: 20, A4

        .= (( Absval x) + ( IFEQ ( FALSE , FALSE , 0 ,(2 to_power (n + m))))) by A2

        .= (( Absval x) + 0 ) by FUNCOP_1:def 8

        .= ( Absval x);

      end;

      

       A0: P[ 0 ]

      proof

        let l be Nat, y be Tuple of l, BOOLEAN ;

        assume

         AS2: y = (x ^ ( 0* 0 ));

        

         A3: (x ^ ( 0* 0 )) = x by FINSEQ_1: 34;

        x is Tuple of l, BOOLEAN by FINSEQ_1: 34, AS2;

        then ( len x) = l by CARD_1:def 7;

        hence ( Absval y) = ( Absval x) by A3, AS2, CARD_1:def 7;

      end;

      for m be Nat holds P[m] from NAT_1:sch 2( A0, A1);

      hence thesis;

    end;

    theorem :: BINARI_6:28

    

     LM090: for n be Nat, x be Element of NAT , y be Tuple of n, BOOLEAN st y = ( Nat2BL . x) holds n = ( LenBSeq x) & ( Absval y) = x & ( Nat2BL . ( Absval y)) = y

    proof

      let n be Nat, x be Element of NAT , y be Tuple of n, BOOLEAN ;

      assume

       AS: y = ( Nat2BL . x);

      

       A1: ( Nat2BL . x) = (( LenBSeq x) -BinarySequence x) by Def2;

      

       A3: x < (2 to_power ( LenBSeq x)) by LM006;

      ( len y) = ( LenBSeq x) by CARD_1:def 7, AS, A1;

      hence n = ( LenBSeq x) by CARD_1:def 7;

      hence thesis by A3, BINARI_3: 35, A1, AS;

    end;

    theorem :: BINARI_6:29

    

     LM100: for x,y be Element of NAT holds ( Nat2BL . (x + y)) = (( Nat2BL . x) + ( Nat2BL . y))

    proof

      let x,y be Element of NAT ;

      (x + y) is Element of NAT by ORDINAL1:def 12;

      then ( Nat2BL . (x + y)) = (( LenBSeq (x + y)) -BinarySequence (x + y)) by Def2;

      then

      reconsider adxy = ( Nat2BL . (x + y)) as Tuple of ( LenBSeq (x + y)), BOOLEAN ;

      set Nx = ( Nat2BL . x);

      set Ny = ( Nat2BL . y);

      

       PX2: Nx = (( LenBSeq x) -BinarySequence x) by Def2;

      

       PA3: Ny = (( LenBSeq y) -BinarySequence y) by Def2;

      then

       A3: ( len Nx) <> 0 & ( len Ny) <> 0 by PX2;

      

       B1: Nx = (( LenBSeq x) -BinarySequence x) by Def2;

      

       B2: Ny = (( LenBSeq y) -BinarySequence y) by Def2;

      

       H1: Nx in ( rng Nat2BL ) by FUNCT_2: 4;

      

       PH3: Ny in ( rng Nat2BL ) by FUNCT_2: 4;

      

       PD0: ( LenMax (Nx,Ny)) = ( max (( len Nx),( len Ny))) by PA3, Def15, PX2;

      then ( len Nx) <= ( LenMax (Nx,Ny)) & ( len Ny) <= ( LenMax (Nx,Ny)) by XXREAL_0: 25;

      then

       E0: (( len Nx) + 0 ) <= (( LenMax (Nx,Ny)) + 1) & (( len Ny) + 0 ) <= (( LenMax (Nx,Ny)) + 1) by XREAL_1: 7;

      per cases ;

        suppose

         C1: (( ExtBit (Nx,( LenMax (Nx,Ny)))),( ExtBit (Ny,( LenMax (Nx,Ny))))) are_summable ;

        then

         C2: (Nx + Ny) = (( ExtBit (Nx,( LenMax (Nx,Ny)))) + ( ExtBit (Ny,( LenMax (Nx,Ny))))) by Def3, A3;

        set ENx = ( ExtBit (Nx,( LenMax (Nx,Ny))));

        set ENy = ( ExtBit (Ny,( LenMax (Nx,Ny))));

        

         D1: ENx = (Nx ^ ( 0* (( LenMax (Nx,Ny)) -' ( len Nx)))) by Def20, PD0, XXREAL_0: 25;

        

         D2: ENy = (Ny ^ ( 0* (( LenMax (Nx,Ny)) -' ( len Ny)))) by Def20, PD0, XXREAL_0: 25;

        

         A4: x = ( Absval (( LenBSeq x) -BinarySequence x)) by LM007

        .= ( Absval ENx) by LM080, B1, D1;

        y = ( Absval (( LenBSeq y) -BinarySequence y)) by LM007

        .= ( Absval ENy) by LM080, B2, D2;

        then

         A6: ( Nat2BL . ( Absval (ENx + ENy))) = ( Nat2BL . (x + y)) by A4, C1, BINARITH: 22;

        consider L be Element of NAT such that

         H5: (ENx + ENy) = ( Nat2BL . L) by FUNCT_2: 113, PH3, C2, LM071, H1;

        thus ( Nat2BL . (x + y)) = (( Nat2BL . x) + ( Nat2BL . y)) by A6, C2, LM090, H5;

      end;

        suppose not (( ExtBit (Nx,( LenMax (Nx,Ny)))),( ExtBit (Ny,( LenMax (Nx,Ny))))) are_summable ;

        then

         C2: (Nx + Ny) = (( ExtBit (Nx,(( LenMax (Nx,Ny)) + 1))) + ( ExtBit (Ny,(( LenMax (Nx,Ny)) + 1)))) by Def3, A3;

        set ENx = ( ExtBit (Nx,(( LenMax (Nx,Ny)) + 1)));

        set ENy = ( ExtBit (Ny,(( LenMax (Nx,Ny)) + 1)));

        

         XX1: ENx = (( ExtBit (Nx,( LenMax (Nx,Ny)))) ^ <* 0 *>) by PD0, LMExtBit1, XXREAL_0: 25;

        

         XX2: ENy = (( ExtBit (Ny,( LenMax (Nx,Ny)))) ^ <* 0 *>) by PD0, LMExtBit1, XXREAL_0: 25;

        

         D1: ENx = (Nx ^ ( 0* ((( LenMax (Nx,Ny)) + 1) -' ( len Nx)))) by Def20, E0;

        

         D2: ENy = (Ny ^ ( 0* ((( LenMax (Nx,Ny)) + 1) -' ( len Ny)))) by Def20, E0;

        

         A4: x = ( Absval (( LenBSeq x) -BinarySequence x)) by LM007

        .= ( Absval ENx) by LM080, B1, D1;

        y = ( Absval (( LenBSeq y) -BinarySequence y)) by LM007

        .= ( Absval ENy) by LM080, B2, D2;

        then

         A6: ( Nat2BL . ( Absval (ENx + ENy))) = ( Nat2BL . (x + y)) by A4, BINARITH: 22, XX1, XX2, LMExtBit2;

        consider L be Element of NAT such that

         H5: (ENx + ENy) = ( Nat2BL . L) by FUNCT_2: 113, PH3, C2, LM071, H1;

        thus ( Nat2BL . (x + y)) = (( Nat2BL . x) + ( Nat2BL . y)) by A6, C2, LM090, H5;

      end;

    end;

    theorem :: BINARI_6:30

    for x,y be Element of ( BOOLEAN * ) st x in ( rng Nat2BL ) & y in ( rng Nat2BL ) holds (x + y) = (y + x)

    proof

      let x,y be Element of ( BOOLEAN * );

      assume

       AS: x in ( rng Nat2BL ) & y in ( rng Nat2BL );

      then

      consider n be Element of NAT such that

       A1: x = ( Nat2BL . n) by FUNCT_2: 113;

      consider m be Element of NAT such that

       A2: y = ( Nat2BL . m) by AS, FUNCT_2: 113;

      

      thus (x + y) = ( Nat2BL . (n + m)) by A1, A2, LM100

      .= (y + x) by A1, A2, LM100;

    end;

    theorem :: BINARI_6:31

    for x,y,z be Element of ( BOOLEAN * ) st x in ( rng Nat2BL ) & y in ( rng Nat2BL ) & z in ( rng Nat2BL ) holds ((x + y) + z) = (x + (y + z))

    proof

      let x,y,z be Element of ( BOOLEAN * );

      assume

       AS: x in ( rng Nat2BL ) & y in ( rng Nat2BL ) & z in ( rng Nat2BL );

      then

      consider n be Element of NAT such that

       A1: x = ( Nat2BL . n) by FUNCT_2: 113;

      consider m be Element of NAT such that

       A2: y = ( Nat2BL . m) by AS, FUNCT_2: 113;

      consider k be Element of NAT such that

       A3: z = ( Nat2BL . k) by AS, FUNCT_2: 113;

      reconsider nm = (n + m) as Element of NAT by ORDINAL1:def 12;

      reconsider mk = (m + k) as Element of NAT by ORDINAL1:def 12;

      

      thus ((x + y) + z) = (( Nat2BL . nm) + ( Nat2BL . k)) by LM100, A1, A2, A3

      .= ( Nat2BL . ((n + m) + k)) by LM100

      .= ( Nat2BL . (n + mk))

      .= (( Nat2BL . n) + ( Nat2BL . mk)) by LM100

      .= (x + (y + z)) by A1, A2, A3, LM100;

    end;

    begin

    definition

      let x be Element of ( BOOLEAN * );

      :: BINARI_6:def6

      func ExAbsval (x) -> Nat means

      : Def100: ex n be Nat, y be Tuple of n, BOOLEAN st y = x & it = ( Absval y);

      existence

      proof

        thus ex IT be Nat st ex n be Nat, y be Tuple of n, BOOLEAN st y = x & IT = ( Absval y)

        proof

          reconsider n = ( len x) as Nat;

          reconsider y = x as Tuple of n, BOOLEAN by CARD_1:def 7;

          take IT = ( Absval y);

          thus ex n be Nat, y be Tuple of n, BOOLEAN st y = x & IT = ( Absval y);

        end;

      end;

      uniqueness

      proof

        let N1,N2 be Nat;

        thus (ex n be Nat, y be Tuple of n, BOOLEAN st y = x & N1 = ( Absval y)) & (ex n be Nat, y be Tuple of n, BOOLEAN st y = x & N2 = ( Absval y)) implies N1 = N2

        proof

          assume that

           A2: (ex n be Nat, y be Tuple of n, BOOLEAN st y = x & N1 = ( Absval y)) and

           A3: (ex n be Nat, y be Tuple of n, BOOLEAN st y = x & N2 = ( Absval y));

          consider n1 be Nat, y1 be Tuple of n1, BOOLEAN such that

           A4: y1 = x & N1 = ( Absval y1) by A2;

          consider n2 be Nat, y2 be Tuple of n2, BOOLEAN such that

           A5: y2 = x & N2 = ( Absval y2) by A3;

          n1 = ( len y1) by CARD_1:def 7

          .= n2 by CARD_1:def 7, A4, A5;

          hence N1 = N2 by A4, A5;

        end;

      end;

    end

    

     D100: for x be Element of ( BOOLEAN * ) st ( len x) = 0 holds ( ExAbsval x) = 0

    proof

      let x be Element of ( BOOLEAN * );

      consider n be Nat, y be Tuple of n, BOOLEAN such that

       y: y = x & ( ExAbsval x) = ( Absval y) by Def100;

      assume ( len x) = 0 ;

      then n = 0 by y;

      then

       lb: ( len ( Binary y)) = 0 ;

      

      thus ( ExAbsval x) = ( Absval y) by y

      .= ( addnat $$ ( Binary y)) by BINARITH:def 4

      .= ( the_unity_wrt addnat ) by lb, FINSOP_1:def 1

      .= 0 by BINOP_2: 5;

    end;

    theorem :: BINARI_6:32

    

     LM210: ex F be Function of ( BOOLEAN * ), NAT st for x be Element of ( BOOLEAN * ) holds (F . x) = ( ExAbsval x)

    proof

      defpred P[ Element of ( BOOLEAN * ), object] means $2 = ( ExAbsval $1);

      

       A1: for x be Element of ( BOOLEAN * ) holds ex y be Element of NAT st P[x, y]

      proof

        let x be Element of ( BOOLEAN * );

        set y = ( ExAbsval x);

        reconsider y as Element of NAT by ORDINAL1:def 12;

        take y;

        thus thesis;

      end;

      consider f be Function of ( BOOLEAN * ), NAT such that

       A2: for x be Element of ( BOOLEAN * ) holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

      take f;

      thus thesis by A2;

    end;

    definition

      :: BINARI_6:def7

      func BL2Nat -> Function of ( BOOLEAN * ), NAT means

      : Def110: for x be Element of ( BOOLEAN * ) holds (it . x) = ( ExAbsval x);

      existence by LM210;

      uniqueness

      proof

        let f1,f2 be Function of ( BOOLEAN * ), NAT ;

        assume that

         AS1: for x be Element of ( BOOLEAN * ) holds (f1 . x) = ( ExAbsval x) and

         AS2: for x be Element of ( BOOLEAN * ) holds (f2 . x) = ( ExAbsval x);

        for x be Element of ( BOOLEAN * ) holds (f1 . x) = (f2 . x)

        proof

          let x be Element of ( BOOLEAN * );

          

          thus (f1 . x) = ( ExAbsval x) by AS1

          .= (f2 . x) by AS2;

        end;

        hence f1 = f2 by FUNCT_2:def 8;

      end;

    end

    definition

      let F be Function of ( BOOLEAN * ), NAT ;

      let x be Element of ( BOOLEAN * );

      :: original: .

      redefine

      func F . x -> Element of NAT ;

      correctness by FUNCT_2: 5;

    end

    

     LM220: for F be Function of ( BOOLEAN * ), NAT st for x be Element of ( BOOLEAN * ) holds (F . x) = ( ExAbsval x) holds F is onto

    proof

      let f be Function of ( BOOLEAN * ), NAT ;

      assume

       AS1: for x be Element of ( BOOLEAN * ) holds (f . x) = ( ExAbsval x);

      for y be object st y in NAT holds ex x be object st x in ( BOOLEAN * ) & y = (f . x)

      proof

        let y be object;

        assume y in NAT ;

        then

        reconsider k = y as Nat;

        per cases ;

          suppose

           C1: k = 0 ;

          reconsider x = ( <*> BOOLEAN ) as Element of ( BOOLEAN * ) by FINSEQ_1:def 11;

          ( len x) = 0 ;

          then ( ExAbsval x) = 0 by D100;

          then y = (f . x) by AS1, C1;

          hence thesis;

        end;

          suppose k <> 0 ;

          then

          consider n be Nat such that

           A1: (2 to_power n) <= k & k < (2 to_power (n + 1)) by LM001;

          set xn = ((n + 1) -BinarySequence k);

          reconsider x = xn as Element of ( BOOLEAN * ) by FINSEQ_1:def 11;

          ( ExAbsval x) = ( Absval xn) by Def100

          .= k by A1, BINARI_3: 35;

          then y = (f . x) by AS1;

          hence thesis;

        end;

      end;

      then ( rng f) = NAT by FUNCT_2: 10;

      hence thesis by FUNCT_2:def 3;

    end;

    registration

      cluster BL2Nat -> onto;

      coherence

      proof

        for x be Element of ( BOOLEAN * ) holds ( BL2Nat . x) = ( ExAbsval x) by Def110;

        hence thesis by LM220;

      end;

    end

    theorem :: BINARI_6:33

    

     LM230: for x be Element of ( BOOLEAN * ), K be Nat st ( len x) <> 0 & ( len x) <= K holds ( ExAbsval x) = ( Absval ( ExtBit (x,K)))

    proof

      let x be Element of ( BOOLEAN * ), K be Nat;

      assume

       AS: ( len x) <> 0 & ( len x) <= K;

      then

      reconsider n = ( len x) as non zero Nat;

      reconsider y = x as Tuple of n, BOOLEAN by CARD_1:def 7;

      ( ExtBit (x,K)) = (y ^ ( 0* (K -' ( len x)))) by AS, Def20;

      

      then ( Absval ( ExtBit (x,K))) = ( Absval y) by LM080

      .= ( ExAbsval x) by Def100;

      hence thesis;

    end;

    theorem :: BINARI_6:34

    

     LM240: for x,y be Element of ( BOOLEAN * ) holds ( BL2Nat . (x + y)) = (( BL2Nat . x) + ( BL2Nat . y))

    proof

      let x,y be Element of ( BOOLEAN * );

      

       XP1: ( BL2Nat . x) = ( ExAbsval x) by Def110;

      

       XP2: ( BL2Nat . y) = ( ExAbsval y) by Def110;

      set ENx = ( ExtBit (x,( LenMax (x,y))));

      set ENy = ( ExtBit (y,( LenMax (x,y))));

      set ENx1 = ( ExtBit (x,(( LenMax (x,y)) + 1)));

      set ENy1 = ( ExtBit (y,(( LenMax (x,y)) + 1)));

      per cases ;

        suppose

         C1: ( len x) = 0 ;

        

        hence ( BL2Nat . (x + y)) = ( 0 + ( BL2Nat . y)) by Def3

        .= (( BL2Nat . x) + ( BL2Nat . y)) by XP1, C1, D100;

      end;

        suppose

         C2: ( len y) = 0 ;

        

        hence ( BL2Nat . (x + y)) = (( BL2Nat . x) + 0 ) by Def3

        .= (( BL2Nat . x) + ( BL2Nat . y)) by XP2, C2, D100;

      end;

        suppose

         C3: (ENx,ENy) are_summable & ( len x) <> 0 & ( len y) <> 0 ;

        then

         C4: (x + y) = (ENx + ENy) by Def3;

        

         PXP3: ( LenMax (x,y)) = ( max (( len x),( len y))) by Def15, C3;

        

         XP7: ( BL2Nat . x) = ( ExAbsval x) by Def110

        .= ( Absval ENx) by PXP3, C3, LM230, XXREAL_0: 25;

        

         XP8: ( BL2Nat . y) = ( ExAbsval y) by Def110

        .= ( Absval ENy) by PXP3, C3, LM230, XXREAL_0: 25;

        

         XP15: ( ExAbsval (x + y)) = ( Absval (ENx + ENy)) by C4, Def100;

        

        thus ( BL2Nat . (x + y)) = ( ExAbsval (x + y)) by Def110

        .= (( BL2Nat . x) + ( BL2Nat . y)) by XP7, XP8, C3, BINARITH: 22, XP15;

      end;

        suppose

         C3: ( not (ENx,ENy) are_summable ) & ( len x) <> 0 & ( len y) <> 0 ;

        then

         C4: (x + y) = (ENx1 + ENy1) by Def3;

        

         PXP3: ( LenMax (x,y)) = ( max (( len x),( len y))) by Def15, C3;

        then ( len x) <= ( LenMax (x,y)) & ( len y) <= ( LenMax (x,y)) by XXREAL_0: 25;

        then

         XP5: (( len x) + 0 ) <= (( LenMax (x,y)) + 1) & (( len y) + 0 ) <= (( LenMax (x,y)) + 1) by XREAL_1: 7;

        

         XP9: ( BL2Nat . x) = ( ExAbsval x) by Def110

        .= ( Absval ENx1) by XP5, C3, LM230;

        

         XP10: ( BL2Nat . y) = ( ExAbsval y) by Def110

        .= ( Absval ENy1) by XP5, C3, LM230;

        

         XX1: ENx1 = (( ExtBit (x,( LenMax (x,y)))) ^ <* 0 *>) by PXP3, LMExtBit1, XXREAL_0: 25;

        

         XX2: ENy1 = (( ExtBit (y,( LenMax (x,y)))) ^ <* 0 *>) by PXP3, LMExtBit1, XXREAL_0: 25;

        

         XP15: ( ExAbsval (x + y)) = ( Absval (ENx1 + ENy1)) by C4, Def100;

        

        thus ( BL2Nat . (x + y)) = ( ExAbsval (x + y)) by Def110

        .= (( BL2Nat . x) + ( BL2Nat . y)) by XP9, XP10, BINARITH: 22, XP15, XX1, XX2, LMExtBit2;

      end;

    end;

    definition

      :: BINARI_6:def8

      func EqBL2Nat -> Equivalence_Relation of ( BOOLEAN * ) means

      : Def300: for x,y be object holds ( [x, y] in it iff (x in ( BOOLEAN * ) & y in ( BOOLEAN * ) & ( BL2Nat . x) = ( BL2Nat . y)));

      existence

      proof

        defpred P1[ object, object] means ( BL2Nat . $1) = ( BL2Nat . $2);

        

         A1: for x be object st x in ( BOOLEAN * ) holds P1[x, x];

        

         A2: for x,y be object st P1[x, y] holds P1[y, x];

        

         A3: for x,y,z be object st P1[x, y] & P1[y, z] holds P1[x, z];

        consider EqR be Equivalence_Relation of ( BOOLEAN * ) such that

         A4: for x,y be object holds ( [x, y] in EqR iff (x in ( BOOLEAN * ) & y in ( BOOLEAN * ) & P1[x, y])) from EQREL_1:sch 1( A1, A2, A3);

        thus thesis by A4;

      end;

      uniqueness

      proof

        let EqR1,EqR2 be Equivalence_Relation of ( BOOLEAN * ) such that

         A1: for x,y be object holds ( [x, y] in EqR1 iff (x in ( BOOLEAN * ) & y in ( BOOLEAN * ) & ( BL2Nat . x) = ( BL2Nat . y))) and

         A2: for x,y be object holds ( [x, y] in EqR2 iff (x in ( BOOLEAN * ) & y in ( BOOLEAN * ) & ( BL2Nat . x) = ( BL2Nat . y)));

        for a,b be object holds ( [a, b] in EqR1 iff [a, b] in EqR2)

        proof

          let x,y be object;

           [x, y] in EqR1 iff (x in ( BOOLEAN * ) & y in ( BOOLEAN * ) & ( BL2Nat . x) = ( BL2Nat . y)) by A1;

          hence [x, y] in EqR1 iff [x, y] in EqR2 by A2;

        end;

        hence thesis;

      end;

    end

    definition

      :: BINARI_6:def9

      func QuBL2Nat -> Function of ( Class EqBL2Nat ), NAT means

      : Def400: for A be Element of ( Class EqBL2Nat ) holds ex x be object st x in A & (it . A) = ( BL2Nat . x);

      existence

      proof

        defpred P[ set, object] means ex x be object st x in $1 & $2 = ( BL2Nat . x);

        

         A1: for A be Element of ( Class EqBL2Nat ) holds ex y be Element of NAT st P[A, y]

        proof

          let A be Element of ( Class EqBL2Nat );

          A is Subset of ( BOOLEAN * ) by TARSKI:def 3;

          then

          consider x be object such that

           A2: x in ( BOOLEAN * ) & A = ( Class ( EqBL2Nat ,x)) by EQREL_1:def 3;

          reconsider y = x as Element of ( BOOLEAN * ) by A2;

          set z = ( BL2Nat . y);

          take z;

          thus thesis by A2, EQREL_1: 20;

        end;

        consider f be Function of ( Class EqBL2Nat ), NAT such that

         A2: for A be Element of ( Class EqBL2Nat ) holds P[A, (f . A)] from FUNCT_2:sch 3( A1);

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be Function of ( Class EqBL2Nat ), NAT ;

        assume

         AS1: for A be Element of ( Class EqBL2Nat ) holds ex x be object st x in A & (f1 . A) = ( BL2Nat . x);

        assume

         AS2: for A be Element of ( Class EqBL2Nat ) holds ex x be object st x in A & (f2 . A) = ( BL2Nat . x);

        for A be Element of ( Class EqBL2Nat ) holds (f1 . A) = (f2 . A)

        proof

          let A be Element of ( Class EqBL2Nat );

          consider x1 be object such that

           P1: x1 in A & (f1 . A) = ( BL2Nat . x1) by AS1;

          consider x2 be object such that

           P2: x2 in A & (f2 . A) = ( BL2Nat . x2) by AS2;

          A is Subset of ( BOOLEAN * ) by TARSKI:def 3;

          then

          consider x be object such that

           P3: x in ( BOOLEAN * ) & A = ( Class ( EqBL2Nat ,x)) by EQREL_1:def 3;

           [x1, x2] in EqBL2Nat by EQREL_1: 22, P1, P2, P3;

          hence thesis by P1, P2, Def300;

        end;

        hence f1 = f2 by FUNCT_2:def 8;

      end;

    end

    

     LemmaQU: QuBL2Nat is onto

    proof

      for y be object st y in NAT holds ex A be object st A in ( Class EqBL2Nat ) & y = ( QuBL2Nat . A)

      proof

        let y be object;

        assume

         A0: y in NAT ;

        then

        reconsider k = y as Nat;

        ( rng BL2Nat ) = NAT by FUNCT_2:def 3;

        then

        consider x be object such that

         A1: x in ( BOOLEAN * ) & y = ( BL2Nat . x) by FUNCT_2: 11, A0;

        reconsider A = ( Class ( EqBL2Nat ,x)) as Element of ( Class EqBL2Nat ) by EQREL_1:def 3, A1;

        consider x1 be object such that

         A2: x1 in A & ( QuBL2Nat . A) = ( BL2Nat . x1) by Def400;

         [x1, x] in EqBL2Nat by A2, EQREL_1: 19;

        then ( BL2Nat . x1) = ( BL2Nat . x) by Def300;

        hence thesis by A1, A2;

      end;

      then ( rng QuBL2Nat ) = NAT by FUNCT_2: 10;

      hence thesis by FUNCT_2:def 3;

    end;

    

     LM600: QuBL2Nat is one-to-one

    proof

      for A1,A2 be object st A1 in ( Class EqBL2Nat ) & A2 in ( Class EqBL2Nat ) & ( QuBL2Nat . A1) = ( QuBL2Nat . A2) holds A1 = A2

      proof

        let A1,A2 be object;

        assume

         P0: A1 in ( Class EqBL2Nat ) & A2 in ( Class EqBL2Nat ) & ( QuBL2Nat . A1) = ( QuBL2Nat . A2);

        consider z1 be object such that

         Q1: z1 in ( BOOLEAN * ) & A1 = ( Class ( EqBL2Nat ,z1)) by P0, EQREL_1:def 3;

        consider z2 be object such that

         Q2: z2 in ( BOOLEAN * ) & A2 = ( Class ( EqBL2Nat ,z2)) by P0, EQREL_1:def 3;

        reconsider A10 = A1, A20 = A2 as Element of ( Class EqBL2Nat ) by P0;

        

         D1: A10 is Subset of ( BOOLEAN * ) by TARSKI:def 3;

        

         D2: A20 is Subset of ( BOOLEAN * ) by TARSKI:def 3;

        consider x1 be object such that

         P1: x1 in A10 & ( QuBL2Nat . A10) = ( BL2Nat . x1) by Def400;

        reconsider x1 as Element of ( BOOLEAN * ) by D1, P1;

        

         R1: ( Class ( EqBL2Nat ,x1)) = ( Class ( EqBL2Nat ,z1)) by Q1, P1, EQREL_1: 23;

        consider x2 be object such that

         P2: x2 in A20 & ( QuBL2Nat . A20) = ( BL2Nat . x2) by Def400;

        reconsider x2 as Element of ( BOOLEAN * ) by D2, P2;

        

         R2: ( Class ( EqBL2Nat ,x2)) = ( Class ( EqBL2Nat ,z2)) by Q2, P2, EQREL_1: 23;

         [x1, x2] in EqBL2Nat by P1, P2, Def300, P0;

        hence A1 = A2 by EQREL_1: 35, R1, R2, Q1, Q2;

      end;

      hence thesis by FUNCT_2: 19;

    end;

    registration

      cluster QuBL2Nat -> one-to-one onto;

      coherence by LemmaQU, LM600;

    end

    theorem :: BINARI_6:35

    

     LM700: for x be Element of ( BOOLEAN * ) holds ( QuBL2Nat . ( Class ( EqBL2Nat ,x))) = ( BL2Nat . x)

    proof

      let x be Element of ( BOOLEAN * );

      reconsider A = ( Class ( EqBL2Nat ,x)) as Element of ( Class EqBL2Nat ) by EQREL_1:def 3;

      reconsider A0 = A as Subset of ( BOOLEAN * );

      consider x1 be object such that

       P1: x1 in A0 & ( QuBL2Nat . A0) = ( BL2Nat . x1) by Def400;

      reconsider x1 as Element of ( BOOLEAN * ) by P1;

      ( Class ( EqBL2Nat ,x1)) = ( Class ( EqBL2Nat ,x)) by P1, EQREL_1: 23;

      then [x1, x] in EqBL2Nat by EQREL_1: 35;

      hence thesis by P1, Def300;

    end;

    definition

      let A,B be Element of ( Class EqBL2Nat );

      :: BINARI_6:def10

      func A + B -> Element of ( Class EqBL2Nat ) means

      : Def500: ex x,y be Element of ( BOOLEAN * ) st x in A & y in B & it = ( Class ( EqBL2Nat ,(x + y)));

      existence

      proof

        

         P0: A in ( Class EqBL2Nat ) & B in ( Class EqBL2Nat );

        consider x be object such that

         Q1: x in ( BOOLEAN * ) & A = ( Class ( EqBL2Nat ,x)) by P0, EQREL_1:def 3;

        consider y be object such that

         Q2: y in ( BOOLEAN * ) & B = ( Class ( EqBL2Nat ,y)) by P0, EQREL_1:def 3;

        reconsider x, y as Element of ( BOOLEAN * ) by Q1, Q2;

        reconsider AB = ( Class ( EqBL2Nat ,(x + y))) as Element of ( Class EqBL2Nat ) by EQREL_1:def 3;

        take AB;

        

         X2: y in B by Q2, EQREL_1: 20;

        thus ex x,y be Element of ( BOOLEAN * ) st x in A & y in B & AB = ( Class ( EqBL2Nat ,(x + y))) by Q1, EQREL_1: 20, X2;

      end;

      uniqueness

      proof

        let AB1,AB2 be Element of ( Class EqBL2Nat ) such that

         P1: ex x,y be Element of ( BOOLEAN * ) st x in A & y in B & AB1 = ( Class ( EqBL2Nat ,(x + y))) and

         P2: ex x,y be Element of ( BOOLEAN * ) st x in A & y in B & AB2 = ( Class ( EqBL2Nat ,(x + y)));

        consider x1,y1 be Element of ( BOOLEAN * ) such that

         P3: x1 in A & y1 in B & AB1 = ( Class ( EqBL2Nat ,(x1 + y1))) by P1;

        consider x2,y2 be Element of ( BOOLEAN * ) such that

         P4: x2 in A & y2 in B & AB2 = ( Class ( EqBL2Nat ,(x2 + y2))) by P2;

        

         P0: A in ( Class EqBL2Nat ) & B in ( Class EqBL2Nat );

        consider x be object such that

         Q1: x in ( BOOLEAN * ) & A = ( Class ( EqBL2Nat ,x)) by P0, EQREL_1:def 3;

        consider y be object such that

         Q2: y in ( BOOLEAN * ) & B = ( Class ( EqBL2Nat ,y)) by P0, EQREL_1:def 3;

        reconsider x, y as Element of ( BOOLEAN * ) by Q1, Q2;

         [x1, x2] in EqBL2Nat by Q1, P3, P4, EQREL_1: 22;

        then

         R1: ( BL2Nat . x1) = ( BL2Nat . x2) by Def300;

         [y1, y2] in EqBL2Nat by Q2, P3, P4, EQREL_1: 22;

        then

         R2: ( BL2Nat . y1) = ( BL2Nat . y2) by Def300;

        ( BL2Nat . (x1 + y1)) = (( BL2Nat . x1) + ( BL2Nat . y1)) by LM240

        .= ( BL2Nat . (x2 + y2)) by LM240, R1, R2;

        then [(x1 + y1), (x2 + y2)] in EqBL2Nat by Def300;

        hence AB1 = AB2 by P3, P4, EQREL_1: 35;

      end;

    end

    theorem :: BINARI_6:36

    

     LM800: for A,B be Element of ( Class EqBL2Nat ), x,y be Element of ( BOOLEAN * ) st x in A & y in B holds (A + B) = ( Class ( EqBL2Nat ,(x + y)))

    proof

      let A,B be Element of ( Class EqBL2Nat ), x2,y2 be Element of ( BOOLEAN * );

      assume

       AS1: x2 in A & y2 in B;

      consider x1,y1 be Element of ( BOOLEAN * ) such that

       T1: x1 in A & y1 in B & (A + B) = ( Class ( EqBL2Nat ,(x1 + y1))) by Def500;

      

       P0: A in ( Class EqBL2Nat ) & B in ( Class EqBL2Nat );

      consider x be object such that

       Q1: x in ( BOOLEAN * ) & A = ( Class ( EqBL2Nat ,x)) by P0, EQREL_1:def 3;

      consider y be object such that

       Q2: y in ( BOOLEAN * ) & B = ( Class ( EqBL2Nat ,y)) by P0, EQREL_1:def 3;

      reconsider x, y as Element of ( BOOLEAN * ) by Q1, Q2;

       [x1, x2] in EqBL2Nat by Q1, AS1, T1, EQREL_1: 22;

      then

       R1: ( BL2Nat . x1) = ( BL2Nat . x2) by Def300;

       [y1, y2] in EqBL2Nat by Q2, AS1, T1, EQREL_1: 22;

      then

       R2: ( BL2Nat . y1) = ( BL2Nat . y2) by Def300;

      ( BL2Nat . (x1 + y1)) = (( BL2Nat . x1) + ( BL2Nat . y1)) by LM240

      .= ( BL2Nat . (x2 + y2)) by LM240, R1, R2;

      then [(x1 + y1), (x2 + y2)] in EqBL2Nat by Def300;

      hence thesis by T1, EQREL_1: 35;

    end;

    theorem :: BINARI_6:37

    for A,B be Element of ( Class EqBL2Nat ) holds ( QuBL2Nat . (A + B)) = (( QuBL2Nat . A) + ( QuBL2Nat . B))

    proof

      let A,B be Element of ( Class EqBL2Nat );

      

       P0: A in ( Class EqBL2Nat ) & B in ( Class EqBL2Nat );

      consider x be object such that

       Q1: x in ( BOOLEAN * ) & A = ( Class ( EqBL2Nat ,x)) by P0, EQREL_1:def 3;

      consider y be object such that

       Q2: y in ( BOOLEAN * ) & B = ( Class ( EqBL2Nat ,y)) by P0, EQREL_1:def 3;

      reconsider x, y as Element of ( BOOLEAN * ) by Q1, Q2;

      x in A & y in B by Q1, Q2, EQREL_1: 20;

      then (A + B) = ( Class ( EqBL2Nat ,(x + y))) by LM800;

      

      then

       R2: ( QuBL2Nat . (A + B)) = ( BL2Nat . (x + y)) by LM700

      .= (( BL2Nat . x) + ( BL2Nat . y)) by LM240;

      ( BL2Nat . x) = ( QuBL2Nat . A) by Q1, LM700;

      hence thesis by R2, Q2, LM700;

    end;

    theorem :: BINARI_6:38

    

     LM910: for A,B be Element of ( Class EqBL2Nat ) holds (A + B) = (B + A)

    proof

      let A,B be Element of ( Class EqBL2Nat );

      

       P0: A in ( Class EqBL2Nat ) & B in ( Class EqBL2Nat );

      consider x be object such that

       Q1: x in ( BOOLEAN * ) & A = ( Class ( EqBL2Nat ,x)) by P0, EQREL_1:def 3;

      consider y be object such that

       Q2: y in ( BOOLEAN * ) & B = ( Class ( EqBL2Nat ,y)) by P0, EQREL_1:def 3;

      reconsider x, y as Element of ( BOOLEAN * ) by Q1, Q2;

      

       R0: x in A & y in B by Q1, Q2, EQREL_1: 20;

      then

       R1: (A + B) = ( Class ( EqBL2Nat ,(x + y))) by LM800;

      

       L1: (B + A) = ( Class ( EqBL2Nat ,(y + x))) by LM800, R0;

      ( QuBL2Nat . (A + B)) = ( BL2Nat . (x + y)) by LM700, R1

      .= (( BL2Nat . x) + ( BL2Nat . y)) by LM240

      .= ( BL2Nat . (y + x)) by LM240

      .= ( QuBL2Nat . (B + A)) by L1, LM700;

      hence thesis by FUNCT_2: 19;

    end;

    theorem :: BINARI_6:39

    for A,B,C be Element of ( Class EqBL2Nat ) holds ((A + B) + C) = (A + (B + C))

    proof

      let A,B,C be Element of ( Class EqBL2Nat );

      

       P0: A in ( Class EqBL2Nat ) & B in ( Class EqBL2Nat ) & C in ( Class EqBL2Nat );

      consider x be object such that

       Q1: x in ( BOOLEAN * ) & A = ( Class ( EqBL2Nat ,x)) by P0, EQREL_1:def 3;

      consider y be object such that

       Q2: y in ( BOOLEAN * ) & B = ( Class ( EqBL2Nat ,y)) by P0, EQREL_1:def 3;

      consider z be object such that

       Q3: z in ( BOOLEAN * ) & C = ( Class ( EqBL2Nat ,z)) by P0, EQREL_1:def 3;

      reconsider x, y, z as Element of ( BOOLEAN * ) by Q1, Q2, Q3;

      

       R0: x in A & y in B & z in C by Q1, Q2, Q3, EQREL_1: 20;

      then

       R1: (A + B) = ( Class ( EqBL2Nat ,(x + y))) by LM800;

      (x + y) in (A + B) by R1, EQREL_1: 20;

      then

       R2: ((A + B) + C) = ( Class ( EqBL2Nat ,((x + y) + z))) by LM800, R0;

      

       L1: (B + C) = ( Class ( EqBL2Nat ,(y + z))) by LM800, R0;

      (y + z) in (B + C) by L1, EQREL_1: 20;

      then

       L2: (A + (B + C)) = ( Class ( EqBL2Nat ,(x + (y + z)))) by LM800, R0;

      ( QuBL2Nat . ((A + B) + C)) = ( BL2Nat . ((x + y) + z)) by LM700, R2

      .= (( BL2Nat . (x + y)) + ( BL2Nat . z)) by LM240

      .= ((( BL2Nat . x) + ( BL2Nat . y)) + ( BL2Nat . z)) by LM240

      .= (( BL2Nat . x) + (( BL2Nat . y) + ( BL2Nat . z)))

      .= (( BL2Nat . x) + ( BL2Nat . (y + z))) by LM240

      .= ( BL2Nat . (x + (y + z))) by LM240

      .= ( QuBL2Nat . (A + (B + C))) by L2, LM700;

      hence thesis by FUNCT_2: 19;

    end;

    theorem :: BINARI_6:40

    

     LM930: for n be Nat, z,z1 be Element of ( BOOLEAN * ) st z = ( <*> BOOLEAN ) & z1 = ( 0* n) holds ( Class ( EqBL2Nat ,z)) = ( Class ( EqBL2Nat ,z1))

    proof

      let n be Nat, z,z1 be Element of ( BOOLEAN * );

      assume

       AS: z = ( <*> BOOLEAN ) & z1 = ( 0* n);

      then

       P1: ( len z) = 0 ;

      

       P2: ( BL2Nat . z) = ( ExAbsval z) by Def110

      .= 0 by D100, P1;

      

       P3: ( BL2Nat . z1) = ( ExAbsval z1) by Def110;

      per cases ;

        suppose n = 0 ;

        hence ( Class ( EqBL2Nat ,z)) = ( Class ( EqBL2Nat ,z1)) by AS;

      end;

        suppose

         nz: n <> 0 ;

        consider n1 be Nat, y be Tuple of n1, BOOLEAN such that

         C2: y = z1 & ( ExAbsval z1) = ( Absval y) by Def100;

        n1 = ( len y) by CARD_1:def 7

        .= n by CARD_1:def 7, AS, C2;

        then ( BL2Nat . z1) = 0 by nz, C2, P3, AS, BINARI_3: 6;

        then [z, z1] in EqBL2Nat by P2, Def300;

        hence ( Class ( EqBL2Nat ,z)) = ( Class ( EqBL2Nat ,z1)) by EQREL_1: 35;

      end;

    end;

    theorem :: BINARI_6:41

    for A,Z be Element of ( Class EqBL2Nat ), n be Nat, z be Element of ( BOOLEAN * ) st Z = ( Class ( EqBL2Nat ,z)) & z = ( 0* n) holds (A + Z) = A & (Z + A) = A

    proof

      let A,Z be Element of ( Class EqBL2Nat ), n be Nat, z be Element of ( BOOLEAN * );

      assume

       AS: Z = ( Class ( EqBL2Nat ,z)) & z = ( 0* n);

      reconsider zempty = ( <*> BOOLEAN ) as Element of ( BOOLEAN * ) by FINSEQ_1:def 11;

      Z = ( Class ( EqBL2Nat ,zempty)) by AS, LM930;

      then

       P3: zempty in Z by EQREL_1: 20;

      

       P4: ( len zempty) = 0 ;

      

       P0: A in ( Class EqBL2Nat );

      consider x be object such that

       Q1: x in ( BOOLEAN * ) & A = ( Class ( EqBL2Nat ,x)) by P0, EQREL_1:def 3;

      reconsider x as Element of ( BOOLEAN * ) by Q1;

      x in A by Q1, EQREL_1: 20;

      

      hence (A + Z) = ( Class ( EqBL2Nat ,(x + zempty))) by P3, LM800

      .= A by Q1, P4, Def3;

      hence (Z + A) = A by LM910;

    end;