binari_3.miz



    begin

    theorem :: BINARI_3:1

    

     Th1: for n be non zero Nat holds for F be Tuple of n, BOOLEAN holds ( Absval F) < (2 to_power n)

    proof

      defpred P[ non zero Nat] means for F be Tuple of $1, BOOLEAN holds ( Absval F) < (2 to_power $1);

      

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

      proof

        let n be non zero Nat;

        assume

         A2: P[n];

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

        then

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

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

        consider T be Element of (n -tuples_on BOOLEAN ), d be Element of BOOLEAN such that

         A4: F = (T ^ <*d*>) by FINSEQ_2: 117;

        

         A5: ( Absval F) = (( Absval T) + ( IFEQ (d, FALSE , 0 ,(2 to_power n)))) by A4, BINARITH: 20;

        

         A6: ( Absval T) < (2 to_power n) by A2;

        per cases by XBOOLEAN:def 3;

          suppose d = FALSE ;

          then ( Absval F) = (( Absval T) + 0 ) by A5, FUNCOP_1:def 8;

          then (( Absval F) + (2 to_power n)) < ((2 to_power n) + (2 to_power (n + 1))) by A2, A3, XREAL_1: 8;

          hence thesis by XREAL_1: 6;

        end;

          suppose d = TRUE ;

          then ( Absval F) = (( Absval T) + (2 to_power n)) by A5, FUNCOP_1:def 8;

          then ( Absval F) < ((2 to_power n) + (2 to_power n)) by A6, XREAL_1: 6;

          then ( Absval F) < ((2 to_power n) * 2);

          then ( Absval F) < ((2 to_power n) * (2 to_power 1)) by POWER: 25;

          hence thesis by POWER: 27;

        end;

      end;

      

       A7: P[1]

      proof

        let F be Tuple of 1, BOOLEAN ;

        consider d be Element of BOOLEAN such that

         A8: F = <*d*> by FINSEQ_2: 97;

        d = TRUE or d = FALSE by XBOOLEAN:def 3;

        then ( Absval F) = 1 or ( Absval F) = 0 by A8, BINARITH: 15, BINARITH: 16;

        then ( Absval F) < 2;

        hence thesis by POWER: 25;

      end;

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

    end;

    theorem :: BINARI_3:2

    

     Th2: for n be non zero Nat holds for F1,F2 be Tuple of n, BOOLEAN st ( Absval F1) = ( Absval F2) holds F1 = F2

    proof

      defpred P[ non zero Nat] means for F1,F2 be Tuple of $1, BOOLEAN st ( Absval F1) = ( Absval F2) holds F1 = F2;

      

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

      proof

        let k be non zero Nat;

        assume

         A2: for F1,F2 be Tuple of k, BOOLEAN st ( Absval F1) = ( Absval F2) holds F1 = F2;

        let F1,F2 be Tuple of (k + 1), BOOLEAN ;

        consider T1 be Element of (k -tuples_on BOOLEAN ), d1 be Element of BOOLEAN such that

         A3: F1 = (T1 ^ <*d1*>) by FINSEQ_2: 117;

        assume

         A4: ( Absval F1) = ( Absval F2);

        consider T2 be Element of (k -tuples_on BOOLEAN ), d2 be Element of BOOLEAN such that

         A5: F2 = (T2 ^ <*d2*>) by FINSEQ_2: 117;

        

         A6: (( Absval T1) + ( IFEQ (d1, FALSE , 0 ,(2 to_power k)))) = ( Absval F1) by A3, BINARITH: 20

        .= (( Absval T2) + ( IFEQ (d2, FALSE , 0 ,(2 to_power k)))) by A5, A4, BINARITH: 20;

        d1 = d2

        proof

          assume

           A7: d1 <> d2;

          per cases by XBOOLEAN:def 3;

            suppose

             A8: d1 = FALSE ;

            then

             A9: ( IFEQ (d1, FALSE , 0 qua Real,(2 to_power k))) = 0 by FUNCOP_1:def 8;

            ( IFEQ (d2, FALSE , 0 qua Real,(2 to_power k))) = (2 to_power k) by A7, A8, FUNCOP_1:def 8;

            hence contradiction by A6, A9, Th1, NAT_1: 11;

          end;

            suppose

             A10: d1 = TRUE ;

            then d2 = FALSE by A7, XBOOLEAN:def 3;

            then

             A11: ( IFEQ (d2, FALSE , 0 qua Real,(2 to_power k))) = 0 by FUNCOP_1:def 8;

            ( IFEQ (d1, FALSE , 0 qua Real,(2 to_power k))) = (2 to_power k) by A10, FUNCOP_1:def 8;

            hence contradiction by A6, A11, Th1, NAT_1: 11;

          end;

        end;

        hence thesis by A2, A3, A5, A6, XCMPLX_1: 2;

      end;

      

       A12: P[1]

      proof

        let F1,F2 be Tuple of 1, BOOLEAN ;

        consider d1 be Element of BOOLEAN such that

         A13: F1 = <*d1*> by FINSEQ_2: 97;

        assume

         A14: ( Absval F1) = ( Absval F2);

        assume

         A15: F1 <> F2;

        consider d2 be Element of BOOLEAN such that

         A16: F2 = <*d2*> by FINSEQ_2: 97;

        per cases by XBOOLEAN:def 3;

          suppose

           A17: d1 = FALSE ;

          then

           A18: ( Absval F1) = 0 by A13, BINARITH: 15;

          d2 = TRUE by A13, A16, A15, A17, XBOOLEAN:def 3;

          hence contradiction by A16, A14, A18, BINARITH: 16;

        end;

          suppose

           A19: d1 = TRUE ;

          then

           A20: ( Absval F1) = 1 by A13, BINARITH: 16;

          d2 = FALSE by A13, A16, A15, A19, XBOOLEAN:def 3;

          hence contradiction by A16, A14, A20, BINARITH: 15;

        end;

      end;

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

    end;

    theorem :: BINARI_3:3

    for t1,t2 be FinSequence st ( Rev t1) = ( Rev t2) holds t1 = t2

    proof

      let t1,t2 be FinSequence;

      assume

       A1: ( Rev t1) = ( Rev t2);

      

      thus t1 = ( Rev ( Rev t1))

      .= t2 by A1;

    end;

    theorem :: BINARI_3:4

    

     Th4: for n be Nat holds ( 0* n) in ( BOOLEAN * )

    proof

      let n be Nat;

      (n |-> FALSE ) is FinSequence of BOOLEAN ;

      hence thesis by FINSEQ_1:def 11;

    end;

    theorem :: BINARI_3:5

    

     Th5: for n be Nat holds for y be Tuple of n, BOOLEAN st y = ( 0* n) holds ( 'not' y) = (n |-> 1)

    proof

      let n be Nat;

      let y be Tuple of n, BOOLEAN ;

      assume

       A1: y = ( 0* n);

       A2:

      now

        

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

        let i be Nat;

        assume that

         A4: 1 <= i and

         A5: i <= ( len ( 'not' y));

        

         A6: ( len ( 'not' y)) = n by CARD_1:def 7;

        then

         A7: i in ( Seg n) by A4, A5, FINSEQ_1: 1;

        then

         A8: (y . i) = FALSE by A1, FUNCOP_1: 7;

        

        thus (( 'not' y) . i) = (( 'not' y) /. i) by A4, A5, FINSEQ_4: 15

        .= ( 'not' (y /. i)) by A7, BINARITH:def 1

        .= ( 'not' FALSE ) by A4, A5, A6, A3, A8, FINSEQ_4: 15

        .= ((n |-> 1) . i) by A7, FUNCOP_1: 7;

      end;

      ( len ( 'not' y)) = n by CARD_1:def 7

      .= ( len (n |-> 1)) by CARD_1:def 7;

      hence thesis by A2, FINSEQ_1: 14;

    end;

    theorem :: BINARI_3:6

    

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

    proof

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

      

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

      proof

        let n be non zero Nat;

        assume

         A2: for F be Tuple of n, BOOLEAN st F = ( 0* n) holds ( Absval F) = 0 ;

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

        ( 0* n) in ( BOOLEAN * ) by Th4;

        then ( 0* n) is FinSequence of BOOLEAN by FINSEQ_1:def 11;

        then

        reconsider F1 = ( 0* n) as Tuple of n, BOOLEAN ;

        assume F = ( 0* (n + 1));

        

        hence ( Absval F) = ( Absval (F1 ^ <* FALSE *>)) by FINSEQ_2: 60

        .= (( Absval F1) + ( IFEQ ( FALSE , FALSE , 0 ,(2 to_power n)))) by BINARITH: 20

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

        .= 0 by FUNCOP_1:def 8;

      end;

      

       A3: P[1] by BINARITH: 15, FINSEQ_2: 59;

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

    end;

    theorem :: BINARI_3:7

    for n be non zero Nat holds for F be Tuple of n, BOOLEAN st F = ( 0* n) holds ( Absval ( 'not' F)) = ((2 to_power n) - 1)

    proof

      let n be non zero Nat;

      let F be Tuple of n, BOOLEAN ;

      assume

       A1: F = ( 0* n);

      

      thus ( Absval ( 'not' F)) = ((( - ( Absval F)) + (2 to_power n)) - 1) by BINARI_2: 13

      .= ((( - 0 ) + (2 to_power n)) - 1) by A1, Th6

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

    end;

    theorem :: BINARI_3:8

    for n be Nat holds ( Rev ( 0* n)) = ( 0* n)

    proof

      let n be Nat;

       A1:

      now

        let k be Nat;

        assume

         A2: k in ( dom ( 0* n));

        then k in ( Seg ( len ( 0* n))) by FINSEQ_1:def 3;

        then

         A3: k in ( Seg n) by CARD_1:def 7;

        then ((n - k) + 1) in ( Seg n) by FINSEQ_5: 2;

        then

         A4: ((( len ( 0* n)) - k) + 1) in ( Seg n) by CARD_1:def 7;

        

        thus (( Rev ( 0* n)) . k) = (( 0* n) . ((( len ( 0* n)) - k) + 1)) by A2, FINSEQ_5: 58

        .= 0 by A4, FUNCOP_1: 7

        .= (( 0* n) . k) by A3, FUNCOP_1: 7;

      end;

      ( dom ( Rev ( 0* n))) = ( Seg ( len ( Rev ( 0* n)))) by FINSEQ_1:def 3

      .= ( Seg ( len ( 0* n))) by FINSEQ_5:def 3

      .= ( dom ( 0* n)) by FINSEQ_1:def 3;

      hence thesis by A1, FINSEQ_1: 13;

    end;

    theorem :: BINARI_3:9

    for n be Nat holds for y be Tuple of n, BOOLEAN st y = ( 0* n) holds ( Rev ( 'not' y)) = ( 'not' y)

    proof

      let n be Nat;

      let y be Tuple of n, BOOLEAN ;

      assume

       A1: y = ( 0* n);

       A2:

      now

        let k be Nat;

        assume

         A3: k in ( dom ( 'not' y));

        then k in ( Seg ( len ( 'not' y))) by FINSEQ_1:def 3;

        then

         A4: k in ( Seg n) by CARD_1:def 7;

        then ((n - k) + 1) in ( Seg n) by FINSEQ_5: 2;

        then

         A5: ((( len ( 'not' y)) - k) + 1) in ( Seg n) by CARD_1:def 7;

        

        thus (( Rev ( 'not' y)) . k) = (( 'not' y) . ((( len ( 'not' y)) - k) + 1)) by A3, FINSEQ_5: 58

        .= ((n |-> 1) . ((( len ( 'not' y)) - k) + 1)) by A1, Th5

        .= 1 by A5, FUNCOP_1: 7

        .= ((n |-> 1) . k) by A4, FUNCOP_1: 7

        .= (( 'not' y) . k) by A1, Th5;

      end;

      ( dom ( Rev ( 'not' y))) = ( Seg ( len ( Rev ( 'not' y)))) by FINSEQ_1:def 3

      .= ( Seg ( len ( 'not' y))) by FINSEQ_5:def 3

      .= ( dom ( 'not' y)) by FINSEQ_1:def 3;

      hence thesis by A2, FINSEQ_1: 13;

    end;

    theorem :: BINARI_3:10

    

     Th10: ( Bin1 1) = <* TRUE *>

    proof

      1 in ( Seg 1) by FINSEQ_1: 3;

      then

       A1: (( Bin1 1) /. 1) = TRUE by BINARI_2: 5;

      ex d be Element of BOOLEAN st ( Bin1 1) = <*d*> by FINSEQ_2: 97;

      hence thesis by A1, FINSEQ_4: 16;

    end;

    theorem :: BINARI_3:11

    

     Th11: for n be non zero Nat holds ( Absval ( Bin1 n)) = 1

    proof

      defpred P[ Nat] means ( Absval ( Bin1 $1)) = 1;

      

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

      proof

        let n be non zero Nat;

        assume

         A2: ( Absval ( Bin1 n)) = 1;

        

        thus ( Absval ( Bin1 (n + 1))) = ( Absval (( Bin1 n) ^ <* FALSE *>)) by BINARI_2: 7

        .= (( Absval ( Bin1 n)) + ( IFEQ ( FALSE , FALSE , 0 ,(2 to_power n)))) by BINARITH: 20

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

        .= 1 by A2;

      end;

      

       A3: P[1] by Th10, BINARITH: 16;

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

    end;

    theorem :: BINARI_3:12

    

     Th12: for x,y be Element of BOOLEAN holds ((x 'or' y) = TRUE iff x = TRUE or y = TRUE ) & ((x 'or' y) = FALSE iff x = FALSE & y = FALSE )

    proof

      let x,y be Element of BOOLEAN ;

      thus (x 'or' y) = TRUE implies x = TRUE or y = TRUE

      proof

        assume (x 'or' y) = TRUE ;

        then ( 'not' x) = FALSE or ( 'not' y) = FALSE by MARGREL1: 12;

        hence thesis;

      end;

      thus x = TRUE or y = TRUE implies (x 'or' y) = TRUE ;

      thus (x 'or' y) = FALSE implies x = FALSE & y = FALSE

      proof

        assume

         A1: (x 'or' y) = FALSE ;

        then ( 'not' x) = TRUE by MARGREL1: 12;

        hence thesis by A1;

      end;

      thus thesis;

    end;

    theorem :: BINARI_3:13

    

     Th13: for x,y be Element of BOOLEAN holds ( add_ovfl ( <*x*>, <*y*>)) = TRUE iff x = TRUE & y = TRUE

    proof

      let x,y be Element of BOOLEAN ;

      

       A1: (( <* TRUE *> /. 1) '&' ( <* TRUE *> /. 1)) = TRUE by FINSEQ_4: 16;

      thus ( add_ovfl ( <*x*>, <*y*>)) = TRUE implies x = TRUE & y = TRUE

      proof

        assume ( add_ovfl ( <*x*>, <*y*>)) = TRUE ;

        then (((( <*x*> /. 1) '&' ( <*y*> /. 1)) 'or' (( <*x*> /. 1) '&' (( carry ( <*x*>, <*y*>)) /. 1))) 'or' (( <*y*> /. 1) '&' (( carry ( <*x*>, <*y*>)) /. 1))) = TRUE by BINARITH:def 6;

        then

         A2: ((( <*x*> /. 1) '&' ( <*y*> /. 1)) 'or' (( <*x*> /. 1) '&' (( carry ( <*x*>, <*y*>)) /. 1))) = TRUE or (( <*y*> /. 1) '&' (( carry ( <*x*>, <*y*>)) /. 1)) = TRUE by Th12;

        now

          per cases by A2, Th12;

            suppose

             A3: (( <*x*> /. 1) '&' ( <*y*> /. 1)) = TRUE ;

            then ( <*x*> /. 1) = TRUE by MARGREL1: 12;

            hence thesis by A3, FINSEQ_4: 16;

          end;

            suppose (( <*x*> /. 1) '&' (( carry ( <*x*>, <*y*>)) /. 1)) = TRUE ;

            then (( carry ( <*x*>, <*y*>)) /. 1) = TRUE by MARGREL1: 12;

            hence thesis by BINARITH:def 2;

          end;

            suppose (( <*y*> /. 1) '&' (( carry ( <*x*>, <*y*>)) /. 1)) = TRUE ;

            then (( carry ( <*x*>, <*y*>)) /. 1) = TRUE by MARGREL1: 12;

            hence thesis by BINARITH:def 2;

          end;

        end;

        hence thesis;

      end;

      assume that

       A4: x = TRUE and

       A5: y = TRUE ;

      

      thus ( add_ovfl ( <*x*>, <*y*>)) = (((( <* TRUE *> /. 1) '&' ( <* TRUE *> /. 1)) 'or' (( <* TRUE *> /. 1) '&' (( carry ( <* TRUE *>, <* TRUE *>)) /. 1))) 'or' (( <* TRUE *> /. 1) '&' (( carry ( <* TRUE *>, <* TRUE *>)) /. 1))) by A4, A5, BINARITH:def 6

      .= TRUE by A1;

    end;

    theorem :: BINARI_3:14

    

     Th14: ( 'not' <* FALSE *>) = <* TRUE *>

    proof

      now

        let i be Nat;

        assume

         A1: i in ( Seg 1);

        then

         A2: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

        ( len <* FALSE *>) = 1 by CARD_1:def 7;

        then

         A3: ( <* FALSE *> /. i) = ( <* FALSE *> . 1) by A2, FINSEQ_4: 15;

        ( len ( 'not' <* FALSE *>)) = 1 by CARD_1:def 7;

        

        hence (( 'not' <* FALSE *>) . i) = (( 'not' <* FALSE *>) /. i) by A2, FINSEQ_4: 15

        .= ( 'not' ( <* FALSE *> /. i)) by A1, BINARITH:def 1

        .= ( 'not' FALSE ) by A3, FINSEQ_1: 40

        .= ( <* TRUE *> . i) by A2, FINSEQ_1: 40;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: BINARI_3:15

    ( 'not' <* TRUE *>) = <* FALSE *>

    proof

      now

        let i be Nat;

        assume

         A1: i in ( Seg 1);

        then

         A2: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

        ( len <* TRUE *>) = 1 by CARD_1:def 7;

        then

         A3: ( <* TRUE *> /. i) = ( <* TRUE *> . 1) by A2, FINSEQ_4: 15;

        ( len ( 'not' <* TRUE *>)) = 1 by CARD_1:def 7;

        

        hence (( 'not' <* TRUE *>) . i) = (( 'not' <* TRUE *>) /. i) by A2, FINSEQ_4: 15

        .= ( 'not' ( <* TRUE *> /. i)) by A1, BINARITH:def 1

        .= ( 'not' TRUE ) by A3, FINSEQ_1: 40

        .= ( <* FALSE *> . i) by A2, FINSEQ_1: 40;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: BINARI_3:16

    ( <* FALSE *> + <* FALSE *>) = <* FALSE *>

    proof

      ( add_ovfl ( <* FALSE *>, <* FALSE *>)) <> TRUE by Th13;

      then ( add_ovfl ( <* FALSE *>, <* FALSE *>)) = FALSE by XBOOLEAN:def 3;

      then ( <* FALSE *>, <* FALSE *>) are_summable by BINARITH:def 7;

      

      then ( Absval ( <* FALSE *> + <* FALSE *>)) = (( Absval <* FALSE *>) + ( Absval <* FALSE *>)) by BINARITH: 22

      .= (( Absval <* FALSE *>) + 0 ) by BINARITH: 15

      .= ( Absval <* FALSE *>);

      hence thesis by Th2;

    end;

    theorem :: BINARI_3:17

    

     Th17: ( <* FALSE *> + <* TRUE *>) = <* TRUE *> & ( <* TRUE *> + <* FALSE *>) = <* TRUE *>

    proof

      ( add_ovfl ( <* FALSE *>, <* TRUE *>)) <> TRUE by Th13;

      then ( add_ovfl ( <* FALSE *>, <* TRUE *>)) = FALSE by XBOOLEAN:def 3;

      then ( <* FALSE *>, <* TRUE *>) are_summable by BINARITH:def 7;

      

      then ( Absval ( <* FALSE *> + <* TRUE *>)) = (( Absval <* FALSE *>) + ( Absval <* TRUE *>)) by BINARITH: 22

      .= (( Absval <* FALSE *>) + 1) by BINARITH: 16

      .= ( 0 + 1) by BINARITH: 15

      .= ( Absval <* TRUE *>) by BINARITH: 16;

      hence ( <* FALSE *> + <* TRUE *>) = <* TRUE *> by Th2;

      ( add_ovfl ( <* TRUE *>, <* FALSE *>)) <> TRUE by Th13;

      then ( add_ovfl ( <* TRUE *>, <* FALSE *>)) = FALSE by XBOOLEAN:def 3;

      then ( <* TRUE *>, <* FALSE *>) are_summable by BINARITH:def 7;

      

      then ( Absval ( <* TRUE *> + <* FALSE *>)) = (( Absval <* TRUE *>) + ( Absval <* FALSE *>)) by BINARITH: 22

      .= (( Absval <* TRUE *>) + 0 ) by BINARITH: 15

      .= ( Absval <* TRUE *>);

      hence thesis by Th2;

    end;

    theorem :: BINARI_3:18

    ( <* TRUE *> + <* TRUE *>) = <* FALSE *>

    proof

      

       A1: ( add_ovfl ( <* TRUE *>, <* TRUE *>)) = TRUE by Th13;

      ( Absval ( <* TRUE *> + <* TRUE *>)) = ((( Absval ( <* TRUE *> + <* TRUE *>)) + 2) - 2)

      .= ((( Absval ( <* TRUE *> + <* TRUE *>)) + (2 to_power 1)) - 2) by POWER: 25

      .= ((( Absval ( <* TRUE *> + <* TRUE *>)) + ( IFEQ (( add_ovfl ( <* TRUE *>, <* TRUE *>)), FALSE , 0 ,(2 to_power 1)))) - 2) by A1, FUNCOP_1:def 8

      .= ((( Absval <* TRUE *>) + ( Absval <* TRUE *>)) - 2) by BINARITH: 21

      .= ((( Absval <* TRUE *>) + 1) - 2) by BINARITH: 16

      .= ((1 + 1) - 2) by BINARITH: 16

      .= ( Absval <* FALSE *>) by BINARITH: 15;

      hence thesis by Th2;

    end;

    theorem :: BINARI_3:19

    

     Th19: for n be non zero Nat holds for x,y be Tuple of n, BOOLEAN st (x /. n) = TRUE & (( carry (x,( Bin1 n))) /. n) = TRUE holds for k be non zero Nat st k <> 1 & k <= n holds (x /. k) = TRUE & (( carry (x,( Bin1 n))) /. k) = TRUE

    proof

      let n be non zero Nat;

      let x,y be Tuple of n, BOOLEAN ;

      assume that

       A1: (x /. n) = TRUE and

       A2: (( carry (x,( Bin1 n))) /. n) = TRUE ;

      defpred P[ Nat] means ($1 in ( Seg (n -' 1)) implies (x /. ((n -' $1) + 1)) = TRUE & (( carry (x,( Bin1 n))) /. ((n -' $1) + 1)) = TRUE );

      let k be non zero Nat;

      assume that

       A3: k <> 1 and

       A4: k <= n;

      set i = ((n -' k) + 1);

      1 < k by A3, NAT_2: 19;

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

      then

       A5: 1 <= (k - 1) by XREAL_1: 19;

      

       A6: for j be non zero Nat st P[j] holds P[(j + 1)]

      proof

        let j be non zero Nat;

        assume that

         A7: P[j] and

         A8: (j + 1) in ( Seg (n -' 1));

        

         A9: (j + 1) <= (n -' 1) by A8, FINSEQ_1: 1;

        then

         A10: j < (n -' 1) by NAT_1: 13;

        then j < (n - 1) by NAT_1: 14, XREAL_1: 233;

        then (j + 1) < n by XREAL_1: 20;

        then

         A11: j < n by NAT_1: 13;

        (j + 1) <= (n - 1) by A9, NAT_1: 14, XREAL_1: 233;

        then 1 <= ((n - 1) - j) by XREAL_1: 19;

        then 1 <= ((n - j) - 1);

        then (1 + 1) <= (n - j) by XREAL_1: 19;

        then (1 + 1) <= (n -' j) by A11, XREAL_1: 233;

        then

         A12: (n -' j) > 1 by NAT_1: 13;

        

         A13: 1 <= j by NAT_1: 14;

        

         A14: (n -' j) < n by NAT_2: 9;

        then (n -' j) in ( Seg n) by A12, FINSEQ_1: 1;

        then

         A15: (( Bin1 n) /. (n -' j)) = FALSE by A12, BINARI_2: 6;

        then ((( Bin1 n) /. (n -' j)) '&' (( carry (x,( Bin1 n))) /. (n -' j))) = FALSE ;

        

        then

         A16: TRUE = (((x /. (n -' j)) '&' (( Bin1 n) /. (n -' j))) 'or' ((x /. (n -' j)) '&' (( carry (x,( Bin1 n))) /. (n -' j)))) by A7, A13, A10, A14, A12, A15, BINARITH:def 2, FINSEQ_1: 1

        .= ((x /. (n -' j)) '&' (( carry (x,( Bin1 n))) /. (n -' j))) by A15;

        then (x /. (n -' j)) = TRUE by MARGREL1: 12;

        hence (x /. ((n -' (j + 1)) + 1)) = TRUE by A11, NAT_2: 7;

        (( carry (x,( Bin1 n))) /. (n -' j)) = TRUE by A16, MARGREL1: 12;

        hence thesis by A11, NAT_2: 7;

      end;

      

       A17: 1 <= i by NAT_1: 11;

      i = ((n - k) + 1) by A4, XREAL_1: 233

      .= (n - (k - 1));

      then

       A18: i <= (n - 1) by A5, XREAL_1: 13;

      then (i + 1) <= n by XREAL_1: 19;

      then i < n by NAT_1: 13;

      then

       A19: k = ((n -' i) + 1) by A4, NAT_2: 5;

      i <= (n -' 1) by A18, NAT_1: 14, XREAL_1: 233;

      then

       A20: i in ( Seg (n -' 1)) by A17, FINSEQ_1: 1;

      

       A21: P[1] by A1, A2, NAT_1: 14, XREAL_1: 235;

      for j be non zero Nat holds P[j] from NAT_1:sch 10( A21, A6);

      hence thesis by A19, A20;

    end;

    registration

      cluster zero -> non positive for Nat;

      coherence ;

    end

    theorem :: BINARI_3:20

    

     Th20: for n be non zero Nat holds for x be Tuple of n, BOOLEAN st (x /. n) = TRUE & (( carry (x,( Bin1 n))) /. n) = TRUE holds ( carry (x,( Bin1 n))) = ( 'not' ( Bin1 n))

    proof

      let n be non zero Nat;

      let x be Tuple of n, BOOLEAN ;

      assume that

       A1: (x /. n) = TRUE and

       A2: (( carry (x,( Bin1 n))) /. n) = TRUE ;

      now

        

         A3: ( len ( 'not' ( Bin1 n))) = n by CARD_1:def 7;

        let i be Nat;

        reconsider z = i as Nat;

        

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

        assume

         A5: i in ( Seg n);

        then

         A6: 1 <= i by FINSEQ_1: 1;

        

         A7: i <= n by A5, FINSEQ_1: 1;

        per cases ;

          suppose

           A8: i = 1;

          

          thus (( carry (x,( Bin1 n))) . i) = (( carry (x,( Bin1 n))) /. z) by A6, A7, A4, FINSEQ_4: 15

          .= ( 'not' TRUE ) by A8, BINARITH:def 2

          .= ( 'not' (( Bin1 n) /. i)) by A5, A8, BINARI_2: 5

          .= (( 'not' ( Bin1 n)) /. z) by A5, BINARITH:def 1

          .= (( 'not' ( Bin1 n)) . i) by A6, A7, A3, FINSEQ_4: 15;

        end;

          suppose

           A9: i <> 1;

          1 <= i by A5, FINSEQ_1: 1;

          then 0 < i;

          then

           A10: i is non zero;

          

          thus (( carry (x,( Bin1 n))) . i) = (( carry (x,( Bin1 n))) /. z) by A6, A7, A4, FINSEQ_4: 15

          .= ( 'not' FALSE ) by A1, A2, A7, A9, A10, Th19

          .= ( 'not' (( Bin1 n) /. i)) by A5, A9, BINARI_2: 6

          .= (( 'not' ( Bin1 n)) /. z) by A5, BINARITH:def 1

          .= (( 'not' ( Bin1 n)) . i) by A6, A7, A3, FINSEQ_4: 15;

        end;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: BINARI_3:21

    

     Th21: for n be non zero Nat holds for x,y be Tuple of n, BOOLEAN st y = ( 0* n) & (x /. n) = TRUE & (( carry (x,( Bin1 n))) /. n) = TRUE holds x = ( 'not' y)

    proof

      let n be non zero Nat;

      let x,y be Tuple of n, BOOLEAN ;

      assume that

       A1: y = ( 0* n) and

       A2: (x /. n) = TRUE and

       A3: (( carry (x,( Bin1 n))) /. n) = TRUE ;

      

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

      

       A5: ( len ( 'not' y)) = n by CARD_1:def 7;

      

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

      

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

      now

        let i be Nat;

        reconsider z = i as Nat;

        assume

         A8: i in ( Seg n);

        then

         A9: 1 <= i by FINSEQ_1: 1;

        

         A10: i <= n by A8, FINSEQ_1: 1;

        

         A11: (y . i) = FALSE by A1, A8, FUNCOP_1: 7;

        now

          per cases ;

            suppose

             A12: i = 1;

            

             A13: n >= 1 by NAT_1: 14;

            now

              per cases by A13, XXREAL_0: 1;

                suppose n = 1;

                hence (x . i) = (( 'not' y) . i) by A3, BINARITH:def 2;

              end;

                suppose

                 A14: n > 1;

                

                 A15: ( len ( 'not' ( Bin1 n))) = n by CARD_1:def 7;

                

                 A16: (( carry (x,( Bin1 n))) /. i) = FALSE by A12, BINARITH:def 2;

                then

                 A17: ((( Bin1 n) /. i) '&' (( carry (x,( Bin1 n))) /. i)) = FALSE ;

                

                 A18: (1 + 1) <= n by A14, NAT_1: 13;

                then

                 A19: 2 in ( Seg n) by FINSEQ_1: 1;

                (( carry (x,( Bin1 n))) . (i + 1)) = (( 'not' ( Bin1 n)) . 2) by A2, A3, A12, Th20

                .= (( 'not' ( Bin1 n)) /. 2) by A18, A15, FINSEQ_4: 15

                .= ( 'not' (( Bin1 n) /. 2)) by A19, BINARITH:def 1

                .= ( 'not' FALSE ) by A19, BINARI_2: 6

                .= TRUE ;

                

                then

                 A20: TRUE = (( carry (x,( Bin1 n))) /. (i + 1)) by A7, A12, A18, FINSEQ_4: 15

                .= (((x /. i) '&' (( Bin1 n) /. i)) 'or' ((x /. i) '&' (( carry (x,( Bin1 n))) /. i))) by A12, A14, A16, A17, BINARITH:def 2

                .= ((x /. i) '&' (( Bin1 n) /. i)) by A16;

                

                thus (x . i) = (x /. z) by A4, A9, A10, FINSEQ_4: 15

                .= ( 'not' FALSE ) by A20, MARGREL1: 12

                .= ( 'not' (y /. z)) by A6, A9, A10, A11, FINSEQ_4: 15

                .= (( 'not' y) /. z) by A8, BINARITH:def 1

                .= (( 'not' y) . i) by A5, A9, A10, FINSEQ_4: 15;

              end;

            end;

            hence (x . i) = (( 'not' y) . i);

          end;

            suppose

             A21: i <> 1;

            1 <= i by A8, FINSEQ_1: 1;

            then 0 < i;

            then

             A22: i is non empty;

            

            thus (x . i) = (x /. z) by A4, A9, A10, FINSEQ_4: 15

            .= ( 'not' FALSE ) by A2, A3, A10, A21, A22, Th19

            .= ( 'not' (y /. z)) by A6, A9, A10, A11, FINSEQ_4: 15

            .= (( 'not' y) /. z) by A8, BINARITH:def 1

            .= (( 'not' y) . i) by A5, A9, A10, FINSEQ_4: 15;

          end;

        end;

        hence (x . i) = (( 'not' y) . i);

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: BINARI_3:22

    

     Th22: for n be non zero Nat holds for y be Tuple of n, BOOLEAN st y = ( 0* n) holds ( carry (( 'not' y),( Bin1 n))) = ( 'not' ( Bin1 n))

    proof

      let n be non zero Nat;

      let y be Tuple of n, BOOLEAN ;

      

       A1: n >= 1 by NAT_1: 14;

      

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

      assume

       A3: y = ( 0* n);

      then

       A4: (y . n) = 0 by FINSEQ_1: 3, FUNCOP_1: 7;

      n in ( Seg n) by FINSEQ_1: 3;

      

      then

       A5: (( 'not' y) /. n) = ( 'not' (y /. n)) by BINARITH:def 1

      .= ( 'not' FALSE ) by A1, A4, A2, FINSEQ_4: 15

      .= TRUE ;

      per cases ;

        suppose

         A6: n = 1;

        now

          let i be Nat;

          

           A7: ( len ( 'not' ( Bin1 n))) = n by CARD_1:def 7;

          assume

           A8: i in ( Seg n);

          then

           A9: i = 1 by A6, FINSEQ_1: 2, TARSKI:def 1;

          ( len ( carry (( 'not' y),( Bin1 n)))) = n by CARD_1:def 7;

          

          hence (( carry (( 'not' y),( Bin1 n))) . i) = (( carry (( 'not' y),( Bin1 n))) /. i) by A6, A9, FINSEQ_4: 15

          .= ( 'not' TRUE ) by A9, BINARITH:def 2

          .= ( 'not' (( Bin1 n) /. i)) by A8, A9, BINARI_2: 5

          .= (( 'not' ( Bin1 n)) /. i) by A8, BINARITH:def 1

          .= (( 'not' ( Bin1 n)) . i) by A6, A9, A7, FINSEQ_4: 15;

        end;

        hence thesis by FINSEQ_2: 119;

      end;

        suppose n <> 1;

        then

         A10: n is non trivial by NAT_2:def 1;

        defpred P[ Nat] means $1 <= n implies (( carry (( 'not' y),( Bin1 n))) /. $1) = TRUE ;

        

         A11: for i be non trivial Nat st P[i] holds P[(i + 1)]

        proof

          let i be non trivial Nat;

          assume that

           A12: i <= n implies (( carry (( 'not' y),( Bin1 n))) /. i) = TRUE and

           A13: (i + 1) <= n;

          

           A14: 1 <= i by NAT_1: 14;

          

           A15: i < n by A13, NAT_1: 13;

          then

           A16: i in ( Seg n) by A14, FINSEQ_1: 1;

          then

           A17: (y . i) = FALSE by A3, FUNCOP_1: 7;

          

           A18: (( 'not' y) /. i) = ( 'not' (y /. i)) by A16, BINARITH:def 1

          .= ( 'not' FALSE ) by A2, A14, A15, A17, FINSEQ_4: 15

          .= TRUE ;

          i <> 1 by NAT_2:def 1;

          then

           A19: (( Bin1 n) /. i) = FALSE by A16, BINARI_2: 6;

          then ((( Bin1 n) /. i) '&' (( carry (( 'not' y),( Bin1 n))) /. i)) = FALSE ;

          

          hence (( carry (( 'not' y),( Bin1 n))) /. (i + 1)) = (((( 'not' y) /. i) '&' (( Bin1 n) /. i)) 'or' ((( 'not' y) /. i) '&' (( carry (( 'not' y),( Bin1 n))) /. i))) by A14, A15, A19, BINARITH:def 2

          .= TRUE by A12, A13, A18, NAT_1: 13;

        end;

        

         A20: P[2]

        proof

          assume 2 <= n;

          then (1 + 1) <= n;

          then

           A21: 1 < n by NAT_1: 13;

          then

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

          then

           A23: (y . 1) = FALSE by A3, FUNCOP_1: 7;

          (( 'not' y) /. 1) = ( 'not' (y /. 1)) by A22, BINARITH:def 1

          .= ( 'not' FALSE ) by A2, A21, A23, FINSEQ_4: 15

          .= TRUE ;

          then

           A24: ((( 'not' y) /. 1) '&' (( Bin1 n) /. 1)) = TRUE by A22, BINARI_2: 5;

          

          thus (( carry (( 'not' y),( Bin1 n))) /. 2) = (( carry (( 'not' y),( Bin1 n))) /. (1 + 1))

          .= ((((( 'not' y) /. 1) '&' (( Bin1 n) /. 1)) 'or' ((( 'not' y) /. 1) '&' (( carry (( 'not' y),( Bin1 n))) /. 1))) 'or' ((( Bin1 n) /. 1) '&' (( carry (( 'not' y),( Bin1 n))) /. 1))) by A21, BINARITH:def 2

          .= TRUE by A24;

        end;

        for i be non trivial Nat holds P[i] from NAT_2:sch 2( A20, A11);

        then (( carry (( 'not' y),( Bin1 n))) /. n) = TRUE by A10;

        hence thesis by A5, Th20;

      end;

    end;

    theorem :: BINARI_3:23

    

     Th23: for n be non zero Nat holds for x,y be Tuple of n, BOOLEAN st y = ( 0* n) holds ( add_ovfl (x,( Bin1 n))) = TRUE iff x = ( 'not' y)

    proof

      let n be non zero Nat;

      let x,y be Tuple of n, BOOLEAN ;

      assume

       A1: y = ( 0* n);

      

       A2: n in ( Seg n) by FINSEQ_1: 3;

      

       A3: 1 in ( Seg 1) by FINSEQ_1: 3;

      thus ( add_ovfl (x,( Bin1 n))) = TRUE implies x = ( 'not' y)

      proof

        assume

         A4: ( add_ovfl (x,( Bin1 n))) = TRUE ;

        then

         A5: ((((x /. n) '&' (( Bin1 n) /. n)) 'or' ((x /. n) '&' (( carry (x,( Bin1 n))) /. n))) 'or' ((( Bin1 n) /. n) '&' (( carry (x,( Bin1 n))) /. n))) = TRUE by BINARITH:def 6;

        per cases ;

          suppose

           A6: n <> 1;

          now

            per cases by A5, Th12;

              suppose

               A7: (((x /. n) '&' (( Bin1 n) /. n)) 'or' ((x /. n) '&' (( carry (x,( Bin1 n))) /. n))) = TRUE ;

              now

                per cases by A7, Th12;

                  suppose

                   A8: ((x /. n) '&' (( Bin1 n) /. n)) = TRUE ;

                  assume x <> ( 'not' y);

                  (( Bin1 n) /. n) = TRUE by A8, MARGREL1: 12;

                  hence contradiction by A2, A6, BINARI_2: 6;

                end;

                  suppose

                   A9: ((x /. n) '&' (( carry (x,( Bin1 n))) /. n)) = TRUE ;

                  then (x /. n) = TRUE by MARGREL1: 12;

                  hence thesis by A1, A9, Th21;

                end;

              end;

              hence thesis;

            end;

              suppose

               A10: ((( Bin1 n) /. n) '&' (( carry (x,( Bin1 n))) /. n)) = TRUE ;

              assume x <> ( 'not' y);

              (( Bin1 n) /. n) = TRUE by A10, MARGREL1: 12;

              hence contradiction by A2, A6, BINARI_2: 6;

            end;

          end;

          hence thesis;

        end;

          suppose

           A11: n = 1;

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

          then 1 in ( dom y) by A3, FINSEQ_1:def 3;

          

          then

           A12: (y /. 1) = (y . 1) by PARTFUN1:def 6

          .= 0 by A1, A11, FINSEQ_1: 3, FUNCOP_1: 7;

          consider d be Element of BOOLEAN such that

           A13: x = <*d*> by A11, FINSEQ_2: 97;

          

           A14: d = TRUE by A4, A11, A13, Th10, Th13;

          now

            let i be Nat;

            assume i in ( Seg n);

            then i = 1 by A11, FINSEQ_1: 2, TARSKI:def 1;

            hence (x /. i) = ( 'not' (y /. i)) by A13, A14, A12, FINSEQ_4: 16;

          end;

          hence thesis by BINARITH:def 1;

        end;

      end;

      assume

       A15: x = ( 'not' y);

      per cases ;

        suppose

         A16: n <> 1;

        

         A17: (( carry (x,( Bin1 n))) /. n) = (( 'not' ( Bin1 n)) /. n) by A1, A15, Th22

        .= ( 'not' (( Bin1 n) /. n)) by A2, BINARITH:def 1

        .= ( 'not' FALSE ) by A2, A16, BINARI_2: 6

        .= TRUE ;

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

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

        

        then

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

        .= 0 by A1, FINSEQ_1: 3, FUNCOP_1: 7;

        

         A19: (x /. n) = ( 'not' (y /. n)) by A2, A15, BINARITH:def 1

        .= TRUE by A18;

        

        thus ( add_ovfl (x,( Bin1 n))) = ((((x /. n) '&' (( Bin1 n) /. n)) 'or' ((x /. n) '&' (( carry (x,( Bin1 n))) /. n))) 'or' ((( Bin1 n) /. n) '&' (( carry (x,( Bin1 n))) /. n))) by BINARITH:def 6

        .= TRUE by A19, A17;

      end;

        suppose

         A20: n = 1;

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

        then 1 in ( dom y) by A3, FINSEQ_1:def 3;

        

        then

         A21: (y /. 1) = (y . 1) by PARTFUN1:def 6

        .= 0 by A1, A20, FINSEQ_1: 3, FUNCOP_1: 7;

        consider d be Element of BOOLEAN such that

         A22: x = <*d*> by A20, FINSEQ_2: 97;

        d = (( 'not' y) /. 1) by A15, A22, FINSEQ_4: 16

        .= ( 'not' (y /. 1)) by A3, A20, BINARITH:def 1

        .= TRUE by A21;

        hence thesis by A20, A22, Th10, Th13;

      end;

    end;

    theorem :: BINARI_3:24

    

     Th24: for n be non zero Nat holds for z be Tuple of n, BOOLEAN st z = ( 0* n) holds (( 'not' z) + ( Bin1 n)) = z

    proof

      let n be non zero Nat;

      let z be Tuple of n, BOOLEAN ;

      assume

       A1: z = ( 0* n);

      then

       A2: ( add_ovfl (( 'not' z),( Bin1 n))) = TRUE by Th23;

      ( Absval (( 'not' z) + ( Bin1 n))) = ((( Absval (( 'not' z) + ( Bin1 n))) + (2 to_power n)) - (2 to_power n))

      .= ((( Absval (( 'not' z) + ( Bin1 n))) + ( IFEQ (( add_ovfl (( 'not' z),( Bin1 n))), FALSE , 0 ,(2 to_power n)))) - (2 to_power n)) by A2, FUNCOP_1:def 8

      .= ((( Absval ( 'not' z)) + ( Absval ( Bin1 n))) - (2 to_power n)) by BINARITH: 21

      .= ((((( - ( Absval z)) + (2 to_power n)) - 1) + ( Absval ( Bin1 n))) - (2 to_power n)) by BINARI_2: 13

      .= ((((( - ( Absval z)) + (2 to_power n)) - 1) + 1) - (2 to_power n)) by Th11

      .= ( - 0 ) by A1, Th6

      .= ( Absval z) by A1, Th6;

      hence thesis by Th2;

    end;

    begin

    definition

      let n,k be Nat;

      :: BINARI_3:def1

      func n -BinarySequence k -> Tuple of n, BOOLEAN means

      : Def1: for i be Nat st i in ( Seg n) holds (it /. i) = ( IFEQ (((k div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE ));

      existence

      proof

        reconsider n9 = n as Nat;

        deffunc F( Nat) = ( IFEQ (((k div (2 to_power ($1 -' 1))) mod 2), 0 , FALSE , TRUE ));

        consider p be FinSequence of BOOLEAN such that

         A1: ( len p) = n9 and

         A2: for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_2:sch 1;

        

         A3: ( dom p) = ( Seg n9) by A1, FINSEQ_1:def 3;

        reconsider p as Element of (n -tuples_on BOOLEAN ) by A1, FINSEQ_2: 92;

        take p;

        let i be Nat;

        assume

         A4: i in ( Seg n);

        then i in ( dom p) by A1, FINSEQ_1:def 3;

        

        hence (p /. i) = (p . i) by PARTFUN1:def 6

        .= ( IFEQ (((k div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE )) by A2, A3, A4;

      end;

      uniqueness

      proof

        let p1,p2 be Tuple of n, BOOLEAN such that

         A5: for i be Nat st i in ( Seg n) holds (p1 /. i) = ( IFEQ (((k div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE )) and

         A6: for i be Nat st i in ( Seg n) holds (p2 /. i) = ( IFEQ (((k div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE ));

        

         A7: ( len p1) = n by CARD_1:def 7;

        then

         A8: ( dom p1) = ( Seg n) by FINSEQ_1:def 3;

        

         A9: ( len p2) = n by CARD_1:def 7;

        now

          let i be Nat;

          assume

           A10: i in ( dom p1);

          then

           A11: i in ( dom p2) by A9, A8, FINSEQ_1:def 3;

          

          thus (p1 . i) = (p1 /. i) by A10, PARTFUN1:def 6

          .= ( IFEQ (((k div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE )) by A5, A8, A10

          .= (p2 /. i) by A6, A8, A10

          .= (p2 . i) by A11, PARTFUN1:def 6;

        end;

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    theorem :: BINARI_3:25

    

     Th25: for n be Nat holds (n -BinarySequence 0 ) = ( 0* n)

    proof

      let n be Nat;

      ( 0* n) in ( BOOLEAN * ) by Th4;

      then ( 0* n) is FinSequence of BOOLEAN by FINSEQ_1:def 11;

      then

      reconsider F = ( 0* n) as Tuple of n, BOOLEAN ;

      now

        let i be Nat;

        assume

         A1: i in ( Seg n);

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

        then i in ( dom (n -BinarySequence 0 )) by A1, FINSEQ_1:def 3;

        

        hence ((n -BinarySequence 0 ) . i) = ((n -BinarySequence 0 ) /. i) by PARTFUN1:def 6

        .= ( IFEQ ((( 0 div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE )) by A1, Def1

        .= ( IFEQ (( 0 mod 2), 0 , FALSE , TRUE )) by NAT_2: 2

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

        .= 0 by FUNCOP_1:def 8

        .= (F . i) by A1, FUNCOP_1: 7;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: BINARI_3:26

    

     Th26: for n,k be Nat st k < (2 to_power n) holds (((n + 1) -BinarySequence k) . (n + 1)) = FALSE

    proof

      let n,k be Nat;

      

       A1: ((n + 1) -' 1) = ((n + 1) - 1) by NAT_D: 37

      .= n;

      assume k < (2 to_power n);

      

      then

       A2: ((k div (2 to_power ((n + 1) -' 1))) mod 2) = ( 0 mod 2) by A1, NAT_D: 27

      .= 0 by NAT_D: 26;

      

       A3: (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

      then (n + 1) in ( Seg ( len ((n + 1) -BinarySequence k))) by CARD_1:def 7;

      then (n + 1) in ( dom ((n + 1) -BinarySequence k)) by FINSEQ_1:def 3;

      

      hence (((n + 1) -BinarySequence k) . (n + 1)) = (((n + 1) -BinarySequence k) /. (n + 1)) by PARTFUN1:def 6

      .= ( IFEQ (((k div (2 to_power ((n + 1) -' 1))) mod 2), 0 , FALSE , TRUE )) by A3, Def1

      .= FALSE by A2, FUNCOP_1:def 8;

    end;

    theorem :: BINARI_3:27

    

     Th27: for n be non zero Nat holds for k be Nat st k < (2 to_power n) holds ((n + 1) -BinarySequence k) = ((n -BinarySequence k) ^ <* FALSE *>)

    proof

      let n be non zero Nat;

      let k be Nat;

      assume

       A1: k < (2 to_power n);

      now

        let i be Nat;

        assume

         A2: i in ( Seg (n + 1));

        then i in ( Seg ( len ((n + 1) -BinarySequence k))) by CARD_1:def 7;

        then

         A3: i in ( dom ((n + 1) -BinarySequence k)) by FINSEQ_1:def 3;

        now

          per cases by A2, FINSEQ_2: 7;

            suppose

             A4: i in ( Seg n);

            then i in ( Seg ( len (n -BinarySequence k))) by CARD_1:def 7;

            then

             A5: i in ( dom (n -BinarySequence k)) by FINSEQ_1:def 3;

            

            thus (((n + 1) -BinarySequence k) . i) = (((n + 1) -BinarySequence k) /. i) by A3, PARTFUN1:def 6

            .= ( IFEQ (((k div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE )) by A2, Def1

            .= ((n -BinarySequence k) /. i) by A4, Def1

            .= ((n -BinarySequence k) . i) by A5, PARTFUN1:def 6

            .= (((n -BinarySequence k) ^ <* FALSE *>) . i) by A5, FINSEQ_1:def 7;

          end;

            suppose

             A6: i = (n + 1);

            

            hence (((n + 1) -BinarySequence k) . i) = FALSE by A1, Th26

            .= (((n -BinarySequence k) ^ <* FALSE *>) . i) by A6, FINSEQ_2: 116;

          end;

        end;

        hence (((n + 1) -BinarySequence k) . i) = (((n -BinarySequence k) ^ <* FALSE *>) . i);

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    

     Lm1: for n be non zero Nat holds ((n + 1) -BinarySequence (2 to_power n)) = (( 0* n) ^ <* TRUE *>)

    proof

      let n be non zero Nat;

      ( 0* n) in ( BOOLEAN * ) by Th4;

      then ( 0* n) is FinSequence of BOOLEAN by FINSEQ_1:def 11;

      then

      reconsider 0n = ( 0* n) as Tuple of n, BOOLEAN ;

      now

        let i be Nat;

        assume

         A1: i in ( Seg (n + 1));

        now

          per cases by A1, FINSEQ_2: 7;

            suppose

             A2: i in ( Seg n);

            then

             A3: i >= 1 by FINSEQ_1: 1;

            i <= (n + 1) by A1, FINSEQ_1: 1;

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

            then

             A4: (i -' 1) <= ((n + 1) - 1) by A3, XREAL_1: 233;

            n = ((n - (i -' 1)) + (i -' 1))

            .= ((n -' (i -' 1)) + (i -' 1)) by A4, XREAL_1: 233;

            then

             A5: (2 to_power n) = ((2 to_power (n -' (i -' 1))) * (2 to_power (i -' 1))) by POWER: 27;

            i in ( Seg ( len 0n)) by A2, CARD_1:def 7;

            then

             A6: i in ( dom 0n) by FINSEQ_1:def 3;

            n >= i by A2, FINSEQ_1: 1;

            then (n + 1) > i by NAT_1: 13;

            then n > (i - 1) by XREAL_1: 19;

            then (n - (i - 1)) > 0 by XREAL_1: 50;

            then (n - (i -' 1)) > 0 by A3, XREAL_1: 233;

            then (n -' (i -' 1)) > 0 by A4, XREAL_1: 233;

            then

            consider n1 be Nat such that

             A7: (n -' (i -' 1)) = (n1 + 1) by NAT_1: 6;

            reconsider n1 as Nat;

            

             A8: (2 to_power (n -' (i -' 1))) = ((2 to_power n1) * (2 to_power 1)) by A7, POWER: 27

            .= ((2 to_power n1) * 2) by POWER: 25;

            (2 to_power (i -' 1)) > 0 by POWER: 34;

            

            then

             A9: (((2 to_power n) div (2 to_power (i -' 1))) mod 2) = ((2 to_power (n -' (i -' 1))) mod 2) by A5, NAT_D: 18

            .= 0 by A8, NAT_D: 13;

            i in ( Seg ( len ((n + 1) -BinarySequence (2 to_power n)))) by A1, CARD_1:def 7;

            then i in ( dom ((n + 1) -BinarySequence (2 to_power n))) by FINSEQ_1:def 3;

            

            hence (((n + 1) -BinarySequence (2 to_power n)) . i) = (((n + 1) -BinarySequence (2 to_power n)) /. i) by PARTFUN1:def 6

            .= ( IFEQ ((((2 to_power n) div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE )) by A1, Def1

            .= 0 by A9, FUNCOP_1:def 8

            .= (0n . i) by A2, FUNCOP_1: 7

            .= ((0n ^ <* TRUE *>) . i) by A6, FINSEQ_1:def 7;

          end;

            suppose

             A10: i = (n + 1);

            

             A11: (2 to_power n) > 0 by POWER: 34;

            (i -' 1) = ((n + 1) - 1) by A10, NAT_D: 37

            .= n;

            

            then

             A12: (((2 to_power n) div (2 to_power (i -' 1))) mod 2) = (1 mod 2) by A11, NAT_2: 3

            .= 1 by NAT_D: 14;

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

            then (n + 1) in ( Seg ( len ((n + 1) -BinarySequence (2 to_power n)))) by CARD_1:def 7;

            then (n + 1) in ( dom ((n + 1) -BinarySequence (2 to_power n))) by FINSEQ_1:def 3;

            

            hence (((n + 1) -BinarySequence (2 to_power n)) . i) = (((n + 1) -BinarySequence (2 to_power n)) /. i) by A10, PARTFUN1:def 6

            .= ( IFEQ ((((2 to_power n) div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE )) by A1, Def1

            .= TRUE by A12, FUNCOP_1:def 8

            .= ((0n ^ <* TRUE *>) . i) by A10, FINSEQ_2: 116;

          end;

        end;

        hence (((n + 1) -BinarySequence (2 to_power n)) . i) = ((0n ^ <* TRUE *>) . i);

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    

     Lm2: for n be non zero Nat holds for k be Nat st (2 to_power n) <= k & k < (2 to_power (n + 1)) holds (((n + 1) -BinarySequence k) . (n + 1)) = TRUE

    proof

      let n be non zero Nat;

      let k be Nat;

      assume that

       A1: (2 to_power n) <= k and

       A2: k < (2 to_power (n + 1));

      k < ((2 to_power n) * (2 to_power 1)) by A2, POWER: 27;

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

      then

       A3: k < ((2 to_power n) + (2 to_power n));

      ((n + 1) -' 1) = ((n + 1) - 1) by NAT_D: 37

      .= n;

      

      then

       A4: ((k div (2 to_power ((n + 1) -' 1))) mod 2) = (1 mod 2) by A1, A3, NAT_2: 20

      .= 1 by NAT_D: 24;

      

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

      then (n + 1) in ( Seg ( len ((n + 1) -BinarySequence k))) by CARD_1:def 7;

      then (n + 1) in ( dom ((n + 1) -BinarySequence k)) by FINSEQ_1:def 3;

      

      hence (((n + 1) -BinarySequence k) . (n + 1)) = (((n + 1) -BinarySequence k) /. (n + 1)) by PARTFUN1:def 6

      .= ( IFEQ (((k div (2 to_power ((n + 1) -' 1))) mod 2), 0 , FALSE , TRUE )) by A5, Def1

      .= TRUE by A4, FUNCOP_1:def 8;

    end;

    

     Lm3: for n be non zero Nat holds for k be Nat st (2 to_power n) <= k & k < (2 to_power (n + 1)) holds ((n + 1) -BinarySequence k) = ((n -BinarySequence (k -' (2 to_power n))) ^ <* TRUE *>)

    proof

      let n be non zero Nat;

      let k be Nat;

      assume that

       A1: (2 to_power n) <= k and

       A2: k < (2 to_power (n + 1));

      now

        let i be Nat;

        reconsider z = i as Nat;

        assume

         A3: i in ( Seg (n + 1));

        then i in ( Seg ( len ((n + 1) -BinarySequence k))) by CARD_1:def 7;

        then

         A4: i in ( dom ((n + 1) -BinarySequence k)) by FINSEQ_1:def 3;

        now

          per cases by A3, FINSEQ_2: 7;

            suppose

             A5: i in ( Seg n);

            then

             A6: 1 <= i by FINSEQ_1: 1;

            

             A7: (2 * (2 to_power (i -' 1))) = ((2 to_power (i -' 1)) * (2 to_power 1)) by POWER: 25

            .= (2 to_power ((i -' 1) + 1)) by POWER: 27

            .= (2 to_power ((i - 1) + 1)) by A6, XREAL_1: 233

            .= (2 to_power i);

            (2 to_power (i -' 1)) > 0 by POWER: 34;

            then

             A8: ( 0 + 1) <= (2 to_power (i -' 1)) by NAT_1: 13;

            i <= n by A5, FINSEQ_1: 1;

            then

             A9: (2 * (2 to_power (z -' 1))) divides (2 to_power n) by A7, NAT_2: 11;

             A10:

            now

              per cases ;

                suppose

                 A11: (k div (2 to_power (i -' 1))) is even;

                then

                 A12: ((k div (2 to_power (i -' 1))) mod 2) = 0 by NAT_2: 21;

                ((k -' (2 to_power n)) div (2 to_power (i -' 1))) is even by A1, A8, A9, A11, NAT_2: 23;

                hence ((k div (2 to_power (i -' 1))) mod 2) = (((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2) by A12, NAT_2: 21;

              end;

                suppose

                 A13: (k div (2 to_power (i -' 1))) is odd;

                then

                 A14: ((k div (2 to_power (i -' 1))) mod 2) = 1 by NAT_2: 22;

                ((k -' (2 to_power n)) div (2 to_power (i -' 1))) is odd by A1, A8, A9, A13, NAT_2: 23;

                hence ((k div (2 to_power (i -' 1))) mod 2) = (((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2) by A14, NAT_2: 22;

              end;

            end;

            i in ( Seg ( len (n -BinarySequence (k -' (2 to_power n))))) by A5, CARD_1:def 7;

            then

             A15: i in ( dom (n -BinarySequence (k -' (2 to_power n)))) by FINSEQ_1:def 3;

            

            thus (((n + 1) -BinarySequence k) . i) = (((n + 1) -BinarySequence k) /. i) by A4, PARTFUN1:def 6

            .= ( IFEQ (((k div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE )) by A3, Def1

            .= ((n -BinarySequence (k -' (2 to_power n))) /. i) by A5, A10, Def1

            .= ((n -BinarySequence (k -' (2 to_power n))) . i) by A15, PARTFUN1:def 6

            .= (((n -BinarySequence (k -' (2 to_power n))) ^ <* TRUE *>) . i) by A15, FINSEQ_1:def 7;

          end;

            suppose

             A16: i = (n + 1);

            

            hence (((n + 1) -BinarySequence k) . i) = TRUE by A1, A2, Lm2

            .= (((n -BinarySequence (k -' (2 to_power n))) ^ <* TRUE *>) . i) by A16, FINSEQ_2: 116;

          end;

        end;

        hence (((n + 1) -BinarySequence k) . i) = (((n -BinarySequence (k -' (2 to_power n))) ^ <* TRUE *>) . i);

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    

     Lm4: for n be non zero Nat holds for k be Nat st k < (2 to_power n) holds for x be Tuple of n, BOOLEAN st x = ( 0* n) holds (n -BinarySequence k) = ( 'not' x) iff k = ((2 to_power n) - 1)

    proof

      let n be non zero Nat;

      let k be Nat;

      assume

       A1: k < (2 to_power n);

      let x be Tuple of n, BOOLEAN ;

      assume

       A2: x = ( 0* n);

      thus (n -BinarySequence k) = ( 'not' x) implies k = ((2 to_power n) - 1)

      proof

        defpred P[ Nat] means for k be Nat holds (k < (2 to_power $1) implies for y be Tuple of $1, BOOLEAN st y = ( 0* $1) holds ($1 -BinarySequence k) = ( 'not' y) implies k = ((2 to_power $1) - 1));

        assume

         A3: (n -BinarySequence k) = ( 'not' x);

        

         A4: for m be non zero Nat st P[m] holds P[(m + 1)]

        proof

          let m be non zero Nat;

          assume

           A5: P[m];

          

           A6: (m + 1) in ( Seg (m + 1)) by FINSEQ_1: 4;

          

           A7: ( 0 + 1) <= (m + 1) by XREAL_1: 6;

          ( 0* m) in ( BOOLEAN * ) by Th4;

          then ( 0* m) is FinSequence of BOOLEAN by FINSEQ_1:def 11;

          then

          reconsider y1 = ( 0* m) as Tuple of m, BOOLEAN ;

          let k be Nat;

          assume

           A8: k < (2 to_power (m + 1));

          let y be Tuple of (m + 1), BOOLEAN ;

          assume that

           A9: y = ( 0* (m + 1)) and

           A10: ((m + 1) -BinarySequence k) = ( 'not' y);

          

           A11: (y . (m + 1)) = FALSE by A9, FINSEQ_1: 4, FUNCOP_1: 7;

          

           A12: y = (y1 ^ <* 0 *>) by A9, FINSEQ_2: 60;

          

           A13: ( len y) = (m + 1) by CARD_1:def 7;

          ( len ( 'not' y)) = (m + 1) by CARD_1:def 7;

          

          then

           A14: (((m + 1) -BinarySequence k) . (m + 1)) = (( 'not' y) /. (m + 1)) by A10, A7, FINSEQ_4: 15

          .= ( 'not' (y /. (m + 1))) by A6, BINARITH:def 1

          .= ( 'not' FALSE ) by A13, A7, A11, FINSEQ_4: 15

          .= TRUE ;

          then ((m + 1) -BinarySequence k) = ((m -BinarySequence (k -' (2 to_power m))) ^ <* TRUE *>) by A8, Lm3, Th26;

          then ((m -BinarySequence (k -' (2 to_power m))) ^ <* TRUE *>) = (( 'not' y1) ^ <*( 'not' FALSE )*>) by A10, A12, BINARI_2: 9;

          then

           A15: (m -BinarySequence (k -' (2 to_power m))) = ( 'not' y1) by FINSEQ_2: 17;

          k < ((2 to_power m) * (2 to_power 1)) by A8, POWER: 27;

          then k < (2 * (2 to_power m)) by POWER: 25;

          then k < ((2 to_power m) + (2 to_power m));

          then (k - (2 to_power m)) < (2 to_power m) by XREAL_1: 19;

          then (k -' (2 to_power m)) < (2 to_power m) by A14, Th26, XREAL_1: 233;

          then (k -' (2 to_power m)) = ((2 to_power m) - 1) by A5, A15;

          then (k - (2 to_power m)) = ((2 to_power m) - 1) by A14, Th26, XREAL_1: 233;

          

          hence k = (((2 to_power m) * 2) - 1)

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

          .= ((2 to_power (m + 1)) - 1) by POWER: 27;

        end;

        

         A16: P[1]

        proof

          let k be Nat;

          

           A17: 1 <= ( len (1 -BinarySequence k)) by CARD_1:def 7;

          assume k < (2 to_power 1);

          then

           A18: k < 2 by POWER: 25;

          let y be Tuple of 1, BOOLEAN ;

          assume y = ( 0* 1);

          then

           A19: y = <* FALSE *> by FINSEQ_2: 59;

          assume

           A20: (1 -BinarySequence k) = ( 'not' y);

          

           A21: 1 in ( Seg 1) by FINSEQ_1: 3;

          

           A22: 1 = ( <*1*> . 1) by FINSEQ_1: 40

          .= ((1 -BinarySequence k) /. 1) by A19, A20, A17, Th14, FINSEQ_4: 15

          .= ( IFEQ (((k div (2 to_power (1 -' 1))) mod 2), 0 , FALSE , TRUE )) by A21, Def1;

          k = 1

          proof

            assume k <> 1;

            then k = 0 by A18, NAT_1: 23;

            then (k div (2 to_power (1 -' 1))) = 0 by NAT_D: 27, POWER: 34;

            then ((k div (2 to_power (1 -' 1))) mod 2) = 0 by NAT_D: 26;

            hence contradiction by A22, FUNCOP_1:def 8;

          end;

          

          hence k = ((1 + 1) - 1)

          .= ((2 to_power 1) - 1) by POWER: 25;

        end;

        for m be non zero Nat holds P[m] from NAT_1:sch 10( A16, A4);

        hence thesis by A1, A2, A3;

      end;

      assume

       A23: k = ((2 to_power n) - 1);

      now

        let i be Nat;

        

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

        (2 to_power (i -' 1)) > 0 by POWER: 34;

        then

         A25: (2 to_power (i -' 1)) >= ( 0 + 1) by NAT_1: 13;

        

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

        

         A27: (2 to_power (n -' (i -' 1))) > 0 by POWER: 34;

        then

         A28: (2 to_power (n -' (i -' 1))) >= ( 0 + 1) by NAT_1: 13;

        reconsider z = i as Nat;

        assume

         A29: i in ( Seg n);

        then

         A30: 1 <= i by FINSEQ_1: 1;

        i <= n by A29, FINSEQ_1: 1;

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

        then

         A31: (i - 1) < ((n + 1) - 1) by XREAL_1: 9;

        1 <= i by A29, FINSEQ_1: 1;

        then

         A32: ( 0 + (i -' 1)) < n by A31, XREAL_1: 233;

        then (n - (i -' 1)) > 0 by XREAL_1: 20;

        then (n -' (i -' 1)) > 0 by A32, XREAL_1: 233;

        then

         A33: ((2 to_power (n -' (i -' 1))) mod 2) = 0 by NAT_2: 17;

        (2 to_power n) > 0 by POWER: 34;

        then

         A34: (2 to_power n) >= ( 0 + 1) by NAT_1: 13;

        

        then (k div (2 to_power (i -' 1))) = (((2 to_power n) -' 1) div (2 to_power (i -' 1))) by A23, XREAL_1: 233

        .= (((2 to_power n) div (2 to_power (i -' 1))) - 1) by A25, A32, A34, NAT_2: 11, NAT_2: 15

        .= ((2 to_power (n -' (i -' 1))) - 1) by A32, NAT_2: 16

        .= ((2 to_power (n -' (i -' 1))) -' 1) by A28, XREAL_1: 233;

        then

         A35: ((k div (2 to_power (i -' 1))) mod 2) = 1 by A33, A27, NAT_2: 18;

        

         A36: (x . i) = FALSE by A2, A29, FUNCOP_1: 7;

        

         A37: i <= n by A29, FINSEQ_1: 1;

        i in ( Seg ( len (n -BinarySequence k))) by A29, CARD_1:def 7;

        then i in ( dom (n -BinarySequence k)) by FINSEQ_1:def 3;

        

        hence ((n -BinarySequence k) . i) = ((n -BinarySequence k) /. i) by PARTFUN1:def 6

        .= ( IFEQ (((k div (2 to_power (i -' 1))) mod 2), 0 , FALSE , TRUE )) by A29, Def1

        .= ( 'not' FALSE ) by A35, FUNCOP_1:def 8

        .= ( 'not' (x /. z)) by A24, A30, A37, A36, FINSEQ_4: 15

        .= (( 'not' x) /. z) by A29, BINARITH:def 1

        .= (( 'not' x) . i) by A26, A30, A37, FINSEQ_4: 15;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: BINARI_3:28

    

     Th28: for i be Nat holds ((i + 1) -BinarySequence (2 to_power i)) = (( 0* i) ^ <*1*>)

    proof

      deffunc Bi( Nat) = (($1 + 1) -BinarySequence (2 to_power $1));

      let i be Nat;

      set Bi = Bi(i);

      per cases ;

        suppose

         A1: i = 0 ;

        then

         A2: ( 0* i) = 0 ;

        reconsider i1 = (i + 1) as non zero Nat;

        

         A3: ( 0* i1) = <* FALSE *> by A1, FINSEQ_2: 59;

        then

        reconsider x = ( 0* i1) as Tuple of i1, BOOLEAN ;

        (2 to_power i1) = 2 by A1, POWER: 25;

        then 1 = ((2 to_power i1) - 1);

        then (i1 -BinarySequence 1) = ( 'not' x) by Lm4;

        

        hence Bi = <* TRUE *> by A1, A3, Th14, POWER: 24

        .= (( 0* i) ^ <*1*>) by A2, FINSEQ_1: 34;

      end;

        suppose i > 0 ;

        then

        reconsider i9 = i as non zero Nat;

        Bi = (( 0* i9) ^ <*1*>) by Lm1;

        hence thesis;

      end;

    end;

    theorem :: BINARI_3:29

    for n be non zero Nat holds for k be Nat st (2 to_power n) <= k & k < (2 to_power (n + 1)) holds (((n + 1) -BinarySequence k) . (n + 1)) = TRUE by Lm2;

    theorem :: BINARI_3:30

    for n be non zero Nat holds for k be Nat st (2 to_power n) <= k & k < (2 to_power (n + 1)) holds ((n + 1) -BinarySequence k) = ((n -BinarySequence (k -' (2 to_power n))) ^ <* TRUE *>) by Lm3;

    theorem :: BINARI_3:31

    for n be non zero Nat holds for k be Nat st k < (2 to_power n) holds for x be Tuple of n, BOOLEAN st x = ( 0* n) holds (n -BinarySequence k) = ( 'not' x) iff k = ((2 to_power n) - 1) by Lm4;

    theorem :: BINARI_3:32

    

     Th32: for n be non zero Nat holds for k be Nat st (k + 1) < (2 to_power n) holds ( add_ovfl ((n -BinarySequence k),( Bin1 n))) = FALSE

    proof

      let n be non zero Nat;

      let k be Nat;

      assume

       A1: (k + 1) < (2 to_power n);

      then

       A2: k < (2 to_power n) by NAT_1: 13;

      ( 0* n) in ( BOOLEAN * ) by Th4;

      then ( 0* n) is FinSequence of BOOLEAN by FINSEQ_1:def 11;

      then

      reconsider y = ( 0* n) as Tuple of n, BOOLEAN ;

      k < ((2 to_power n) - 1) by A1, XREAL_1: 20;

      then (n -BinarySequence k) <> ( 'not' y) by A2, Lm4;

      then ( add_ovfl ((n -BinarySequence k),( Bin1 n))) <> TRUE by Th23;

      hence thesis by XBOOLEAN:def 3;

    end;

    theorem :: BINARI_3:33

    

     Th33: for n be non zero Nat holds for k be Nat st (k + 1) < (2 to_power n) holds (n -BinarySequence (k + 1)) = ((n -BinarySequence k) + ( Bin1 n))

    proof

      defpred P[ non zero Nat] means for k be Nat st (k + 1) < (2 to_power $1) holds ($1 -BinarySequence (k + 1)) = (($1 -BinarySequence k) + ( Bin1 $1));

      

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

      proof

        let n be non zero Nat;

        assume

         A2: P[n];

        let k be Nat;

        assume

         A3: (k + 1) < (2 to_power (n + 1));

        then

         A4: k < (2 to_power (n + 1)) by NAT_1: 13;

        now

          per cases by XXREAL_0: 1;

            suppose

             A5: (k + 1) < (2 to_power n);

            then

             A6: k < (2 to_power n) by NAT_1: 13;

            

             A7: ( add_ovfl ((n -BinarySequence k),( Bin1 n))) = FALSE by A5, Th32;

            

            thus ((n + 1) -BinarySequence (k + 1)) = ((n -BinarySequence (k + 1)) ^ <* FALSE *>) by A5, Th27

            .= (((n -BinarySequence k) + ( Bin1 n)) ^ <*(( FALSE 'xor' FALSE ) 'xor' ( add_ovfl ((n -BinarySequence k),( Bin1 n))))*>) by A2, A5, A7

            .= (((n -BinarySequence k) ^ <* FALSE *>) + (( Bin1 n) ^ <* FALSE *>)) by BINARITH: 19

            .= (((n -BinarySequence k) ^ <* FALSE *>) + ( Bin1 (n + 1))) by BINARI_2: 7

            .= (((n + 1) -BinarySequence k) + ( Bin1 (n + 1))) by A6, Th27;

          end;

            suppose

             A8: (k + 1) > (2 to_power n);

            then

             A9: k >= (2 to_power n) by NAT_1: 13;

            (k + 1) < ((2 to_power n) * (2 to_power 1)) by A3, POWER: 27;

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

            then (k + 1) < ((2 to_power n) + (2 to_power n));

            then ((k + 1) - (2 to_power n)) < (2 to_power n) by XREAL_1: 19;

            then ((k - (2 to_power n)) + 1) < (2 to_power n);

            then

             A10: ((k -' (2 to_power n)) + 1) < (2 to_power n) by A9, XREAL_1: 233;

            then

             A11: ( add_ovfl ((n -BinarySequence (k -' (2 to_power n))),( Bin1 n))) = FALSE by Th32;

            

            thus ((n + 1) -BinarySequence (k + 1)) = ((n -BinarySequence ((k + 1) -' (2 to_power n))) ^ <* TRUE *>) by A3, A8, Lm3

            .= ((n -BinarySequence ((k -' (2 to_power n)) + 1)) ^ <* TRUE *>) by A9, NAT_D: 38

            .= (((n -BinarySequence (k -' (2 to_power n))) + ( Bin1 n)) ^ <*(( TRUE 'xor' FALSE ) 'xor' ( add_ovfl ((n -BinarySequence (k -' (2 to_power n))),( Bin1 n))))*>) by A2, A10, A11

            .= (((n -BinarySequence (k -' (2 to_power n))) ^ <* TRUE *>) + (( Bin1 n) ^ <* FALSE *>)) by BINARITH: 19

            .= (((n -BinarySequence (k -' (2 to_power n))) ^ <* TRUE *>) + ( Bin1 (n + 1))) by BINARI_2: 7

            .= (((n + 1) -BinarySequence k) + ( Bin1 (n + 1))) by A4, A9, Lm3;

          end;

            suppose

             A12: (k + 1) = (2 to_power n);

            ( 0* n) in ( BOOLEAN * ) by Th4;

            then ( 0* n) is FinSequence of BOOLEAN by FINSEQ_1:def 11;

            then

            reconsider z = ( 0* n) as Tuple of n, BOOLEAN ;

            

             A13: k < (2 to_power n) by A12, NAT_1: 13;

            k = ((2 to_power n) - 1) by A12;

            then

             A14: (n -BinarySequence k) = ( 'not' z) by A13, Lm4;

            

            thus ((n + 1) -BinarySequence (k + 1)) = (( 0* n) ^ <*1*>) by A12, Th28

            .= ((( 'not' z) + ( Bin1 n)) ^ <* TRUE *>) by Th24

            .= (((n -BinarySequence k) + ( Bin1 n)) ^ <*(( FALSE 'xor' FALSE ) 'xor' ( add_ovfl ((n -BinarySequence k),( Bin1 n))))*>) by A14, Th23

            .= (((n -BinarySequence k) ^ <* FALSE *>) + (( Bin1 n) ^ <* FALSE *>)) by BINARITH: 19

            .= (((n -BinarySequence k) ^ <* FALSE *>) + ( Bin1 (n + 1))) by BINARI_2: 7

            .= (((n + 1) -BinarySequence k) + ( Bin1 (n + 1))) by A13, Th27;

          end;

        end;

        hence thesis;

      end;

      

       A15: P[1]

      proof

        ( 0* 1) in ( BOOLEAN * ) by Th4;

        then ( 0* 1) is FinSequence of BOOLEAN by FINSEQ_1:def 11;

        then

        reconsider x = ( 0* 1) as Tuple of 1, BOOLEAN ;

        let k be Nat;

        

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

        assume

         A17: (k + 1) < (2 to_power 1);

        then (k + 1) < (1 + 1) by POWER: 25;

        then k < 1 by XREAL_1: 6;

        then

         A18: k = 0 by NAT_1: 14;

        

        then (k + 1) = (2 - 1)

        .= ((2 to_power 1) - 1) by POWER: 25;

        

        hence (1 -BinarySequence (k + 1)) = ( 'not' x) by A17, Lm4

        .= ((1 -BinarySequence k) + ( Bin1 1)) by A18, A16, Th10, Th14, Th17, Th25;

      end;

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

    end;

    theorem :: BINARI_3:34

    for n,i be Nat holds ((n + 1) -BinarySequence i) = ( <*(i mod 2)*> ^ (n -BinarySequence (i div 2)))

    proof

      let n,i be Nat;

      

       A1: ( len ((n + 1) -BinarySequence i)) = (n + 1) by CARD_1:def 7;

      then

       A2: ( dom ((n + 1) -BinarySequence i)) = ( Seg (n + 1)) by FINSEQ_1:def 3;

      

       A3: ( len ( <*(i mod 2)*> ^ (n -BinarySequence (i div 2)))) = (1 + ( len (n -BinarySequence (i div 2)))) by FINSEQ_5: 8

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

      now

        let j be Nat;

        reconsider z = j as Nat;

        assume

         A4: j in ( dom ((n + 1) -BinarySequence i));

        then

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

        

         A6: j <= (n + 1) by A2, A4, FINSEQ_1: 1;

        

         A7: ( len <*(i mod 2)*>) = 1 by FINSEQ_1: 39;

        now

          per cases by A5, XXREAL_0: 1;

            suppose

             A8: j > 1;

            

             A9: (2 to_power (((j -' 1) -' 1) + 1)) = ((2 to_power ((j -' 1) -' 1)) * (2 to_power 1)) by POWER: 27

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

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

            then (j -' 1) > 0 by A5, XREAL_1: 233;

            then

             A10: (j -' 1) >= ( 0 + 1) by NAT_1: 13;

            

            then

             A11: (i div (2 to_power (j -' 1))) = (i div (2 to_power (((j -' 1) -' 1) + 1))) by XREAL_1: 235

            .= ((i div 2) div (2 to_power ((j -' 1) -' 1))) by A9, NAT_2: 27;

            (j - 1) <= n by A6, XREAL_1: 20;

            then

             A12: (j -' 1) <= n by A5, XREAL_1: 233;

            then

             A13: (j -' 1) <= ( len (n -BinarySequence (i div 2))) by CARD_1:def 7;

            

             A14: (j -' 1) in ( Seg n) by A10, A12, FINSEQ_1: 1;

            j <= ( len ((n + 1) -BinarySequence i)) by A6, CARD_1:def 7;

            

            hence (((n + 1) -BinarySequence i) . j) = (((n + 1) -BinarySequence i) /. z) by A5, FINSEQ_4: 15

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

            .= ((n -BinarySequence (i div 2)) /. (j -' 1)) by A14, A11, Def1

            .= ((n -BinarySequence (i div 2)) . (j -' 1)) by A10, A13, FINSEQ_4: 15

            .= ((n -BinarySequence (i div 2)) . (j - 1)) by A5, XREAL_1: 233

            .= (( <*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j) by A3, A6, A7, A8, FINSEQ_1: 24;

          end;

            suppose

             A15: j = 1;

             A16:

            now

              per cases ;

                suppose (i mod 2) = 0 ;

                hence ( IFEQ ((i mod 2), 0 , FALSE , TRUE )) = (i mod 2) by FUNCOP_1:def 8;

              end;

                suppose

                 A17: (i mod 2) <> 0 ;

                

                hence ( IFEQ ((i mod 2), 0 , FALSE , TRUE )) = 1 by FUNCOP_1:def 8

                .= (i mod 2) by A17, NAT_D: 12;

              end;

            end;

            

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

            

            thus (((n + 1) -BinarySequence i) . j) = (((n + 1) -BinarySequence i) /. z) by A1, A5, A6, FINSEQ_4: 15

            .= ( IFEQ (((i div (2 to_power (1 -' 1))) mod 2), 0 , FALSE , TRUE )) by A2, A4, A15, Def1

            .= ( IFEQ (((i div 1) mod 2), 0 , FALSE , TRUE )) by A18, XREAL_1: 232

            .= ( IFEQ ((i mod 2), 0 , FALSE , TRUE )) by NAT_2: 4

            .= (( <*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j) by A15, A16, FINSEQ_1: 41;

          end;

        end;

        hence (((n + 1) -BinarySequence i) . j) = (( <*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j);

      end;

      hence thesis by A1, A3, FINSEQ_2: 9;

    end;

    theorem :: BINARI_3:35

    

     Th35: for n be non zero Nat holds for k be Nat holds k < (2 to_power n) implies ( Absval (n -BinarySequence k)) = k

    proof

      let n be non zero Nat;

      defpred P[ Nat] means $1 < (2 to_power n) implies ( Absval (n -BinarySequence $1)) = $1;

      

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

      proof

        ( 0* n) in ( BOOLEAN * ) by Th4;

        then ( 0* n) is FinSequence of BOOLEAN by FINSEQ_1:def 11;

        then

        reconsider 0n = ( 0* n) as Tuple of n, BOOLEAN ;

        let k be Nat;

        assume

         A2: k < (2 to_power n) implies ( Absval (n -BinarySequence k)) = k;

        assume

         A3: (k + 1) < (2 to_power n);

        then

         A4: ((k + 1) - 1) < ((2 to_power n) - 1) by XREAL_1: 9;

        k < (2 to_power n) by A3, NAT_1: 13;

        then (n -BinarySequence k) <> ( 'not' 0n) by A4, Lm4;

        then ( add_ovfl ((n -BinarySequence k),( Bin1 n))) <> TRUE by Th23;

        then ( add_ovfl ((n -BinarySequence k),( Bin1 n))) = FALSE by XBOOLEAN:def 3;

        then

         A5: ((n -BinarySequence k),( Bin1 n)) are_summable by BINARITH:def 7;

        

        thus ( Absval (n -BinarySequence (k + 1))) = ( Absval ((n -BinarySequence k) + ( Bin1 n))) by A3, Th33

        .= (( Absval (n -BinarySequence k)) + ( Absval ( Bin1 n))) by A5, BINARITH: 22

        .= (k + 1) by A2, A3, Th11, NAT_1: 13;

      end;

      

       A6: P[ 0 ]

      proof

        assume 0 < (2 to_power n);

        (n -BinarySequence 0 ) = ( 0* n) by Th25;

        hence thesis by Th6;

      end;

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

    end;

    theorem :: BINARI_3:36

    for n be non zero Nat holds for x be Tuple of n, BOOLEAN holds (n -BinarySequence ( Absval x)) = x

    proof

      let n be non zero Nat;

      let x be Tuple of n, BOOLEAN ;

      ( Absval x) < (2 to_power n) by Th1;

      then ( Absval (n -BinarySequence ( Absval x))) = ( Absval x) by Th35;

      hence thesis by Th2;

    end;