binari_4.miz



    begin

    reserve n for non zero Nat,

j,k,l,m for Nat,

g,h,i for Integer;

    theorem :: BINARI_4:1

    

     Th1: for m be Nat st m > 0 holds (m * 2) >= (m + 1)

    proof

      let m be Nat;

      assume m > 0 ;

      then

       A1: m >= ( 0 + 1) by INT_1: 7;

      (m * 2) = (m + m);

      hence thesis by A1, XREAL_1: 6;

    end;

    theorem :: BINARI_4:2

    

     Th2: for m be Nat holds (2 to_power m) >= m

    proof

      defpred P[ Nat] means (2 to_power $1) >= $1;

      

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

      proof

        let m be Nat such that

         A2: (2 to_power m) >= m;

        per cases ;

          suppose

           A3: m = 0 ;

          then (2 to_power (m + 1)) = 2 by POWER: 25;

          hence thesis by A3;

        end;

          suppose

           A4: m > 0 ;

          reconsider m2 = (2 to_power m) as Nat;

          (m2 * 2) >= (m * 2) & (2 to_power 1) = 2 by A2, NAT_1: 4, POWER: 25;

          then

           A5: (2 to_power (m + 1)) >= (m * 2) by POWER: 27;

          (m * 2) >= (m + 1) by A4, Th1;

          hence thesis by A5, XXREAL_0: 2;

        end;

      end;

      

       A6: P[ 0 ];

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

    end;

    theorem :: BINARI_4:3

    for m be Nat holds (( 0* m) + ( 0* m)) = ( 0* m)

    proof

      let m be Nat;

      

       A1: ( dom ( 0* m)) = ( Seg m) by FUNCOP_1: 13;

      ( dom addreal ) = [: REAL , REAL :] & ( rng ( 0* m)) c= REAL by FINSEQ_1:def 4, FUNCT_2:def 1;

      then

       A2: [:( rng ( 0* m)), ( rng ( 0* m)):] c= ( dom addreal ) by ZFMISC_1: 96;

      

       A3: ( dom (( 0* m) + ( 0* m))) = ( dom ( addreal .: (( 0* m),( 0* m)))) by RVSUM_1:def 4

      .= (( dom ( 0* m)) /\ ( dom ( 0* m))) by A2, FUNCOP_1: 69

      .= ( Seg m) by FUNCOP_1: 13;

      for k be Nat st k in ( dom ( 0* m)) holds (( 0* m) . k) = ((( 0* m) + ( 0* m)) . k)

      proof

        let k be Nat such that

         A4: k in ( dom ( 0* m));

        (( 0* m) . k) = 0 ;

        then ((( 0* m) + ( 0* m)) . k) = ( 0 + 0 ) by A3, A1, A4, VALUED_1:def 1;

        hence thesis;

      end;

      hence thesis by A3, FINSEQ_1: 13, FUNCOP_1: 13;

    end;

    theorem :: BINARI_4:4

    

     Th4: for k,m,l be Nat holds k <= l & l <= m implies k = l or (k + 1) <= l & l <= m

    proof

      defpred P[ Nat] means for m,l be Nat holds $1 <= l & l <= m implies $1 = l or (($1 + 1) <= l & l <= m);

      

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

      proof

        let k be Nat such that P[k];

        let m,l be Nat;

        assume that

         A2: (k + 1) <= l and

         A3: l <= m;

        (k + 1) = l or (k + 1) < l by A2, XXREAL_0: 1;

        hence thesis by A3, NAT_1: 13;

      end;

      

       A4: P[ 0 ] by NAT_1: 13;

      thus for k be Nat holds P[k] from NAT_1:sch 2( A4, A1);

    end;

    theorem :: BINARI_4:5

    

     Th5: for n be non zero Nat holds for x,y be Tuple of n, BOOLEAN st x = ( 0* n) & y = ( 0* n) holds ( carry (x,y)) = ( 0* n)

    proof

      let n be non zero Nat;

      let x,y be Tuple of n, BOOLEAN such that

       A1: x = ( 0* n) and

       A2: y = ( 0* n);

      

       A3: for j be Nat st 1 < j & j <= n holds (( carry (x,y)) . j) = 0

      proof

        let j be Nat such that

         A4: 1 < j and

         A5: j <= n;

        reconsider k = (j - 1) as Element of NAT by A4, INT_1: 5;

        (k + 1) = j;

        then

         A6: 1 <= k & k < n by A4, A5, NAT_1: 13;

        ( len ( 0* n)) = n by CARD_1:def 7;

        

        then

         A7: (x /. k) = (( 0* n) . k) by A1, A6, FINSEQ_4: 15

        .= FALSE ;

        

         A8: j = (k + 1);

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

        

        then (( carry (x,y)) . j) = (( carry (x,y)) /. j) by A4, A5, FINSEQ_4: 15

        .= ((( FALSE '&' FALSE ) 'or' ( FALSE '&' (( carry (x,y)) /. k))) 'or' ( FALSE '&' (( carry (x,y)) /. k))) by A1, A2, A6, A8, A7, BINARITH:def 2

        .= FALSE ;

        hence thesis;

      end;

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

      

      then

       A9: (( carry (x,y)) . 1) = (( carry (x,y)) /. 1) by FINSEQ_4: 15

      .= 0 by BINARITH:def 2;

      for l be Nat st l in ( Seg n) holds (( carry (x,y)) . l) = (( 0* n) . l)

      proof

        let l be Nat such that

         A10: l in ( Seg n);

        

         A11: 1 <= l by A10, FINSEQ_1: 1;

        

         A12: (( 0* n) . l) = 0 ;

        per cases by A10, A11, Th4, FINSEQ_1: 1;

          suppose l = 1;

          hence thesis by A9;

        end;

          suppose

           A13: (1 + 1) <= l & l <= n;

          then 1 < l by NAT_1: 13;

          hence thesis by A3, A12, A13;

        end;

      end;

      hence thesis by A1, FINSEQ_2: 119;

    end;

    theorem :: BINARI_4:6

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

    proof

      let n be non zero Nat;

      let x,y be Tuple of n, BOOLEAN such that

       A1: x = ( 0* n) and

       A2: y = ( 0* n);

      for k be Nat st k in ( Seg n) holds ((x + y) . k) = (( 0* n) . k)

      proof

        let k be Nat such that

         A3: k in ( Seg n);

        reconsider k as Nat;

        

         A4: (( 0* n) . k) = FALSE ;

        

         A5: 1 <= k by A3, FINSEQ_1: 1;

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

        then k <= ( len x) by A3, FINSEQ_1: 1;

        then

         A6: (y /. k) = FALSE by A1, A2, A4, A5, FINSEQ_4: 15;

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

        then k <= ( len ( carry (x,y))) by A3, FINSEQ_1: 1;

        

        then

         A7: (( carry (x,y)) /. k) = (( carry (x,y)) . k) by A5, FINSEQ_4: 15

        .= FALSE by A1, A2, A4, Th5;

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

        then k <= ( len (x + y)) by A3, FINSEQ_1: 1;

        

        then ((x + y) . k) = ((x + y) /. k) by A5, FINSEQ_4: 15

        .= ( FALSE 'xor' FALSE ) by A1, A2, A3, A6, A7, BINARITH:def 5

        .= FALSE ;

        hence thesis;

      end;

      hence thesis by A1, FINSEQ_2: 119;

    end;

    theorem :: BINARI_4:7

    for n be non zero Nat holds for F be Tuple of n, BOOLEAN st F = ( 0* n) holds ( Intval F) = 0

    proof

      let n be non zero Nat;

      let F be Tuple of n, BOOLEAN such that

       A1: F = ( 0* n);

      

       A2: 1 <= n by NAT_1: 14;

      n <= ( len F) by CARD_1:def 7;

      

      then (F /. n) = (F . n) by A2, FINSEQ_4: 15

      .= FALSE by A1;

      then ( Intval F) = ( Absval F) by BINARI_2:def 3;

      hence thesis by A1, BINARI_3: 6;

    end;

    theorem :: BINARI_4:8

    

     Th8: (l + m) <= (k - 1) implies l < k & m < k

    proof

      assume

       A1: (l + m) <= (k - 1);

      then

       A2: ((l + m) - m) <= ((k - 1) - m) by XREAL_1: 9;

      k <= (k + m) by NAT_1: 11;

      then

       A3: (k - m) <= ((k + m) - m) by XREAL_1: 9;

      ((k - 1) - m) = ((k - m) - 1);

      then ((k - 1) - m) < k by A3, XREAL_1: 146, XXREAL_0: 2;

      hence l < k by A2, XXREAL_0: 2;

      k <= (k + l) by NAT_1: 11;

      then

       A4: (k - l) <= ((k + l) - l) by XREAL_1: 9;

      

       A5: ((m + l) - l) <= ((k - 1) - l) by A1, XREAL_1: 9;

      ((k - 1) - l) = ((k - l) - 1);

      then ((k - 1) - l) < k by A4, XREAL_1: 146, XXREAL_0: 2;

      hence thesis by A5, XXREAL_0: 2;

    end;

    theorem :: BINARI_4:9

    

     Th9: g <= (h + i) & h < 0 & i < 0 implies g < h & g < i

    proof

      assume that

       A1: g <= (h + i) and

       A2: h < 0 and

       A3: i < 0 ;

      (g - i) <= ((h + i) - i) by A1, XREAL_1: 9;

      then (i + (g + ( - i))) < ( 0 + h) by A3, XREAL_1: 8;

      hence g < h;

      (g - h) <= ((i + h) - h) by A1, XREAL_1: 9;

      then (h + (g + ( - h))) < ( 0 + i) by A2, XREAL_1: 8;

      hence thesis;

    end;

    theorem :: BINARI_4:10

    

     Th10: (l + m) <= ((2 to_power n) - 1) implies ( add_ovfl ((n -BinarySequence l),(n -BinarySequence m))) = FALSE

    proof

      set L = (n -BinarySequence l), M = (n -BinarySequence m);

      

       A1: (( Absval (L + M)) + (2 to_power n)) >= (2 to_power n) by NAT_1: 11;

      assume

       A2: (l + m) <= ((2 to_power n) - 1);

      then

       A3: l < (2 to_power n) by Th8;

      assume ( add_ovfl (L,M)) <> FALSE ;

      then

       A4: ( IFEQ (( add_ovfl (L,M)), FALSE , 0 ,(2 to_power n))) = (2 to_power n) by FUNCOP_1:def 8;

      

       A5: m < (2 to_power n) by A2, Th8;

      (( Absval (L + M)) + ( IFEQ (( add_ovfl (L,M)), FALSE , 0 ,(2 to_power n)))) = (( Absval L) + ( Absval M)) by BINARITH: 21

      .= (l + ( Absval M)) by A3, BINARI_3: 35

      .= (l + m) by A5, BINARI_3: 35;

      hence contradiction by A2, A4, A1, XREAL_1: 146, XXREAL_0: 2;

    end;

    theorem :: BINARI_4:11

    

     Th11: for n be non zero Nat, l,m be Nat st (l + m) <= ((2 to_power n) - 1) holds ( Absval ((n -BinarySequence l) + (n -BinarySequence m))) = (l + m)

    proof

      let n be non zero Nat, l,m be Nat such that

       A1: (l + m) <= ((2 to_power n) - 1);

      

       A2: l < (2 to_power n) by A1, Th8;

      set L = (n -BinarySequence l), M = (n -BinarySequence m);

      ( add_ovfl (L,M)) = FALSE by A1, Th10;

      then (L,M) are_summable by BINARITH:def 7;

      

      then

       A3: ( Absval (L + M)) = (( Absval L) + ( Absval M)) by BINARITH: 22

      .= (l + ( Absval M)) by A2, BINARI_3: 35;

      m < (2 to_power n) by A1, Th8;

      hence thesis by A3, BINARI_3: 35;

    end;

    theorem :: BINARI_4:12

    

     Th12: for n be non zero Nat holds for z be Tuple of n, BOOLEAN st (z /. n) = TRUE holds ( Absval z) >= (2 to_power (n -' 1))

    proof

      defpred P[ Nat] means (for z be Tuple of $1, BOOLEAN st (z /. $1) = TRUE holds ( Absval z) >= (2 to_power ($1 -' 1)));

      

       A1: for n be non zero Nat st P[n] holds P[(n + 1)]

      proof

        let n be non zero Nat such that P[n];

        let z be Tuple of (n + 1), BOOLEAN such that

         A2: (z /. (n + 1)) = TRUE ;

        consider x be Element of (n -tuples_on BOOLEAN ), a be Element of BOOLEAN such that

         A3: z = (x ^ <*a*>) by FINSEQ_2: 117;

        

         A4: (n + 1) >= 1 by NAT_1: 11;

        then ((n + 1) - 1) >= (1 - 1) by XREAL_1: 9;

        then

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

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

        

        then

         A6: (z /. (n + 1)) = ((x ^ <*a*>) . (n + 1)) by A3, A4, FINSEQ_4: 15

        .= a by FINSEQ_2: 116;

        ( Absval z) = (( Absval x) + ( IFEQ (a, FALSE , 0 ,(2 to_power n)))) by A3, BINARITH: 20

        .= (( Absval x) + (2 to_power n)) by A2, A6, FUNCOP_1:def 8;

        hence thesis by A5, NAT_1: 11;

      end;

      

       A7: P[1]

      proof

        let z be Tuple of 1, BOOLEAN such that

         A8: (z /. 1) = TRUE ;

        

         A9: ( len z) = 1 by CARD_1:def 7;

        then (z . 1) = (z /. 1) by FINSEQ_4: 15;

        then z = <* TRUE *> by A8, A9, FINSEQ_1: 40;

        then

         A10: ( Absval z) = 1 by BINARITH: 16;

        (2 to_power (1 -' 1)) = (2 to_power (1 - 1)) by XREAL_0:def 2;

        hence thesis by A10, POWER: 24;

      end;

      thus for n be non zero Nat holds P[n] from NAT_1:sch 10( A7, A1);

    end;

    theorem :: BINARI_4:13

    

     Th13: (l + m) <= ((2 to_power (n -' 1)) - 1) implies (( carry ((n -BinarySequence l),(n -BinarySequence m))) /. n) = FALSE

    proof

      set L = (n -BinarySequence l), M = (n -BinarySequence m), F = FALSE , T = TRUE ;

      assume

       A1: (l + m) <= ((2 to_power (n -' 1)) - 1);

      then

       A2: l < (2 to_power (n -' 1)) by Th8;

      n >= 1 by NAT_1: 14;

      then (n - 1) >= (1 - 1) by XREAL_1: 9;

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

      then (2 to_power (n -' 1)) < (2 to_power n) by POWER: 39, XREAL_1: 146;

      then

       A3: ((2 to_power (n -' 1)) - 1) < ((2 to_power n) - 1) by XREAL_1: 14;

      assume not (( carry (L,M)) /. n) = F;

      then

       A4: (( carry (L,M)) /. n) = T by XBOOLEAN:def 3;

      

       A5: m < (2 to_power (n -' 1)) by A1, Th8;

      1 <= n by NAT_1: 14;

      then

       A6: n in ( Seg n) by FINSEQ_1: 1;

      

      then

       A7: (M /. n) = ( IFEQ (((m div (2 to_power (n -' 1))) mod 2), 0 ,F,T)) by BINARI_3:def 1

      .= ( IFEQ (( 0 mod 2), 0 ,F,T)) by A5, NAT_D: 27

      .= ( IFEQ ( 0 , 0 ,F,T)) by NAT_D: 26

      .= F by FUNCOP_1:def 8;

      (L /. n) = ( IFEQ (((l div (2 to_power (n -' 1))) mod 2), 0 ,F,T)) by A6, BINARI_3:def 1

      .= ( IFEQ (( 0 mod 2), 0 ,F,T)) by A2, NAT_D: 27

      .= ( IFEQ ( 0 , 0 ,F,T)) by NAT_D: 26

      .= F by FUNCOP_1:def 8;

      

      then ((L + M) /. n) = ((F 'xor' F) 'xor' T) by A4, A6, A7, BINARITH:def 5

      .= T;

      then

       A8: ( Absval (L + M)) >= (2 to_power (n -' 1)) by Th12;

      (l + m) < (2 to_power (n -' 1)) by A1, XREAL_1: 146, XXREAL_0: 2;

      hence contradiction by A1, A3, A8, Th11, XXREAL_0: 2;

    end;

    theorem :: BINARI_4:14

    

     Th14: for n be non zero Nat st (l + m) <= ((2 to_power (n -' 1)) - 1) holds ( Intval ((n -BinarySequence l) + (n -BinarySequence m))) = (l + m)

    proof

      let n be non zero Nat such that

       A1: (l + m) <= ((2 to_power (n -' 1)) - 1);

      

       A2: l < (2 to_power (n -' 1)) by A1, Th8;

      set L = (n -BinarySequence l), M = (n -BinarySequence m), F = FALSE , T = TRUE ;

      n >= 1 by NAT_1: 14;

      then (n - 1) >= (1 - 1) by XREAL_1: 9;

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

      then (2 to_power (n -' 1)) < (2 to_power n) by POWER: 39, XREAL_1: 146;

      then

       A3: ((2 to_power (n -' 1)) - 1) < ((2 to_power n) - 1) by XREAL_1: 14;

      

       A4: m < (2 to_power (n -' 1)) by A1, Th8;

      1 <= n by NAT_1: 14;

      then

       A5: n in ( Seg n) by FINSEQ_1: 1;

      

      then

       A6: (M /. n) = ( IFEQ (((m div (2 to_power (n -' 1))) mod 2), 0 ,F,T)) by BINARI_3:def 1

      .= ( IFEQ (( 0 mod 2), 0 ,F,T)) by A4, NAT_D: 27

      .= ( IFEQ ( 0 , 0 ,F,T)) by NAT_D: 26

      .= F by FUNCOP_1:def 8;

      (L /. n) = ( IFEQ (((l div (2 to_power (n -' 1))) mod 2), 0 ,F,T)) by A5, BINARI_3:def 1

      .= ( IFEQ (( 0 mod 2), 0 ,F,T)) by A2, NAT_D: 27

      .= ( IFEQ ( 0 , 0 ,F,T)) by NAT_D: 26

      .= F by FUNCOP_1:def 8;

      

      then ((L + M) /. n) = ((F 'xor' F) 'xor' (( carry (L,M)) /. n)) by A5, A6, BINARITH:def 5

      .= F by A1, Th13;

      then ( Intval (L + M)) = ( Absval (L + M)) by BINARI_2:def 3;

      hence thesis by A1, A3, Th11, XXREAL_0: 2;

    end;

    theorem :: BINARI_4:15

    

     Th15: for z be Tuple of 1, BOOLEAN st z = <* TRUE *> holds ( Intval z) = ( - 1)

    proof

      let z be Tuple of 1, BOOLEAN such that

       A1: z = <* TRUE *>;

      ( len z) = 1 by CARD_1:def 7;

      

      then (z /. 1) = (z . 1) by FINSEQ_4: 15

      .= TRUE by A1, FINSEQ_1: 40;

      

      then ( Intval z) = (( Absval z) - (2 to_power 1)) by BINARI_2:def 3

      .= (1 - (2 to_power 1)) by A1, BINARITH: 16

      .= (1 - (1 + 1)) by POWER: 25

      .= ( 0 - 1);

      hence thesis;

    end;

    theorem :: BINARI_4:16

    for z be Tuple of 1, BOOLEAN st z = <* FALSE *> holds ( Intval z) = 0

    proof

      let z be Tuple of 1, BOOLEAN such that

       A1: z = <* FALSE *>;

      ( len z) = 1 by CARD_1:def 7;

      

      then (z /. 1) = (z . 1) by FINSEQ_4: 15

      .= FALSE by A1, FINSEQ_1: 40;

      then ( Intval z) = ( Absval z) by BINARI_2:def 3;

      hence thesis by A1, BINARITH: 15;

    end;

    theorem :: BINARI_4:17

    for x be boolean object holds ( TRUE 'or' x) = TRUE ;

    theorem :: BINARI_4:18

    for n be non zero Nat holds 0 <= ((2 to_power (n -' 1)) - 1) & ( - (2 to_power (n -' 1))) <= 0

    proof

      defpred P[ Nat] means 0 <= ((2 to_power ($1 -' 1)) - 1) & ( - (2 to_power ($1 -' 1))) <= 0 ;

      

       A1: for k be non zero Nat st P[k] holds P[(k + 1)]

      proof

        let k be non zero Nat such that

         A2: 0 <= ((2 to_power (k -' 1)) - 1) and ( - (2 to_power (k -' 1))) <= 0 ;

        ((k + 1) -' 1) = k by NAT_D: 34;

        then (2 to_power (k -' 1)) < (2 to_power ((k + 1) -' 1)) by NAT_2: 9, POWER: 39;

        hence thesis by A2, XREAL_1: 9;

      end;

      (1 - 1) = 0 ;

      

      then (2 to_power (1 -' 1)) = (2 to_power 0 ) by XREAL_0:def 2

      .= 1 by POWER: 24;

      then

       A3: P[1];

      thus for n be non zero Nat holds P[n] from NAT_1:sch 10( A3, A1);

    end;

    theorem :: BINARI_4:19

    for x,y be Tuple of n, BOOLEAN st x = ( 0* n) & y = ( 0* n) holds (x,y) are_summable

    proof

      let x,y be Tuple of n, BOOLEAN such that

       A1: x = ( 0* n) and

       A2: y = ( 0* n);

      

       A3: 1 <= n by NAT_1: 14;

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

      

      then (x /. n) = (( 0* n) . n) by A1, A3, FINSEQ_4: 15

      .= FALSE ;

      

      then ( add_ovfl (x,y)) = ((( FALSE '&' FALSE ) 'or' ( FALSE '&' (( carry (x,y)) /. n))) 'or' ( FALSE '&' (( carry (x,y)) /. n))) by A1, A2, BINARITH:def 6

      .= FALSE ;

      hence thesis by BINARITH:def 7;

    end;

    theorem :: BINARI_4:20

    

     Th20: ((i * n) mod n) = 0 by NAT_D: 71;

    begin

    definition

      let m,j be Nat;

      :: BINARI_4:def1

      func MajP (m,j) -> Nat means

      : Def1: (2 to_power it ) >= j & it >= m & for k be Nat st (2 to_power k) >= j & k >= m holds k >= it ;

      existence

      proof

        per cases ;

          suppose

           A1: (2 to_power m) >= j;

          for k be Nat st (2 to_power k) >= j & k >= m holds k >= m;

          hence thesis by A1;

        end;

          suppose

           A2: (2 to_power m) < j;

          defpred P[ Nat] means (2 to_power $1) >= j & $1 >= m;

          (2 to_power m) >= m by Th2;

          then

           A3: j >= m by A2, XXREAL_0: 2;

          (2 to_power j) >= j by Th2;

          then

           A4: ex k be Nat st P[k] by A3;

          ex k be Nat st P[k] & for l be Nat st P[l] holds l >= k from NAT_1:sch 5( A4);

          hence thesis;

        end;

      end;

      uniqueness

      proof

        let p,q be Nat;

        assume (2 to_power p) >= j & p >= m & (for k be Nat st (2 to_power k) >= j & k >= m holds k >= p) & (2 to_power q) >= j & (q >= m & for k be Nat st (2 to_power k) >= j & k >= m holds k >= q);

        then p >= q & q >= p;

        hence thesis by XXREAL_0: 1;

      end;

    end

    theorem :: BINARI_4:21

    j >= k implies ( MajP (m,j)) >= ( MajP (m,k))

    proof

      assume

       A1: j >= k;

      

       A2: ( MajP (m,j)) >= m by Def1;

      (2 to_power ( MajP (m,j))) >= j by Def1;

      then (2 to_power ( MajP (m,j))) >= k by A1, XXREAL_0: 2;

      hence thesis by A2, Def1;

    end;

    theorem :: BINARI_4:22

    

     Th22: l >= m implies ( MajP (l,j)) >= ( MajP (m,j))

    proof

      assume

       A1: l >= m;

      

       A2: (2 to_power ( MajP (l,j))) >= j by Def1;

      ( MajP (l,j)) >= l by Def1;

      then ( MajP (l,j)) >= m by A1, XXREAL_0: 2;

      hence thesis by A2, Def1;

    end;

    theorem :: BINARI_4:23

    m >= 1 implies ( MajP (m,1)) = m

    proof

      assume m >= 1;

      then

       A1: (2 to_power m) >= 1 by POWER: 35;

      for k be Nat st (2 to_power k) >= 1 & k >= m holds k >= m;

      hence thesis by A1, Def1;

    end;

    theorem :: BINARI_4:24

    

     Th24: j <= (2 to_power m) implies ( MajP (m,j)) = m

    proof

      

       A1: for k be Nat st (2 to_power k) >= j & k >= m holds k >= m;

      assume j <= (2 to_power m);

      hence thesis by A1, Def1;

    end;

    theorem :: BINARI_4:25

    j > (2 to_power m) implies ( MajP (m,j)) > m

    proof

      assume

       A1: j > (2 to_power m);

      (2 to_power ( MajP (m,j))) >= j by Def1;

      then (2 to_power ( MajP (m,j))) > (2 to_power m) by A1, XXREAL_0: 2;

      hence thesis by PRE_FF: 8;

    end;

    begin

    definition

      let m be Nat;

      let i be Integer;

      :: BINARI_4:def2

      func 2sComplement (m,i) -> Tuple of m, BOOLEAN equals

      : Def2: (m -BinarySequence |.((2 to_power ( MajP (m, |.i.|))) + i).|) if i < 0

      otherwise (m -BinarySequence |.i.|);

      correctness ;

    end

    theorem :: BINARI_4:26

    for m be Nat holds ( 2sComplement (m, 0 )) = ( 0* m)

    proof

      let m be Nat;

      ( 2sComplement (m, 0 )) = (m -BinarySequence |. 0 .|) by Def2

      .= (m -BinarySequence 0 ) by ABSVALUE: 2;

      hence thesis by BINARI_3: 25;

    end;

    theorem :: BINARI_4:27

    for i be Integer st i <= ((2 to_power (n -' 1)) - 1) & ( - (2 to_power (n -' 1))) <= i holds ( Intval ( 2sComplement (n,i))) = i

    proof

      let i such that

       A1: i <= ((2 to_power (n -' 1)) - 1) and

       A2: ( - (2 to_power (n -' 1))) <= i;

      

       A3: n >= 1 by NAT_1: 14;

      now

        per cases ;

          suppose i >= 0 ;

          then

          reconsider i as Element of NAT by INT_1: 3;

          

           A4: ( 2sComplement (n,i)) = (n -BinarySequence |.i.|) by Def2

          .= (n -BinarySequence i) by ABSVALUE:def 1;

          (i + 1) <= (((2 to_power (n -' 1)) - 1) + 1) by A1, XREAL_1: 6;

          then

           A5: i < (2 to_power (n -' 1)) by NAT_1: 13;

          n >= 1 by NAT_1: 14;

          then (n - 1) >= (1 - 1) by XREAL_1: 9;

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

          then (2 to_power (n -' 1)) < (2 to_power n) by POWER: 39, XREAL_1: 146;

          then i < (2 to_power n) by A5, XXREAL_0: 2;

          then

           A6: ( Absval (n -BinarySequence i)) = i by BINARI_3: 35;

          1 <= n by NAT_1: 14;

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

          

          then ((n -BinarySequence i) /. n) = ( IFEQ (((i div (2 to_power (n -' 1))) mod 2), 0 , FALSE , TRUE )) by BINARI_3:def 1

          .= ( IFEQ (( 0 mod 2), 0 , FALSE , TRUE )) by A5, NAT_D: 27

          .= ( IFEQ ( 0 , 0 , FALSE , TRUE )) by NAT_D: 26

          .= FALSE by FUNCOP_1:def 8;

          hence thesis by A4, A6, BINARI_2:def 3;

        end;

          suppose

           A7: i < 0 ;

          

           A8: (2 to_power n) >= (2 to_power (n -' 1)) by NAT_2: 9, POWER: 39;

          then ( - (2 to_power n)) <= ( - (2 to_power (n -' 1))) by XREAL_1: 24;

          then ( - (2 to_power n)) <= i by A2, XXREAL_0: 2;

          then (( - (2 to_power n)) - i) <= (i - i) by XREAL_1: 9;

          then ( - ((2 to_power n) + i)) <= 0 ;

          then ((2 to_power n) + i) >= ( - 0 );

          then

          reconsider k = ((2 to_power n) + i) as Element of NAT by INT_1: 3;

           |.i.| = ( - i) by A7, ABSVALUE:def 1;

          then |.i.| <= ( - ( - (2 to_power (n -' 1)))) by A2, XREAL_1: 24;

          then ( MajP (n, |.i.|)) = n by A8, Th24, XXREAL_0: 2;

          

          then

           A9: ( 2sComplement (n,i)) = (n -BinarySequence |.k.|) by A7, Def2

          .= (n -BinarySequence k) by ABSVALUE:def 1;

          k < ((2 to_power n) + 0 ) by A7, XREAL_1: 8;

          then k < ((2 to_power 1) * (2 to_power (n -' 1))) by NAT_1: 14, NAT_2: 10;

          then k < (2 * (2 to_power (n -' 1))) by POWER: 25;

          then

           A10: k < ((2 to_power (n -' 1)) + (2 to_power (n -' 1)));

          

           A11: ((2 to_power n) + i) < ((2 to_power n) + 0 ) by A7, XREAL_1: 6;

          ((2 to_power n) + ( - (2 to_power (n -' 1)))) = ((2 to_power n) - (2 to_power (n -' 1)))

          .= (((2 to_power 1) * (2 to_power (n -' 1))) - (2 to_power (n -' 1))) by NAT_1: 14, NAT_2: 10

          .= ((2 * (2 to_power (n -' 1))) - (2 to_power (n -' 1))) by POWER: 25

          .= (2 to_power (n -' 1));

          then

           A12: k >= (2 to_power (n -' 1)) by A2, XREAL_1: 6;

          n in ( Seg n) by A3, FINSEQ_1: 1;

          

          then ((n -BinarySequence k) /. n) = ( IFEQ (((k div (2 to_power (n -' 1))) mod 2), 0 , FALSE , TRUE )) by BINARI_3:def 1

          .= ( IFEQ ((1 mod 2), 0 , FALSE , TRUE )) by A12, A10, NAT_2: 20

          .= ( IFEQ (1, 0 , FALSE , TRUE )) by NAT_D: 14

          .= TRUE by FUNCOP_1:def 8;

          

          then ( Intval ( 2sComplement (n,i))) = (( Absval (n -BinarySequence k)) - (2 to_power n)) by A9, BINARI_2:def 3

          .= (k - (2 to_power n)) by A11, BINARI_3: 35

          .= ( 0 + i);

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm1: (k mod n) = (l mod n) & k > l implies ex s be Integer st k = (l + (s * n))

    proof

      assume that

       A1: (k mod n) = (l mod n) and

       A2: k > l;

      consider m be Nat such that

       A3: k = (l + m) by A2, NAT_1: 10;

      take (m div n);

      l = (((l div n) * n) + (l mod n)) & k = (((k div n) * n) + (l mod n)) by A1, NAT_D: 2;

      

      then (m mod n) = ((((k div n) - (l div n)) * n) mod n) by A3

      .= 0 by Th20;

      then ((l + m) div n) = ((l div n) + (m div n)) by NAT_D: 19;

      

      then k = ((((l div n) + (m div n)) * n) + (l mod n)) by A1, A3, NAT_D: 2

      .= (((m div n) * n) + (((l div n) * n) + (l mod n)))

      .= (((m div n) * n) + l) by NAT_D: 2;

      hence thesis;

    end;

    

     Lm2: (k mod n) = (l mod n) implies ex s be Integer st k = (l + (s * n))

    proof

      assume

       A1: (k mod n) = (l mod n);

      now

        per cases by XXREAL_0: 1;

          suppose

           A2: k = l;

          set s = 0 ;

          k = (l + (s * n)) by A2;

          hence thesis;

        end;

          suppose

           A3: k > l or l > k;

          now

            per cases by A3;

              suppose k > l;

              hence thesis by A1, Lm1;

            end;

              suppose k < l;

              then

              consider t be Integer such that

               A4: l = (k + (t * n)) by A1, Lm1;

              k = (l + (( - t) * n)) by A4;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm3: for k,l,m be Nat st m < n & (k mod (2 to_power n)) = (l mod (2 to_power n)) holds ((k div (2 to_power m)) mod 2) = ((l div (2 to_power m)) mod 2)

    proof

      let k,l,m be Nat such that

       A1: m < n and

       A2: (k mod (2 to_power n)) = (l mod (2 to_power n));

      consider j be Nat such that

       A3: n = (m + j) by A1, NAT_1: 10;

      (2 to_power n) = (2 |^ n) by POWER: 41;

      then (2 to_power n) is non zero by PREPOWER: 5;

      then

      consider s be Integer such that

       A4: k = (l + (s * (2 to_power n))) by A2, Lm2;

      reconsider j as Nat;

      set M = (2 to_power m), J = (2 to_power j);

      (m + ( - m)) < (n + ( - m)) by A1, XREAL_1: 8;

      then ( 0 + 1) < (j + 1) by A3, XREAL_1: 8;

      then 1 <= j by NAT_1: 13;

      then (2 to_power 1) divides (2 to_power j) by NAT_2: 11;

      then 2 divides (2 to_power j) by POWER: 25;

      then (J mod 2) = 0 by PEPIN: 6;

      

      then

       A5: ((s * J) mod 2) = (((s mod 2) * 0 ) mod 2) by NAT_D: 67

      .= 0 by NAT_D: 26;

      reconsider L = l as Integer;

      

       A6: M > 0 by POWER: 34;

      (k div M) = ((l + (s * (J * M))) div M) by A4, A3, POWER: 27

      .= ((l + ((s * J) * M)) div M)

      .= ((l div M) + (s * J)) by A6, NAT_D: 61;

      

      then ((k div M) mod 2) = ((((L div M) mod 2) + 0 ) mod 2) by A5, NAT_D: 66

      .= ((L div M) mod 2) by NAT_D: 65;

      hence thesis;

    end;

    

     Lm4: for h,i be Integer st (h mod (2 to_power n)) = (i mod (2 to_power n)) holds (((2 to_power ( MajP (n, |.h.|))) + h) mod (2 to_power n)) = (((2 to_power ( MajP (n, |.i.|))) + i) mod (2 to_power n))

    proof

      let h,i be Integer such that

       A1: (h mod (2 to_power n)) = (i mod (2 to_power n));

      n <= ( MajP (n, |.i.|)) by Def1;

      then

      consider y be Nat such that

       A2: ( MajP (n, |.i.|)) = (n + y) by NAT_1: 10;

      reconsider L = (2 to_power ( MajP (n, |.i.|))) as Integer;

      reconsider M = (2 to_power ( MajP (n, |.h.|))) as Integer;

      n <= ( MajP (n, |.h.|)) by Def1;

      then

      consider x be Nat such that

       A3: ( MajP (n, |.h.|)) = (n + x) by NAT_1: 10;

      reconsider x as Nat;

      M = ((2 to_power n) * (2 to_power x)) by A3, POWER: 27;

      

      then

       A4: (M mod (2 to_power n)) = ((((2 to_power n) mod (2 to_power n)) * (2 to_power x)) mod (2 to_power n)) by EULER_2: 8

      .= (( 0 * (2 to_power x)) mod (2 to_power n)) by NAT_D: 25

      .= 0 by NAT_D: 26;

      reconsider y as Nat;

      L = ((2 to_power n) * (2 to_power y)) by A2, POWER: 27;

      

      then

       A5: (L mod (2 to_power n)) = ((((2 to_power n) mod (2 to_power n)) * (2 to_power y)) mod (2 to_power n)) by EULER_2: 8

      .= (( 0 * (2 to_power y)) mod (2 to_power n)) by NAT_D: 25

      .= 0 by NAT_D: 26;

      

       A6: ((L + i) mod (2 to_power n)) = (((L mod (2 to_power n)) + (i mod (2 to_power n))) mod (2 to_power n)) by NAT_D: 66

      .= ((i mod (2 to_power n)) mod (2 to_power n)) by A5;

      ((M + h) mod (2 to_power n)) = (((M mod (2 to_power n)) + (h mod (2 to_power n))) mod (2 to_power n)) by NAT_D: 66

      .= ((h mod (2 to_power n)) mod (2 to_power n)) by A4;

      hence thesis by A1, A6;

    end;

    

     Lm5: for h,i be Integer st h >= 0 & i >= 0 & (h mod (2 to_power n)) = (i mod (2 to_power n)) holds ( 2sComplement (n,h)) = ( 2sComplement (n,i))

    proof

      let h,i be Integer such that

       A1: h >= 0 & i >= 0 and

       A2: (h mod (2 to_power n)) = (i mod (2 to_power n));

      

       A3: for j be Nat st j in ( Seg n) holds ((n -BinarySequence |.h.|) . j) = ((n -BinarySequence |.i.|) . j)

      proof

        

         A4: |.h.| = h & |.i.| = i by A1, ABSVALUE:def 1;

        let j be Nat such that

         A5: j in ( Seg n);

        reconsider j as Nat;

        

         A6: j <= n by A5, FINSEQ_1: 1;

        

         A7: 1 <= j by A5, FINSEQ_1: 1;

        then (j - 1) >= (1 - 1) by XREAL_1: 9;

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

        then

         A8: (j -' 1) < n by A6, XREAL_1: 146, XXREAL_0: 2;

        ( len (n -BinarySequence |.i.|)) = n by CARD_1:def 7;

        

        then

         A9: ((n -BinarySequence |.i.|) . j) = ((n -BinarySequence |.i.|) /. j) by A7, A6, FINSEQ_4: 15

        .= ( IFEQ ((( |.i.| div (2 to_power (j -' 1))) mod 2), 0 , FALSE , TRUE )) by A5, BINARI_3:def 1;

        ( len (n -BinarySequence |.h.|)) = n by CARD_1:def 7;

        

        then ((n -BinarySequence |.h.|) . j) = ((n -BinarySequence |.h.|) /. j) by A7, A6, FINSEQ_4: 15

        .= ( IFEQ ((( |.h.| div (2 to_power (j -' 1))) mod 2), 0 , FALSE , TRUE )) by A5, BINARI_3:def 1

        .= ( IFEQ ((( |.i.| div (2 to_power (j -' 1))) mod 2), 0 , FALSE , TRUE )) by A2, A8, A4, Lm3;

        hence thesis by A9;

      end;

      ( 2sComplement (n,h)) = (n -BinarySequence |.h.|) & ( 2sComplement (n,i)) = (n -BinarySequence |.i.|) by A1, Def2;

      hence thesis by A3, FINSEQ_2: 119;

    end;

    

     Lm6: for h,i be Integer st h < 0 & i < 0 & (h mod (2 to_power n)) = (i mod (2 to_power n)) holds ( 2sComplement (n,h)) = ( 2sComplement (n,i))

    proof

      let h,i be Integer such that

       A1: h < 0 and

       A2: i < 0 and

       A3: (h mod (2 to_power n)) = (i mod (2 to_power n));

       |.i.| = ( - i) by A2, ABSVALUE:def 1;

      then (2 to_power ( MajP (n, |.i.|))) >= ( - i) by Def1;

      then ((2 to_power ( MajP (n, |.i.|))) + i) >= (( - i) + i) by XREAL_1: 6;

      then

      reconsider I = ((2 to_power ( MajP (n, |.i.|))) + i) as Element of NAT by INT_1: 3;

       |.h.| = ( - h) by A1, ABSVALUE:def 1;

      then (2 to_power ( MajP (n, |.h.|))) >= ( - h) by Def1;

      then ((2 to_power ( MajP (n, |.h.|))) + h) >= (( - h) + h) by XREAL_1: 6;

      then

      reconsider H = ((2 to_power ( MajP (n, |.h.|))) + h) as Element of NAT by INT_1: 3;

      

       A4: (H qua Nat mod (2 to_power n)) = (I qua Nat mod (2 to_power n)) by A3, Lm4;

      

       A5: for j be Nat st j in ( Seg n) holds ((n -BinarySequence |.H.|) . j) = ((n -BinarySequence |.I.|) . j)

      proof

        

         A6: ( len (n -BinarySequence I)) = n by CARD_1:def 7;

        let j be Nat such that

         A7: j in ( Seg n);

        

         A8: 1 <= j by A7, FINSEQ_1: 1;

        

         A9: j <= n by A7, FINSEQ_1: 1;

        reconsider j as Nat;

        (j - 1) >= (1 - 1) by A8, XREAL_1: 9;

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

        then

         A10: (j -' 1) < n by A9, XREAL_1: 146, XXREAL_0: 2;

        ( len (n -BinarySequence H)) = n & |.H.| = H by ABSVALUE:def 1, CARD_1:def 7;

        

        then ((n -BinarySequence |.H.|) . j) = ((n -BinarySequence H) /. j) by A8, A9, FINSEQ_4: 15

        .= ( IFEQ (((H div (2 to_power (j -' 1))) mod 2), 0 , FALSE , TRUE )) by A7, BINARI_3:def 1

        .= ( IFEQ (((I div (2 to_power (j -' 1))) mod 2), 0 , FALSE , TRUE )) by A4, A10, Lm3

        .= ((n -BinarySequence I) /. j) by A7, BINARI_3:def 1

        .= ((n -BinarySequence I) . j) by A8, A9, A6, FINSEQ_4: 15;

        hence thesis by ABSVALUE:def 1;

      end;

      ( 2sComplement (n,h)) = (n -BinarySequence |.((2 to_power ( MajP (n, |.h.|))) + h).|) & ( 2sComplement (n,i)) = (n -BinarySequence |.((2 to_power ( MajP (n, |.i.|))) + i).|) by A1, A2, Def2;

      hence thesis by A5, FINSEQ_2: 119;

    end;

    theorem :: BINARI_4:28

    for h,i be Integer st (h >= 0 & i >= 0 or h < 0 & i < 0 ) & (h mod (2 to_power n)) = (i mod (2 to_power n)) holds ( 2sComplement (n,h)) = ( 2sComplement (n,i)) by Lm5, Lm6;

    theorem :: BINARI_4:29

    for h,i be Integer st (h >= 0 & i >= 0 or h < 0 & i < 0 ) & (h,i) are_congruent_mod (2 to_power n) holds ( 2sComplement (n,h)) = ( 2sComplement (n,i))

    proof

      let h,i be Integer such that

       A1: h >= 0 & i >= 0 or h < 0 & i < 0 and

       A2: (h,i) are_congruent_mod (2 to_power n);

      (h mod (2 to_power n)) = (i mod (2 to_power n)) by A2, NAT_D: 64;

      hence thesis by A1, Lm5, Lm6;

    end;

    theorem :: BINARI_4:30

    

     Th30: for l,m be Nat st (l mod (2 to_power n)) = (m mod (2 to_power n)) holds (n -BinarySequence l) = (n -BinarySequence m)

    proof

      let l,m be Nat such that

       A1: (l mod (2 to_power n)) = (m mod (2 to_power n));

       |.m.| = m by ABSVALUE:def 1;

      then

       A2: ( 2sComplement (n,m)) = (n -BinarySequence m) by Def2;

       |.l.| = l by ABSVALUE:def 1;

      then ( 2sComplement (n,l)) = (n -BinarySequence l) by Def2;

      hence thesis by A1, A2, Lm5;

    end;

    theorem :: BINARI_4:31

    for l,m be Nat st (l,m) are_congruent_mod (2 to_power n) holds (n -BinarySequence l) = (n -BinarySequence m)

    proof

      let l,m be Nat;

      assume (l,m) are_congruent_mod (2 to_power n);

      then (l qua Integer mod (2 to_power n)) = (m qua Integer mod (2 to_power n)) by NAT_D: 64;

      hence thesis by Th30;

    end;

    theorem :: BINARI_4:32

    

     Th32: for j be Nat st 1 <= j & j <= n holds (( 2sComplement ((n + 1),i)) /. j) = (( 2sComplement (n,i)) /. j)

    proof

      let j be Nat such that

       A1: 1 <= j and

       A2: j <= n;

      

       A3: j in ( Seg n) by A1, A2, FINSEQ_1: 1;

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

      then j <= (n + 1) by A2, XXREAL_0: 2;

      then

       A4: j in ( Seg (n + 1)) by A1, FINSEQ_1: 1;

      set N = |.((2 to_power ( MajP (n, |.i.|))) + i).|;

      set M = |.((2 to_power ( MajP ((n + 1), |.i.|))) + i).|;

      

       A5: i < 0 implies ((M div (2 to_power (j -' 1))) mod 2) = ((N div (2 to_power (j -' 1))) mod 2)

      proof

        ( MajP ((n + 1), |.i.|)) >= ( MajP (n, |.i.|)) by Th22, NAT_1: 11;

        then

        consider m be Nat such that

         A6: ( MajP ((n + 1), |.i.|)) = (( MajP (n, |.i.|)) + m) by NAT_1: 10;

        reconsider m as Nat;

        set P = ( MajP (n, |.i.|));

        assume

         A7: i < 0 ;

        set Q = (2 to_power P);

        

         A8: ((Q * (2 to_power m)) qua Integer mod Q) = 0 by NAT_D: 13;

        (2 to_power ( MajP ((n + 1), |.i.|))) >= |.i.| by Def1;

        then (2 to_power ( MajP ((n + 1), |.i.|))) >= ( - i) by A7, ABSVALUE:def 1;

        then ((2 to_power ( MajP ((n + 1), |.i.|))) + i) >= (( - i) + i) by XREAL_1: 6;

        

        then M = ((2 to_power (P + m)) + i) by A6, ABSVALUE:def 1

        .= ((Q * (2 to_power m)) + i) by POWER: 27;

        

        then

         A9: (M mod Q) = ((((Q * (2 to_power m)) qua Integer mod Q) + (i mod Q)) mod Q) by NAT_D: 66

        .= ((i mod Q) mod Q) by A8;

        

         A10: (Q qua Integer mod Q) = 0 by NAT_D: 25;

        (j + ( - 1)) >= (1 + ( - 1)) by A1, XREAL_1: 6;

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

        then

         A11: (j -' 1) < n by A2, XREAL_1: 146, XXREAL_0: 2;

        P >= n by Def1;

        then

         A12: (j -' 1) < P by A11, XXREAL_0: 2;

        Q >= |.i.| by Def1;

        then Q >= ( - i) by A7, ABSVALUE:def 1;

        then (Q + i) >= (( - i) + i) by XREAL_1: 6;

        then N = (Q + i) by ABSVALUE:def 1;

        

        then (N mod Q) = (((Q qua Integer mod Q) + (i mod Q)) mod Q) by NAT_D: 66

        .= ((i mod Q) mod Q) by A10;

        hence thesis by A9, A12, Lm3;

      end;

      per cases ;

        suppose i >= 0 ;

        then

        reconsider i as Element of NAT by INT_1: 3;

        

         A13: (( 2sComplement (n,i)) /. j) = ((n -BinarySequence |.i.|) /. j) by Def2

        .= ((n -BinarySequence i) /. j) by ABSVALUE:def 1

        .= ( IFEQ (((i div (2 to_power (j -' 1))) mod 2), 0 , FALSE , TRUE )) by A3, BINARI_3:def 1;

        (( 2sComplement ((n + 1),i)) /. j) = (((n + 1) -BinarySequence |.i.|) /. j) by Def2

        .= (((n + 1) -BinarySequence i) /. j) by ABSVALUE:def 1

        .= ( IFEQ (((i div (2 to_power (j -' 1))) mod 2), 0 , FALSE , TRUE )) by A4, BINARI_3:def 1;

        hence thesis by A13;

      end;

        suppose

         A14: i < 0 ;

        

        then

         A15: (( 2sComplement (n,i)) /. j) = ((n -BinarySequence N) /. j) by Def2

        .= ( IFEQ (((N div (2 to_power (j -' 1))) mod 2), 0 , FALSE , TRUE )) by A3, BINARI_3:def 1;

        (( 2sComplement ((n + 1),i)) /. j) = (((n + 1) -BinarySequence M) /. j) by A14, Def2

        .= ( IFEQ (((M div (2 to_power (j -' 1))) mod 2), 0 , FALSE , TRUE )) by A4, BINARI_3:def 1;

        hence thesis by A5, A14, A15;

      end;

    end;

    theorem :: BINARI_4:33

    

     Th33: ex x be Element of BOOLEAN st ( 2sComplement ((m + 1),i)) = (( 2sComplement (m,i)) ^ <*x*>)

    proof

      consider a be Element of (m -tuples_on BOOLEAN ), b be Element of BOOLEAN such that

       A1: ( 2sComplement ((m + 1),i)) = (a ^ <*b*>) by FINSEQ_2: 117;

      now

        per cases ;

          suppose m > 0 ;

          then

          reconsider m as non zero Nat;

          for j be Nat st j in ( Seg m) holds (( 2sComplement (m,i)) . j) = (a . j)

          proof

            

             A2: ( len ( 2sComplement (m,i))) = m by CARD_1:def 7;

            let j be Nat such that

             A3: j in ( Seg m);

            reconsider j as Nat;

            

             A4: 1 <= j by A3, FINSEQ_1: 1;

            ( len a) = m by CARD_1:def 7;

            then

             A5: j in ( dom a) by A3, FINSEQ_1:def 3;

            

             A6: j <= m by A3, FINSEQ_1: 1;

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

            then ( len ( 2sComplement ((m + 1),i))) = (m + 1) & j <= (m + 1) by A6, CARD_1:def 7, XXREAL_0: 2;

            

            then (( 2sComplement ((m + 1),i)) . j) = (( 2sComplement ((m + 1),i)) /. j) by A4, FINSEQ_4: 15

            .= (( 2sComplement (m,i)) /. j) by A4, A6, Th32

            .= (( 2sComplement (m,i)) . j) by A2, A4, A6, FINSEQ_4: 15;

            hence thesis by A1, A5, FINSEQ_1:def 7;

          end;

          then a = ( 2sComplement (m,i)) by FINSEQ_2: 119;

          hence thesis by A1;

        end;

          suppose

           A7: m = 0 ;

          then

          consider c be Element of BOOLEAN such that

           A8: ( 2sComplement ((m + 1),i)) = <*c*> by FINSEQ_2: 97;

          

           A9: ( 2sComplement ((m + 1),i)) = ( {} ^ <*c*>) by A8, FINSEQ_1: 34;

          ( 2sComplement (m,i)) = {} by A7;

          hence thesis by A9;

        end;

      end;

      hence thesis;

    end;

    theorem :: BINARI_4:34

    ex x be Element of BOOLEAN st ((m + 1) -BinarySequence l) = ((m -BinarySequence l) ^ <*x*>)

    proof

      consider x be Element of BOOLEAN such that

       A1: ( 2sComplement ((m + 1),l)) = (( 2sComplement (m,l)) ^ <*x*>) by Th33;

      

       A2: |.l.| = l by ABSVALUE:def 1;

      

      then ((m + 1) -BinarySequence l) = (( 2sComplement (m,l)) ^ <*x*>) by A1, Def2

      .= ((m -BinarySequence l) ^ <*x*>) by A2, Def2;

      hence thesis;

    end;

    theorem :: BINARI_4:35

    

     Th35: for n be non zero Nat holds ( - (2 to_power n)) <= (h + i) & h < 0 & i < 0 & ( - (2 to_power (n -' 1))) <= h & ( - (2 to_power (n -' 1))) <= i implies (( carry (( 2sComplement ((n + 1),h)),( 2sComplement ((n + 1),i)))) /. (n + 1)) = TRUE

    proof

      defpred P[ Nat] means ( - (2 to_power $1)) <= (h + i) & h < 0 & i < 0 & ( - (2 to_power ($1 -' 1))) <= h & ( - (2 to_power ($1 -' 1))) <= i implies (( carry (( 2sComplement (($1 + 1),h)),( 2sComplement (($1 + 1),i)))) /. ($1 + 1)) = TRUE ;

      

       A1: for n be non zero Nat st P[n] holds P[(n + 1)]

      proof

        let n be non zero Nat such that P[n];

        assume that ( - (2 to_power (n + 1))) <= (h + i) and

         A2: h < 0 and

         A3: i < 0 and

         A4: ( - (2 to_power ((n + 1) -' 1))) <= h and

         A5: ( - (2 to_power ((n + 1) -' 1))) <= i;

        set H1 = ( 2sComplement (((n + 1) + 1),h)), I1 = ( 2sComplement (((n + 1) + 1),i)), H = ( 2sComplement ((n + 1),h)), I = ( 2sComplement ((n + 1),i)), T = TRUE , N = (n + 1);

        

         A6: (N -' 1) = (N - 1) by XREAL_0:def 2;

        then

         A7: (2 to_power (N -' 1)) < (2 to_power N) by POWER: 39, XREAL_1: 146;

        ((2 to_power (N -' 1)) + (2 to_power (N -' 1))) = (2 * (2 to_power (N -' 1)))

        .= ((2 to_power 1) * (2 to_power (N -' 1))) by POWER: 25

        .= (2 to_power ( 0 + N)) by A6, POWER: 27;

        then

         A8: (( - (2 to_power (N -' 1))) + (2 to_power N)) = (2 to_power (N -' 1));

        then

         A9: (2 to_power (N -' 1)) <= ((2 to_power N) + h) by A4, XREAL_1: 6;

        

         A10: (2 to_power (N -' 1)) <= ((2 to_power N) + i) by A5, A8, XREAL_1: 6;

        

         A11: ((2 to_power N) + i) < ( 0 + (2 to_power N)) by A3, XREAL_1: 8;

        (N - 1) = n;

        then

         A12: (N -' 1) = n by XREAL_0:def 2;

         0 <= ((2 to_power N) + h) & 0 <= ((2 to_power N) + i) by A4, A5, A8, XREAL_1: 6;

        then

        reconsider NH = ((2 to_power N) + h), NI = ((2 to_power N) + i) as Element of NAT by INT_1: 3;

        

         A13: ( len (N -BinarySequence NI)) = N by CARD_1:def 7;

        

         A14: 1 <= N by NAT_1: 11;

        then

         A15: (H1 /. N) = (H /. N) & (I1 /. N) = (I /. N) by Th32;

        

         A16: ((2 to_power N) + h) < ( 0 + (2 to_power N)) by A2, XREAL_1: 8;

        

         A17: N < (N + 1) by NAT_1: 13;

         |.i.| = ( - i) by A3, ABSVALUE:def 1;

        then ( - ( - (2 to_power (N -' 1)))) >= |.i.| by A5, XREAL_1: 24;

        then ( MajP (N, |.i.|)) = N by A7, Th24, XXREAL_0: 2;

        

        then

         A18: (I /. N) = ((N -BinarySequence |.NI.|) /. N) by A3, Def2

        .= ((N -BinarySequence NI) /. N) by ABSVALUE:def 1

        .= ((N -BinarySequence NI) . N) by A14, A13, FINSEQ_4: 15

        .= T by A12, A10, A11, BINARI_3: 29;

        

         A19: ( len (N -BinarySequence NH)) = N by CARD_1:def 7;

         |.h.| = ( - h) by A2, ABSVALUE:def 1;

        then ( - ( - (2 to_power (N -' 1)))) >= |.h.| by A4, XREAL_1: 24;

        then ( MajP (N, |.h.|)) = N by A7, Th24, XXREAL_0: 2;

        

        then (H /. N) = ((N -BinarySequence |.NH.|) /. N) by A2, Def2

        .= ((N -BinarySequence NH) /. N) by ABSVALUE:def 1

        .= ((N -BinarySequence NH) . N) by A14, A19, FINSEQ_4: 15

        .= T by A12, A9, A16, BINARI_3: 29;

        

        then (( carry (H1,I1)) /. (N + 1)) = (((T '&' T) 'or' (T '&' (( carry (H1,I1)) /. N))) 'or' (T '&' (( carry (H1,I1)) /. N))) by A14, A18, A15, A17, BINARITH:def 2

        .= (T 'or' (( carry (H1,I1)) /. N));

        hence thesis;

      end;

      

       A20: P[1]

      proof

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

        

        then (3 div (2 to_power (1 -' 1))) = ((1 + 2) div 1) by POWER: 24

        .= 3 by NAT_2: 4;

        

        then

         A21: ((3 div (2 to_power (1 -' 1))) mod 2) = ((2 + 1) mod 2)

        .= (((2 mod 2) + 1) mod 2) by NAT_D: 22

        .= (( 0 + 1) mod 2) by NAT_D: 25

        .= 1 by PEPIN: 5;

        

         A22: (( - 2) + 1) = ( - 1);

        set H = ( 2sComplement (2,h)), I = ( 2sComplement (2,i)), T = TRUE ;

        assume that

         A23: ( - (2 to_power 1)) <= (h + i) and

         A24: h < 0 and

         A25: i < 0 and ( - (2 to_power (1 -' 1))) <= h and ( - (2 to_power (1 -' 1))) <= i;

        

         A26: i <= ( - 1) by A25, INT_1: 8;

        ( - (2 to_power 1)) < h by A23, A24, A25, Th9;

        then ( - 2) < h by POWER: 25;

        then

         A27: ( - 1) <= h by A22, INT_1: 7;

        ( - (2 to_power 1)) < i by A23, A24, A25, Th9;

        then ( - 2) < i by POWER: 25;

        then ( - 1) <= i by A22, INT_1: 7;

        then

         A28: i = ( - 1) by A26, XXREAL_0: 1;

        

         A29: 1 in ( Seg 2) by FINSEQ_1: 1;

        

         A30: (2 to_power 2) = (2 |^ (1 + 1)) by POWER: 41

        .= ((2 |^ 1) + (2 |^ 1)) by PEPIN: 29

        .= ((2 to_power 1) + (2 |^ 1)) by POWER: 41

        .= ((2 to_power 1) + (2 to_power 1)) by POWER: 41

        .= (2 + (2 to_power 1)) by POWER: 25

        .= (2 + 2) by POWER: 25;

        

         A31: (2 to_power 2) > (2 to_power 0 ) by POWER: 39;

        

         A32: h <= ( - 1) by A24, INT_1: 8;

        then

         A33: h = ( - 1) by A27, XXREAL_0: 1;

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

        then (2 to_power 0 ) = |.h.| by POWER: 24;

        then ( MajP (2, |.h.|)) = 2 by A31, Th24;

        

        then |.((2 to_power ( MajP (2, |.h.|))) + h).| = |.(4 + ( - 1)).| by A27, A32, A30, XXREAL_0: 1

        .= 3 by ABSVALUE:def 1;

        

        then (( 2sComplement (2,h)) /. 1) = ((2 -BinarySequence 3) /. 1) by A24, Def2

        .= ( IFEQ (1, 0 , FALSE , TRUE )) by A21, A29, BINARI_3:def 1

        .= TRUE by FUNCOP_1:def 8;

        

        then (( carry (H,I)) /. (1 + 1)) = (((T '&' T) 'or' (T '&' (( carry (H,I)) /. 1))) 'or' (T '&' (( carry (H,I)) /. 1))) by A33, A28, BINARITH:def 2

        .= (T 'or' (( carry (H,I)) /. 1));

        hence thesis;

      end;

      thus for n be non zero Nat holds P[n] from NAT_1:sch 10( A20, A1);

    end;

    theorem :: BINARI_4:36

    for n be non zero Nat st (h + i) <= ((2 to_power (n -' 1)) - 1) & h >= 0 & i >= 0 holds ( Intval (( 2sComplement (n,h)) + ( 2sComplement (n,i)))) = (h + i)

    proof

      let n be non zero Nat such that

       A1: (h + i) <= ((2 to_power (n -' 1)) - 1) and

       A2: h >= 0 & i >= 0 ;

      reconsider h, i as Element of NAT by A2, INT_1: 3;

      

       A3: ( 2sComplement (n,i)) = (n -BinarySequence |.i.|) by Def2

      .= (n -BinarySequence i) by ABSVALUE:def 1;

      ( 2sComplement (n,h)) = (n -BinarySequence |.h.|) by Def2

      .= (n -BinarySequence h) by ABSVALUE:def 1;

      hence thesis by A1, A3, Th14;

    end;

    theorem :: BINARI_4:37

    for n be non zero Nat st ( - (2 to_power ((n + 1) -' 1))) <= (h + i) & h < 0 & i < 0 & ( - (2 to_power (n -' 1))) <= h & ( - (2 to_power (n -' 1))) <= i holds ( Intval (( 2sComplement ((n + 1),h)) + ( 2sComplement ((n + 1),i)))) = (h + i)

    proof

      let n be non zero Nat such that

       A1: ( - (2 to_power ((n + 1) -' 1))) <= (h + i) and

       A2: h < 0 and

       A3: i < 0 and

       A4: ( - (2 to_power (n -' 1))) <= h & ( - (2 to_power (n -' 1))) <= i;

      

       A5: ((2 to_power (n + 1)) + ( - (2 to_power n))) = (( - (2 to_power n)) + ((2 to_power 1) * (2 to_power n))) by POWER: 27

      .= (( - (2 to_power n)) + (2 * (2 to_power n))) by POWER: 25

      .= (2 to_power n);

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

      then

       A6: ( - (2 to_power n)) <= (h + i) by A1, XREAL_0:def 2;

      then

       A7: ( - (2 to_power n)) < h by A2, A3, Th9;

      then

       A8: (2 to_power n) <= ((2 to_power (n + 1)) + h) by A5, XREAL_1: 6;

      

       A9: ( - (2 to_power n)) < i by A2, A3, A6, Th9;

      then

       A10: 0 <= ((2 to_power (n + 1)) + i) by A5, XREAL_1: 6;

       0 <= ((2 to_power (n + 1)) + h) by A7, A5, XREAL_1: 6;

      then

      reconsider NH = ((2 to_power (n + 1)) + h), NI = ((2 to_power (n + 1)) + i) as Element of NAT by A10, INT_1: 3;

      

       A11: 1 <= (n + 1) by NAT_1: 11;

      set H = ( 2sComplement (n,h)), I = ( 2sComplement (n,i)), H1 = ( 2sComplement ((n + 1),h)), I1 = ( 2sComplement ((n + 1),i)), F = FALSE , T = TRUE ;

      n < (n + 1) by XREAL_1: 29;

      then

       A12: (2 to_power n) < (2 to_power (n + 1)) by POWER: 39;

      

       A13: (ex a be Element of BOOLEAN st H1 = (H ^ <*a*>)) & ex a be Element of BOOLEAN st I1 = (I ^ <*a*>) by Th33;

      

       A14: ((2 to_power (n + 1)) + h) < ((2 to_power (n + 1)) + 0 ) by A2, XREAL_1: 8;

      ( - h) < ( - ( - (2 to_power n))) by A7, XREAL_1: 24;

      then |.h.| < (2 to_power n) by A2, ABSVALUE:def 1;

      then

       A15: ( MajP ((n + 1), |.h.|)) = (n + 1) by A12, Th24, XXREAL_0: 2;

      

      then

       A16: H1 = ((n + 1) -BinarySequence |.((2 to_power (n + 1)) + h).|) by A2, Def2

      .= ((n + 1) -BinarySequence NH) by ABSVALUE:def 1;

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

      

      then

       A17: (H1 /. (n + 1)) = (H1 . (n + 1)) by A11, FINSEQ_4: 15

      .= (((n + 1) -BinarySequence |.((2 to_power (n + 1)) + h).|) . (n + 1)) by A2, A15, Def2

      .= (((n + 1) -BinarySequence NH) . (n + 1)) by ABSVALUE:def 1

      .= T by A14, A8, BINARI_3: 29;

      

       A18: (2 to_power n) <= ((2 to_power (n + 1)) + i) by A9, A5, XREAL_1: 6;

      

       A19: ((2 to_power (n + 1)) + i) < ((2 to_power (n + 1)) + 0 ) by A3, XREAL_1: 8;

      ( - i) < ( - ( - (2 to_power n))) by A9, XREAL_1: 24;

      then |.i.| < (2 to_power n) by A3, ABSVALUE:def 1;

      then

       A20: ( MajP ((n + 1), |.i.|)) = (n + 1) by A12, Th24, XXREAL_0: 2;

      

      then

       A21: I1 = ((n + 1) -BinarySequence |.((2 to_power (n + 1)) + i).|) by A3, Def2

      .= ((n + 1) -BinarySequence NI) by ABSVALUE:def 1;

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

      

      then

       A22: (I1 /. (n + 1)) = (I1 . (n + 1)) by A11, FINSEQ_4: 15

      .= (((n + 1) -BinarySequence |.((2 to_power (n + 1)) + i).|) . (n + 1)) by A3, A20, Def2

      .= (((n + 1) -BinarySequence NI) . (n + 1)) by ABSVALUE:def 1

      .= T by A19, A18, BINARI_3: 29;

      

      then

       A23: ( Intval I1) = (( Absval I1) - (2 to_power (n + 1))) by BINARI_2:def 3

      .= (NI - (2 to_power (n + 1))) by A19, A21, BINARI_3: 35

      .= i;

      

       A24: (( carry (H1,I1)) /. (n + 1)) = T by A2, A3, A4, A6, Th35;

      

      then

       A25: ( Int_add_ovfl (H1,I1)) = ((F '&' ( 'not' T)) '&' T) by A17, A22, BINARI_2:def 4

      .= F;

      

       A26: ( Int_add_udfl (H1,I1)) = ((T '&' T) '&' ( 'not' T)) by A17, A22, A24, BINARI_2:def 5

      .= F;

      ( Intval H1) = (( Absval H1) - (2 to_power (n + 1))) by A17, BINARI_2:def 3

      .= (NH - (2 to_power (n + 1))) by A14, A16, BINARI_3: 35

      .= h;

      

      then ( Intval (H1 + I1)) = (((h + i) - ( IFEQ (F,F, 0 ,(2 to_power (n + 1))))) + ( IFEQ (F,F, 0 ,(2 to_power (n + 1))))) by A13, A23, A25, A26, BINARI_2: 12

      .= (((h + i) - 0 ) + 0 );

      hence thesis;

    end;

    theorem :: BINARI_4:38

    for n be non zero Nat holds ( - (2 to_power (n -' 1))) <= h & h <= ((2 to_power (n -' 1)) - 1) & ( - (2 to_power (n -' 1))) <= i & i <= ((2 to_power (n -' 1)) - 1) & ( - (2 to_power (n -' 1))) <= (h + i) & (h + i) <= ((2 to_power (n -' 1)) - 1) & (h >= 0 & i < 0 or h < 0 & i >= 0 ) implies ( Intval (( 2sComplement (n,h)) + ( 2sComplement (n,i)))) = (h + i)

    proof

      defpred P[ non zero Nat] means ( - (2 to_power ($1 -' 1))) <= h & h <= ((2 to_power ($1 -' 1)) - 1) & ( - (2 to_power ($1 -' 1))) <= i & i <= ((2 to_power ($1 -' 1)) - 1) & ( - (2 to_power ($1 -' 1))) <= (h + i) & (h + i) <= ((2 to_power ($1 -' 1)) - 1) & ((h >= 0 & i < 0 ) or (h < 0 & i >= 0 )) implies ( Intval (( 2sComplement ($1,h)) + ( 2sComplement ($1,i)))) = (h + i);

      

       A1: for n be non zero Nat st P[n] holds P[(n + 1)]

      proof

        let n be non zero Nat such that ( - (2 to_power (n -' 1))) <= h & h <= ((2 to_power (n -' 1)) - 1) & ( - (2 to_power (n -' 1))) <= i & i <= ((2 to_power (n -' 1)) - 1) & ( - (2 to_power (n -' 1))) <= (h + i) & (h + i) <= ((2 to_power (n -' 1)) - 1) & (h >= 0 & i < 0 or h < 0 & i >= 0 ) implies ( Intval (( 2sComplement (n,h)) + ( 2sComplement (n,i)))) = (h + i);

        assume that

         A2: ( - (2 to_power ((n + 1) -' 1))) <= h and

         A3: h <= ((2 to_power ((n + 1) -' 1)) - 1) and

         A4: ( - (2 to_power ((n + 1) -' 1))) <= i and

         A5: i <= ((2 to_power ((n + 1) -' 1)) - 1) and ( - (2 to_power ((n + 1) -' 1))) <= (h + i) and (h + i) <= ((2 to_power ((n + 1) -' 1)) - 1) and

         A6: h >= 0 & i < 0 or h < 0 & i >= 0 ;

        set H = ( 2sComplement (n,h)), I = ( 2sComplement (n,i)), H1 = ( 2sComplement ((n + 1),h)), I1 = ( 2sComplement ((n + 1),i)), n2 = (2 to_power n), F = FALSE , T = TRUE ;

        

         A7: ((n + 1) - 1) = n;

        then

         A8: ( - n2) <= h by A2, XREAL_0:def 2;

        

         A9: i <= (n2 - 1) by A5, A7, XREAL_0:def 2;

        

         A10: (ex a be Element of BOOLEAN st H1 = (H ^ <*a*>)) & ex b be Element of BOOLEAN st I1 = (I ^ <*b*>) by Th33;

        

         A11: ( - n2) <= i by A4, A7, XREAL_0:def 2;

        

         A12: h <= (n2 - 1) by A3, A7, XREAL_0:def 2;

        now

          per cases by A6;

            suppose

             A13: h >= 0 & i < 0 ;

            ((2 to_power (n + 1)) + ( - (2 to_power n))) = (( - (2 to_power n)) + ((2 to_power 1) * (2 to_power n))) by POWER: 27

            .= (( - (2 to_power n)) + (2 * (2 to_power n))) by POWER: 25

            .= (2 to_power n);

            then

             A14: (2 to_power n) <= ((2 to_power (n + 1)) + i) by A11, XREAL_1: 6;

            then

            reconsider NI = ((2 to_power (n + 1)) + i) as Element of NAT by INT_1: 3;

            n < (n + 1) by XREAL_1: 29;

            then

             A15: (2 to_power n) < (2 to_power (n + 1)) by POWER: 39;

             |.i.| = ( - i) by A13, ABSVALUE:def 1;

            then |.i.| <= ( - ( - (2 to_power n))) by A11, XREAL_1: 24;

            then

             A16: ( MajP ((n + 1), |.i.|)) = (n + 1) by A15, Th24, XXREAL_0: 2;

            

            then

             A17: I1 = ((n + 1) -BinarySequence |.((2 to_power (n + 1)) + i).|) by A13, Def2

            .= ((n + 1) -BinarySequence NI) by ABSVALUE:def 1;

            

             A18: ((2 to_power (n + 1)) + i) < ((2 to_power (n + 1)) + 0 ) by A13, XREAL_1: 8;

            reconsider h as Element of NAT by A13, INT_1: 3;

            

             A19: h < (2 to_power n) by A12, XREAL_1: 146, XXREAL_0: 2;

            

             A20: H1 = ((n + 1) -BinarySequence |.h.|) by Def2

            .= ((n + 1) -BinarySequence h) by ABSVALUE:def 1;

            then

             A21: (H1 . (n + 1)) = F by A19, BINARI_3: 26;

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

            then (2 to_power n) < (2 to_power (n + 1)) by POWER: 39;

            then

             A22: h < (2 to_power (n + 1)) by A19, XXREAL_0: 2;

            

             A23: 1 <= (n + 1) by NAT_1: 11;

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

            then

             A24: (I1 /. (n + 1)) = (I1 . (n + 1)) by A23, FINSEQ_4: 15;

            

             A25: (I1 . (n + 1)) = (((n + 1) -BinarySequence |.((2 to_power (n + 1)) + i).|) . (n + 1)) by A13, A16, Def2

            .= (((n + 1) -BinarySequence NI) . (n + 1)) by ABSVALUE:def 1

            .= T by A18, A14, BINARI_3: 29;

            

            then

             A26: ( Intval I1) = (( Absval I1) - (2 to_power (n + 1))) by A24, BINARI_2:def 3

            .= (NI - (2 to_power (n + 1))) by A18, A17, BINARI_3: 35

            .= i;

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

            then

             A27: (H1 /. (n + 1)) = (H1 . (n + 1)) by A23, FINSEQ_4: 15;

            

            then

             A28: ( Int_add_ovfl (H1,I1)) = ((( 'not' F) '&' ( 'not' T)) '&' (( carry (H1,I1)) /. (n + 1))) by A21, A25, A24, BINARI_2:def 4

            .= F;

            

             A29: ( Int_add_udfl (H1,I1)) = ((F '&' T) '&' ( 'not' (( carry (H1,I1)) /. (n + 1)))) by A21, A25, A27, A24, BINARI_2:def 5

            .= F;

            ( Intval H1) = ( Absval H1) by A21, A27, BINARI_2:def 3

            .= h by A20, A22, BINARI_3: 35;

            

            then ( Intval (H1 + I1)) = (((h + i) - ( IFEQ (F,F, 0 ,(2 to_power (n + 1))))) + ( IFEQ (F,F, 0 ,(2 to_power (n + 1))))) by A10, A26, A28, A29, BINARI_2: 12

            .= (((h + i) - 0 ) + 0 );

            hence thesis;

          end;

            suppose

             A30: h < 0 & i >= 0 ;

            ((2 to_power (n + 1)) + ( - (2 to_power n))) = (( - (2 to_power n)) + ((2 to_power 1) * (2 to_power n))) by POWER: 27

            .= (( - (2 to_power n)) + (2 * (2 to_power n))) by POWER: 25

            .= (2 to_power n);

            then

             A31: (2 to_power n) <= ((2 to_power (n + 1)) + h) by A8, XREAL_1: 6;

            then

            reconsider NH = ((2 to_power (n + 1)) + h) as Element of NAT by INT_1: 3;

            n < (n + 1) by XREAL_1: 29;

            then

             A32: (2 to_power n) < (2 to_power (n + 1)) by POWER: 39;

             |.h.| = ( - h) by A30, ABSVALUE:def 1;

            then |.h.| <= ( - ( - (2 to_power n))) by A8, XREAL_1: 24;

            then

             A33: ( MajP ((n + 1), |.h.|)) = (n + 1) by A32, Th24, XXREAL_0: 2;

            

            then

             A34: H1 = ((n + 1) -BinarySequence |.((2 to_power (n + 1)) + h).|) by A30, Def2

            .= ((n + 1) -BinarySequence NH) by ABSVALUE:def 1;

            

             A35: ((2 to_power (n + 1)) + h) < ((2 to_power (n + 1)) + 0 ) by A30, XREAL_1: 8;

            reconsider i as Element of NAT by A30, INT_1: 3;

            

             A36: i < (2 to_power n) by A9, XREAL_1: 146, XXREAL_0: 2;

            

             A37: I1 = ((n + 1) -BinarySequence |.i.|) by Def2

            .= ((n + 1) -BinarySequence i) by ABSVALUE:def 1;

            then

             A38: (I1 . (n + 1)) = F by A36, BINARI_3: 26;

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

            then (2 to_power n) < (2 to_power (n + 1)) by POWER: 39;

            then

             A39: i < (2 to_power (n + 1)) by A36, XXREAL_0: 2;

            

             A40: 1 <= (n + 1) by NAT_1: 11;

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

            then

             A41: (H1 /. (n + 1)) = (H1 . (n + 1)) by A40, FINSEQ_4: 15;

            

             A42: (H1 . (n + 1)) = (((n + 1) -BinarySequence |.((2 to_power (n + 1)) + h).|) . (n + 1)) by A30, A33, Def2

            .= (((n + 1) -BinarySequence NH) . (n + 1)) by ABSVALUE:def 1

            .= T by A35, A31, BINARI_3: 29;

            

            then

             A43: ( Intval H1) = (( Absval H1) - (2 to_power (n + 1))) by A41, BINARI_2:def 3

            .= (NH - (2 to_power (n + 1))) by A35, A34, BINARI_3: 35

            .= h;

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

            then

             A44: (I1 /. (n + 1)) = (I1 . (n + 1)) by A40, FINSEQ_4: 15;

            

            then

             A45: ( Int_add_ovfl (H1,I1)) = ((( 'not' T) '&' ( 'not' F)) '&' (( carry (H1,I1)) /. (n + 1))) by A38, A42, A41, BINARI_2:def 4

            .= F;

            

             A46: ( Int_add_udfl (H1,I1)) = ((T '&' F) '&' ( 'not' (( carry (H1,I1)) /. (n + 1)))) by A38, A42, A44, A41, BINARI_2:def 5

            .= F;

            ( Intval I1) = ( Absval I1) by A38, A44, BINARI_2:def 3

            .= i by A37, A39, BINARI_3: 35;

            

            then ( Intval (H1 + I1)) = (((h + i) - ( IFEQ (F,F, 0 ,(2 to_power (n + 1))))) + ( IFEQ (F,F, 0 ,(2 to_power (n + 1))))) by A10, A43, A45, A46, BINARI_2: 12

            .= (((h + i) - 0 ) + 0 );

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A47: P[1]

      proof

        

         A48: |.( - 1).| = ( - ( - 1)) by ABSVALUE:def 1

        .= 1;

        (2 to_power 1) = 2 & for k be Nat st (2 to_power k) >= 1 & k >= 1 holds k >= 1 by POWER: 25;

        then ( MajP (1, |.( - 1).|)) = 1 by A48, Def1;

        

        then

         A49: ( 2sComplement (1,( - 1))) = (1 -BinarySequence |.((2 to_power 1) + ( - 1)).|) by Def2

        .= (1 -BinarySequence |.(2 + ( - 1)).|) by POWER: 25

        .= (1 -BinarySequence 1) by ABSVALUE:def 1

        .= (( 0 + 1) -BinarySequence (2 to_power 0 )) by POWER: 24

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

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

        assume that

         A50: ( - (2 to_power (1 -' 1))) <= h and

         A51: h <= ((2 to_power (1 -' 1)) - 1) and

         A52: ( - (2 to_power (1 -' 1))) <= i and

         A53: i <= ((2 to_power (1 -' 1)) - 1) and ( - (2 to_power (1 -' 1))) <= (h + i) and (h + i) <= ((2 to_power (1 -' 1)) - 1) and

         A54: h >= 0 & i < 0 or h < 0 & i >= 0 ;

        

         A55: (1 -' 1) = (1 - 1) by XREAL_0:def 2

        .= 0 ;

        then

         A56: h <= (1 - 1) by A51, POWER: 24;

        

         A57: i <= (1 - 1) by A53, A55, POWER: 24;

        

         A58: ( - 1) <= i by A52, A55, POWER: 24;

        

         A59: ( 2sComplement (1, 0 )) = (1 -BinarySequence |. 0 .|) by Def2

        .= (1 -BinarySequence 0 ) by ABSVALUE:def 1

        .= ( 0* 1) by BINARI_3: 25

        .= <* FALSE *> by FINSEQ_2: 59;

        

         A60: ( - 1) <= h by A50, A55, POWER: 24;

        now

          per cases by A54;

            suppose

             A61: h >= 0 & i < 0 ;

            then i <= ( - 1) by INT_1: 8;

            then

             A62: i = ( - 1) by A58, XXREAL_0: 1;

            h = 0 by A56, A61;

            hence thesis by A59, A49, A62, Th15, BINARI_3: 17;

          end;

            suppose

             A63: h < 0 & i >= 0 ;

            then h <= ( - 1) by INT_1: 8;

            then

             A64: h = ( - 1) by A60, XXREAL_0: 1;

            i = 0 by A57, A63;

            hence thesis by A59, A49, A64, Th15, BINARI_3: 17;

          end;

        end;

        hence thesis;

      end;

      thus for n be non zero Nat holds P[n] from NAT_1:sch 10( A47, A1);

    end;