binari_2.miz



    begin

    reserve i,n for Nat;

    reserve m for non zero Nat;

    reserve p,q for Tuple of n, BOOLEAN ;

    reserve d,d1,d2 for Element of BOOLEAN ;

    

     Lm1: ( len p) = n & ( len q) = n & (for i st i in ( Seg n) holds (p /. i) = (q /. i)) implies p = q

    proof

      assume that

       A1: ( len p) = n and

       A2: ( len q) = n and

       A3: for i st i in ( Seg n) holds (p /. i) = (q /. i);

      

       A4: ( dom p) = ( Seg n) by A1, FINSEQ_1:def 3;

      for i be Nat st i in ( dom p) holds (p . i) = (q . i)

      proof

        let i be Nat;

        assume

         A5: i in ( dom p);

        then

         A6: i in ( dom q) by A2, A4, FINSEQ_1:def 3;

        

         A7: (p /. i) = (p . i) by A5, PARTFUN1:def 6;

        (q /. i) = (q . i) by A6, PARTFUN1:def 6;

        hence thesis by A3, A4, A5, A7;

      end;

      hence thesis by A1, A2, FINSEQ_2: 9;

    end;

    definition

      let n be Nat;

      :: BINARI_2:def1

      func Bin1 (n) -> Tuple of n, BOOLEAN means

      : Def1: for i st i in ( Seg n) holds (it /. i) = ( IFEQ (i,1, TRUE , FALSE ));

      existence

      proof

        deffunc F( set) = ( IFEQ ($1,1, TRUE , FALSE ));

        consider z be FinSequence of BOOLEAN such that

         A1: ( len z) = n and

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

        

         A3: ( dom z) = ( Seg n) by A1, FINSEQ_1:def 3;

        z is Element of (n -tuples_on BOOLEAN ) by A1, FINSEQ_2: 92;

        then

        reconsider z as Tuple of n, BOOLEAN ;

        take z;

        let i;

        assume

         A4: i in ( Seg n);

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

        

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

        .= ( IFEQ (i,1, TRUE , FALSE )) by A2, A3, A4;

      end;

      uniqueness

      proof

        let z1,z2 be Tuple of n, BOOLEAN such that

         A5: for i st i in ( Seg n) holds (z1 /. i) = ( IFEQ (i,1, TRUE , FALSE )) and

         A6: for i st i in ( Seg n) holds (z2 /. i) = ( IFEQ (i,1, TRUE , FALSE ));

        

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

        

         A8: ( len z2) = n by CARD_1:def 7;

        

         A9: ( dom z1) = ( Seg n) by A7, FINSEQ_1:def 3;

        now

          let j be Nat;

          assume

           A10: j in ( dom z1);

          then

           A11: j in ( dom z2) by A8, A9, FINSEQ_1:def 3;

          

          thus (z1 . j) = (z1 /. j) by A10, PARTFUN1:def 6

          .= ( IFEQ (j,1, TRUE , FALSE )) by A5, A9, A10

          .= (z2 /. j) by A6, A9, A10

          .= (z2 . j) by A11, PARTFUN1:def 6;

        end;

        hence thesis by A7, A8, FINSEQ_2: 9;

      end;

    end

    definition

      let n be non zero Nat, x be Tuple of n, BOOLEAN ;

      :: BINARI_2:def2

      func Neg2 (x) -> Tuple of n, BOOLEAN equals (( 'not' x) + ( Bin1 n));

      correctness ;

    end

    definition

      let n be Nat, x be Tuple of n, BOOLEAN ;

      :: BINARI_2:def3

      func Intval (x) -> Integer equals

      : Def3: ( Absval x) if (x /. n) = FALSE

      otherwise (( Absval x) - (2 to_power n));

      correctness ;

    end

    definition

      let n be non zero Nat, z1,z2 be Tuple of n, BOOLEAN ;

      :: BINARI_2:def4

      func Int_add_ovfl (z1,z2) -> Element of BOOLEAN equals ((( 'not' (z1 /. n)) '&' ( 'not' (z2 /. n))) '&' (( carry (z1,z2)) /. n));

      correctness ;

    end

    definition

      let n be non zero Nat, z1,z2 be Tuple of n, BOOLEAN ;

      :: BINARI_2:def5

      func Int_add_udfl (z1,z2) -> Element of BOOLEAN equals (((z1 /. n) '&' (z2 /. n)) '&' ( 'not' (( carry (z1,z2)) /. n)));

      correctness ;

    end

    theorem :: BINARI_2:1

    for z1 be Tuple of 2, BOOLEAN holds z1 = ( <* FALSE *> ^ <* FALSE *>) implies ( Intval z1) = 0

    proof

      let z1 be Tuple of 2, BOOLEAN ;

      assume

       A1: z1 = ( <* FALSE *> ^ <* FALSE *>);

      consider k1,k2 be Element of NAT such that

       A2: ( Binary z1) = <*k1, k2*> by FINSEQ_2: 100;

      

       A3: z1 = <* FALSE , FALSE *> by A1, FINSEQ_1:def 9;

      then

       A4: (z1 /. 1) = FALSE by FINSEQ_4: 17;

      

       A5: (z1 /. 2) = FALSE by A3, FINSEQ_4: 17;

      1 in ( Seg 1) & ( Seg 1) c= ( Seg 2) by FINSEQ_1: 3, FINSEQ_1: 5;

      

      then

       A6: (( Binary z1) /. 1) = ( IFEQ ((z1 /. 1), FALSE , 0 ,(2 to_power (1 -' 1)))) by BINARITH:def 3

      .= 0 by A4, FUNCOP_1:def 8;

      2 in ( Seg 2) by FINSEQ_1: 3;

      

      then

       A7: (( Binary z1) /. 2) = ( IFEQ ((z1 /. 2), FALSE , 0 ,(2 to_power (2 -' 1)))) by BINARITH:def 3

      .= 0 by A5, FUNCOP_1:def 8;

      (( Binary z1) /. 1) = k1 & (( Binary z1) /. 2) = k2 by A2, FINSEQ_4: 17;

      

      then ( Absval z1) = ( addnat $$ <* 0 , 0 *>) by A2, A6, A7, BINARITH:def 4

      .= ( addnat $$ ( <* 0 *> ^ <* 0 *>)) by FINSEQ_1:def 9

      .= ( addnat . (( addnat $$ <* 0 *>),( addnat $$ <* 0 *>))) by FINSOP_1: 5

      .= ( addnat . ( 0 ,( addnat $$ <* 0 *>))) by FINSOP_1: 11

      .= ( addnat . ( 0 , 0 )) by FINSOP_1: 11

      .= ( 0 + 0 ) by BINOP_2:def 23

      .= 0 ;

      hence thesis by A5, Def3;

    end;

    theorem :: BINARI_2:2

    

     Th2: for z1 be Tuple of 2, BOOLEAN holds z1 = ( <* TRUE *> ^ <* FALSE *>) implies ( Intval z1) = 1

    proof

      let z1 be Tuple of 2, BOOLEAN ;

      assume

       A1: z1 = ( <* TRUE *> ^ <* FALSE *>);

      consider k1,k2 be Element of NAT such that

       A2: ( Binary z1) = <*k1, k2*> by FINSEQ_2: 100;

      

       A3: z1 = <* TRUE , FALSE *> by A1, FINSEQ_1:def 9;

      then

       A4: (z1 /. 1) = TRUE by FINSEQ_4: 17;

      

       A5: (z1 /. 2) = FALSE by A3, FINSEQ_4: 17;

      1 in ( Seg 1) & ( Seg 1) c= ( Seg 2) by FINSEQ_1: 3, FINSEQ_1: 5;

      

      then

       A6: (( Binary z1) /. 1) = ( IFEQ ((z1 /. 1), FALSE , 0 ,(2 to_power (1 -' 1)))) by BINARITH:def 3

      .= (2 to_power (1 -' 1)) by A4, FUNCOP_1:def 8;

      (1 - 1) = 0 ;

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

      then

       A7: (( Binary z1) /. 1) = 1 by A6, POWER: 24;

      2 in ( Seg 2) by FINSEQ_1: 3;

      

      then

       A8: (( Binary z1) /. 2) = ( IFEQ ((z1 /. 2), FALSE , 0 ,(2 to_power (2 -' 1)))) by BINARITH:def 3

      .= 0 by A5, FUNCOP_1:def 8;

      (( Binary z1) /. 1) = k1 & (( Binary z1) /. 2) = k2 by A2, FINSEQ_4: 17;

      

      then ( Absval z1) = ( addnat $$ <*1, 0 *>) by A2, A7, A8, BINARITH:def 4

      .= ( addnat $$ ( <*1*> ^ <* 0 *>)) by FINSEQ_1:def 9

      .= ( addnat . (( addnat $$ <*1*>),( addnat $$ <* 0 *>))) by FINSOP_1: 5

      .= ( addnat . (1,( addnat $$ <* 0 *>))) by FINSOP_1: 11

      .= ( addnat . (1, 0 )) by FINSOP_1: 11

      .= (1 + 0 ) by BINOP_2:def 23

      .= 1;

      hence thesis by A5, Def3;

    end;

    theorem :: BINARI_2:3

    for z1 be Tuple of 2, BOOLEAN holds z1 = ( <* FALSE *> ^ <* TRUE *>) implies ( Intval z1) = ( - 2)

    proof

      let z1 be Tuple of 2, BOOLEAN ;

      assume

       A1: z1 = ( <* FALSE *> ^ <* TRUE *>);

      consider k1,k2 be Element of NAT such that

       A2: ( Binary z1) = <*k1, k2*> by FINSEQ_2: 100;

      

       A3: z1 = <* FALSE , TRUE *> by A1, FINSEQ_1:def 9;

      then

       A4: (z1 /. 1) = FALSE by FINSEQ_4: 17;

      

       A5: (z1 /. 2) = TRUE by A3, FINSEQ_4: 17;

      

      then

       A6: ( Intval z1) = (( Absval z1) - (2 to_power (1 + 1))) by Def3

      .= (( Absval z1) - ((2 to_power 1) * (2 to_power 1))) by POWER: 27

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

      .= (( Absval z1) - (2 * 2)) by POWER: 25

      .= (( Absval z1) - 4);

      1 in ( Seg 1) & ( Seg 1) c= ( Seg 2) by FINSEQ_1: 3, FINSEQ_1: 5;

      

      then

       A7: (( Binary z1) /. 1) = ( IFEQ ((z1 /. 1), FALSE , 0 ,(2 to_power (1 -' 1)))) by BINARITH:def 3

      .= 0 by A4, FUNCOP_1:def 8;

      2 in ( Seg 2) by FINSEQ_1: 3;

      

      then

       A8: (( Binary z1) /. 2) = ( IFEQ ((z1 /. 2), FALSE , 0 ,(2 to_power (2 -' 1)))) by BINARITH:def 3

      .= (2 to_power (2 -' 1)) by A5, FUNCOP_1:def 8;

      (2 - 1) = 1;

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

      then

       A9: (( Binary z1) /. 2) = 2 by A8, POWER: 25;

      (( Binary z1) /. 1) = k1 & (( Binary z1) /. 2) = k2 by A2, FINSEQ_4: 17;

      

      then ( Absval z1) = ( addnat $$ <* 0 , 2*>) by A2, A7, A9, BINARITH:def 4

      .= ( addnat $$ ( <* 0 *> ^ <*2*>)) by FINSEQ_1:def 9

      .= ( addnat . (( addnat $$ <* 0 *>),( addnat $$ <*2*>))) by FINSOP_1: 5

      .= ( addnat . ( 0 ,( addnat $$ <*2*>))) by FINSOP_1: 11

      .= ( addnat . ( 0 ,2)) by FINSOP_1: 11

      .= ( 0 + 2) by BINOP_2:def 23

      .= 2;

      hence thesis by A6;

    end;

    theorem :: BINARI_2:4

    for z1 be Tuple of 2, BOOLEAN holds z1 = ( <* TRUE *> ^ <* TRUE *>) implies ( Intval z1) = ( - 1)

    proof

      let z1 be Tuple of 2, BOOLEAN ;

      assume

       A1: z1 = ( <* TRUE *> ^ <* TRUE *>);

      consider k1,k2 be Element of NAT such that

       A2: ( Binary z1) = <*k1, k2*> by FINSEQ_2: 100;

      

       A3: z1 = <* TRUE , TRUE *> by A1, FINSEQ_1:def 9;

      then

       A4: (z1 /. 1) <> FALSE by FINSEQ_4: 17;

      

       A5: (z1 /. 2) <> FALSE by A3, FINSEQ_4: 17;

      

      then

       A6: ( Intval z1) = (( Absval z1) - (2 to_power (1 + 1))) by Def3

      .= (( Absval z1) - ((2 to_power 1) * (2 to_power 1))) by POWER: 27

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

      .= (( Absval z1) - (2 * 2)) by POWER: 25

      .= (( Absval z1) - 4);

      1 in ( Seg 1) & ( Seg 1) c= ( Seg 2) by FINSEQ_1: 3, FINSEQ_1: 5;

      

      then

       A7: (( Binary z1) /. 1) = ( IFEQ ((z1 /. 1), FALSE , 0 ,(2 to_power (1 -' 1)))) by BINARITH:def 3

      .= (2 to_power (1 -' 1)) by A4, FUNCOP_1:def 8;

      (1 - 1) = 0 ;

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

      then

       A8: (( Binary z1) /. 1) = 1 by A7, POWER: 24;

      2 in ( Seg 2) by FINSEQ_1: 3;

      

      then

       A9: (( Binary z1) /. 2) = ( IFEQ ((z1 /. 2), FALSE , 0 ,(2 to_power (2 -' 1)))) by BINARITH:def 3

      .= (2 to_power (2 -' 1)) by A5, FUNCOP_1:def 8;

      (2 - 1) = 1;

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

      then

       A10: (( Binary z1) /. 2) = 2 by A9, POWER: 25;

      (( Binary z1) /. 1) = k1 & (( Binary z1) /. 2) = k2 by A2, FINSEQ_4: 17;

      

      then ( Absval z1) = ( addnat $$ <*1, 2*>) by A2, A8, A10, BINARITH:def 4

      .= ( addnat $$ ( <*1*> ^ <*2*>)) by FINSEQ_1:def 9

      .= ( addnat . (( addnat $$ <*1*>),( addnat $$ <*2*>))) by FINSOP_1: 5

      .= ( addnat . (1,( addnat $$ <*2*>))) by FINSOP_1: 11

      .= ( addnat . (1,2)) by FINSOP_1: 11

      .= (1 + 2) by BINOP_2:def 23

      .= 3;

      hence thesis by A6;

    end;

    theorem :: BINARI_2:5

    

     Th5: for i st i in ( Seg n) & i = 1 holds (( Bin1 n) /. i) = TRUE

    proof

      let i be Nat such that

       A1: i in ( Seg n) and

       A2: i = 1;

      

      thus (( Bin1 n) /. i) = ( IFEQ (i,1, TRUE , FALSE )) by A1, Def1

      .= TRUE by A2, FUNCOP_1:def 8;

    end;

    theorem :: BINARI_2:6

    

     Th6: for i st i in ( Seg n) & i <> 1 holds (( Bin1 n) /. i) = FALSE

    proof

      let i be Nat such that

       A1: i in ( Seg n) and

       A2: i <> 1;

      

      thus (( Bin1 n) /. i) = ( IFEQ (i,1, TRUE , FALSE )) by A1, Def1

      .= FALSE by A2, FUNCOP_1:def 8;

    end;

    theorem :: BINARI_2:7

    

     Th7: ( Bin1 (m + 1)) = (( Bin1 m) ^ <* FALSE *>)

    proof

      

       A1: ( len ( Bin1 (m + 1))) = (m + 1) & ( len (( Bin1 m) ^ <* FALSE *>)) = (m + 1) by CARD_1:def 7;

      for i st i in ( Seg (m + 1)) holds (( Bin1 (m + 1)) /. i) = ((( Bin1 m) ^ <* FALSE *>) /. i)

      proof

        let i such that

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

        per cases by A2, FINSEQ_2: 7;

          suppose

           A3: i in ( Seg m);

          thus (( Bin1 (m + 1)) /. i) = ((( Bin1 m) ^ <* FALSE *>) /. i)

          proof

            per cases ;

              suppose

               A4: i = 1;

              ((( Bin1 m) ^ <* FALSE *>) /. i) = (( Bin1 m) /. i) by A3, BINARITH: 1

              .= TRUE by A3, A4, Th5;

              hence thesis by A2, A4, Th5;

            end;

              suppose

               A5: i <> 1;

              ((( Bin1 m) ^ <* FALSE *>) /. i) = (( Bin1 m) /. i) by A3, BINARITH: 1

              .= FALSE by A3, A5, Th6;

              hence thesis by A2, A5, Th6;

            end;

          end;

        end;

          suppose

           A6: i = (m + 1);

          1 <> (m + 1) by NAT_1: 14;

          then (( Bin1 (m + 1)) /. i) = FALSE by A2, A6, Th6;

          hence thesis by A6, BINARITH: 2;

        end;

      end;

      hence thesis by A1, Lm1;

    end;

    theorem :: BINARI_2:8

    

     Th8: for m holds ( Intval (( Bin1 m) ^ <* FALSE *>)) = 1

    proof

      defpred P[ non zero Nat] means ( Intval (( Bin1 $1) ^ <* FALSE *>)) = 1;

      

       A1: P[1]

      proof

        consider k be Element of BOOLEAN such that

         A2: ( Bin1 1) = <*k*> by FINSEQ_2: 97;

        

         A3: (( Bin1 1) /. 1) = k by A2, FINSEQ_4: 16;

        1 in ( Seg 1) by FINSEQ_1: 3;

        then ( Bin1 1) = <* TRUE *> by A2, A3, Th5;

        hence thesis by Th2;

      end;

       A4:

      now

        let m be non zero Nat such that

         A5: P[m];

        ((( Bin1 m) ^ <* FALSE *>) /. (m + 1)) = FALSE by BINARITH: 2;

        then

         A6: ( Absval (( Bin1 m) ^ <* FALSE *>)) = 1 by A5, Def3;

        ((( Bin1 (m + 1)) ^ <* FALSE *>) /. ((m + 1) + 1)) = FALSE by BINARITH: 2;

        

        then ( Intval (( Bin1 (m + 1)) ^ <* FALSE *>)) = ( Absval (( Bin1 (m + 1)) ^ <* FALSE *>)) by Def3

        .= ( Absval ((( Bin1 m) ^ <* FALSE *>) ^ <* FALSE *>)) by Th7

        .= (( Absval (( Bin1 m) ^ <* FALSE *>)) + ( IFEQ ( FALSE , FALSE , 0 ,(2 to_power (m + 1))))) by BINARITH: 20

        .= (1 + 0 ) by A6, FUNCOP_1:def 8

        .= 1;

        hence P[(m + 1)];

      end;

      thus for m holds P[m] from NAT_1:sch 10( A1, A4);

    end;

    theorem :: BINARI_2:9

    

     Th9: for z be Tuple of m, BOOLEAN holds for d be Element of BOOLEAN holds ( 'not' (z ^ <*d*>)) = (( 'not' z) ^ <*( 'not' d)*>)

    proof

      let z be Tuple of m, BOOLEAN ;

      let d;

      

       A1: ( len ( 'not' (z ^ <*d*>))) = (m + 1) & ( len (( 'not' z) ^ <*( 'not' d)*>)) = (m + 1) by CARD_1:def 7;

      for i st i in ( Seg (m + 1)) holds (( 'not' (z ^ <*d*>)) /. i) = ((( 'not' z) ^ <*( 'not' d)*>) /. i)

      proof

        let i such that

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

        per cases by A2, FINSEQ_2: 7;

          suppose

           A3: i in ( Seg m);

          

           A4: (( 'not' (z ^ <*d*>)) /. i) = ( 'not' ((z ^ <*d*>) /. i)) by A2, BINARITH:def 1

          .= ( 'not' (z /. i)) by A3, BINARITH: 1;

          ((( 'not' z) ^ <*( 'not' d)*>) /. i) = (( 'not' z) /. i) by A3, BINARITH: 1

          .= ( 'not' (z /. i)) by A3, BINARITH:def 1;

          hence thesis by A4;

        end;

          suppose

           A5: i = (m + 1);

          (( 'not' (z ^ <*d*>)) /. i) = ( 'not' ((z ^ <*d*>) /. i)) by A2, BINARITH:def 1

          .= ( 'not' d) by A5, BINARITH: 2;

          hence thesis by A5, BINARITH: 2;

        end;

      end;

      hence thesis by A1, Lm1;

    end;

    theorem :: BINARI_2:10

    

     Th10: for z be Tuple of m, BOOLEAN holds for d be Element of BOOLEAN holds ( Intval (z ^ <*d*>)) = (( Absval z) - ( IFEQ (d, FALSE , 0 ,(2 to_power m))) qua Nat)

    proof

      let z be Tuple of m, BOOLEAN ;

      let d;

      per cases by XBOOLEAN:def 3;

        suppose

         A1: d = FALSE ;

        then ((z ^ <*d*>) /. (m + 1)) = FALSE by BINARITH: 2;

        

        then

         A2: ( Intval (z ^ <*d*>)) = ( Absval (z ^ <*d*>)) by Def3

        .= (( Absval z) + ( IFEQ (d, FALSE , 0 ,(2 to_power m)))) by BINARITH: 20

        .= (( Absval z) + 0 ) by A1, FUNCOP_1:def 8

        .= ( Absval z);

        (( Absval z) - ( IFEQ (d, FALSE , 0 ,(2 to_power m))) qua Nat) = (( Absval z) - 0 ) by A1, FUNCOP_1:def 8

        .= ( Absval z);

        hence thesis by A2;

      end;

        suppose

         A3: d = TRUE ;

        then ((z ^ <*d*>) /. (m + 1)) <> FALSE by BINARITH: 2;

        

        then ( Intval (z ^ <*d*>)) = (( Absval (z ^ <*d*>)) - (2 to_power (m + 1))) by Def3

        .= ((( Absval z) + ( IFEQ (d, FALSE , 0 ,(2 to_power m)))) - (2 to_power (m + 1))) by BINARITH: 20

        .= ((( Absval z) + (2 to_power m)) - (2 to_power (m + 1))) by A3, FUNCOP_1:def 8

        .= ((( Absval z) + (2 to_power m)) - ((2 to_power m) * (2 to_power 1))) by POWER: 27

        .= ((( Absval z) + (2 to_power m)) - (2 * (2 to_power m))) by POWER: 25

        .= (( Absval z) - (2 to_power m));

        hence thesis by A3, FUNCOP_1:def 8;

      end;

    end;

    theorem :: BINARI_2:11

    

     Th11: for z1,z2 be Tuple of m, BOOLEAN holds for d1,d2 be Element of BOOLEAN holds ((( Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + ( IFEQ (( Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))), FALSE , 0 ,(2 to_power (m + 1))))) - ( IFEQ (( Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))), FALSE , 0 ,(2 to_power (m + 1))))) = (( Intval (z1 ^ <*d1*>)) + ( Intval (z2 ^ <*d2*>)))

    proof

      let z1,z2 be Tuple of m, BOOLEAN ;

      let d1,d2 be Element of BOOLEAN ;

      set f = FALSE , t = TRUE ;

      

       A1: ( Absval (z1 + z2)) = ((( Absval z1) + ( Absval z2)) - ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power m))))

      proof

        set siki1 = ( Absval (z1 + z2)), siki2 = ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power m)));

        ((siki1 + siki2) - siki2) = siki1;

        hence thesis by BINARITH: 21;

      end;

      

       A2: ( Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) = ( Intval ((z1 + z2) ^ <*((d1 'xor' d2) 'xor' ( add_ovfl (z1,z2)))*>)) by BINARITH: 19

      .= (((( Absval z1) + ( Absval z2)) - ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power m)))) - ( IFEQ (((d1 'xor' d2) 'xor' ( add_ovfl (z1,z2))), FALSE , 0 ,(2 to_power m)))) by A1, Th10;

      

       A3: ( Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) = ((( 'not' d1) '&' ( 'not' ((z2 ^ <*d2*>) /. (m + 1)))) '&' (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1))) by BINARITH: 2

      .= ((( 'not' d1) '&' ( 'not' d2)) '&' (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1))) by BINARITH: 2

      .= ((( 'not' d1) '&' ( 'not' d2)) '&' ( add_ovfl (z1,z2))) by BINARITH: 18;

      

       A4: ( Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) = ((d1 '&' ((z2 ^ <*d2*>) /. (m + 1))) '&' ( 'not' (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)))) by BINARITH: 2

      .= ((d1 '&' d2) '&' ( 'not' (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)))) by BINARITH: 2

      .= ((d1 '&' d2) '&' ( 'not' ( add_ovfl (z1,z2)))) by BINARITH: 18;

      

       A5: ( Intval (z1 ^ <*d1*>)) = (( Absval z1) - ( IFEQ (d1, FALSE , 0 ,(2 to_power m)))) by Th10;

      

       A6: ( Intval (z2 ^ <*d2*>)) = (( Absval z2) - ( IFEQ (d2, FALSE , 0 ,(2 to_power m)))) by Th10;

      per cases by XBOOLEAN:def 3;

        suppose

         A7: d1 = f & d2 = f;

        

        then

         A8: (( Absval z1) - ( IFEQ (d1, FALSE , 0 ,(2 to_power m)))) = (( Absval z1) - 0 ) by FUNCOP_1:def 8

        .= ( Absval z1);

        

         A9: (( Absval z2) - ( IFEQ (d2, FALSE , 0 ,(2 to_power m)))) = (( Absval z2) - 0 ) by A7, FUNCOP_1:def 8

        .= ( Absval z2);

        

         A10: ( IFEQ (((d1 '&' d2) '&' ( 'not' ( add_ovfl (z1,z2)))),f, 0 ,(2 to_power (m + 1)))) = 0 by A7, FUNCOP_1:def 8;

        thus thesis

        proof

          per cases by XBOOLEAN:def 3;

            suppose ( add_ovfl (z1,z2)) = f;

            hence thesis by A2, A3, A4, A6, A7, A8, Th10;

          end;

            suppose

             A11: ( add_ovfl (z1,z2)) = t;

            then ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power m))) = (2 to_power m) by FUNCOP_1:def 8;

            

            then ((( Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + ( IFEQ (( Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))), FALSE , 0 ,(2 to_power (m + 1))))) - ( IFEQ (( Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))), FALSE , 0 ,(2 to_power (m + 1))))) = (((( Absval z1) + ( Absval z2)) - (2 * (2 to_power m))) + (2 to_power (m + 1))) by A2, A3, A4, A7, A10, A11, FUNCOP_1:def 8

            .= (((( Absval z1) + ( Absval z2)) - ((2 to_power 1) * (2 to_power m))) + (2 to_power (m + 1))) by POWER: 25

            .= (((( Absval z1) + ( Absval z2)) - (2 to_power (m + 1))) + (2 to_power (m + 1))) by POWER: 27

            .= (( Absval z1) + ( Absval z2));

            hence thesis by A6, A8, A9, Th10;

          end;

        end;

      end;

        suppose

         A12: d1 = t & d2 = f;

        

        then

         A13: (( Absval z2) - ( IFEQ (d2, FALSE , 0 ,(2 to_power m)))) = (( Absval z2) - 0 ) by FUNCOP_1:def 8

        .= ( Absval z2);

        thus thesis

        proof

          per cases by XBOOLEAN:def 3;

            suppose

             A14: ( add_ovfl (z1,z2)) = f;

            then ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power m))) = 0 by FUNCOP_1:def 8;

            hence thesis by A2, A3, A4, A5, A6, A12, A13, A14;

          end;

            suppose ( add_ovfl (z1,z2)) = t;

            hence thesis by A2, A3, A4, A5, A6, A12;

          end;

        end;

      end;

        suppose

         A15: d1 = f & d2 = t;

        

        then

         A16: (( Absval z1) - ( IFEQ (d1, FALSE , 0 ,(2 to_power m)))) = (( Absval z1) - 0 ) by FUNCOP_1:def 8

        .= ( Absval z1);

        thus thesis

        proof

          per cases by XBOOLEAN:def 3;

            suppose

             A17: ( add_ovfl (z1,z2)) = f;

            then ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power m))) = 0 by FUNCOP_1:def 8;

            hence thesis by A2, A3, A4, A5, A6, A15, A16, A17;

          end;

            suppose ( add_ovfl (z1,z2)) = t;

            hence thesis by A2, A3, A4, A5, A6, A15;

          end;

        end;

      end;

        suppose

         A18: d1 = t & d2 = t;

        then

         A19: (( Absval z2) - ( IFEQ (d2, FALSE , 0 ,(2 to_power m)))) = (( Absval z2) - (2 to_power m)) by FUNCOP_1:def 8;

        

         A20: (( Intval (z1 ^ <*d1*>)) + ( Intval (z2 ^ <*d2*>))) = ((( Absval z1) - ( IFEQ (d1, FALSE , 0 ,(2 to_power m)))) + ( Intval (z2 ^ <*d2*>))) by A5

        .= ((( Absval z1) + ( Absval z2)) - (2 * (2 to_power m))) by A6, A18, A19

        .= ((( Absval z1) + ( Absval z2)) - ((2 to_power 1) * (2 to_power m))) by POWER: 25

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

        

         A21: ( IFEQ (((( 'not' d1) '&' ( 'not' d2)) '&' ( add_ovfl (z1,z2))),f, 0 ,(2 to_power (m + 1)))) = 0 by A18, FUNCOP_1:def 8;

        thus thesis

        proof

          per cases by XBOOLEAN:def 3;

            suppose

             A22: ( add_ovfl (z1,z2)) = f;

            then ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power m))) = 0 by FUNCOP_1:def 8;

            hence thesis by A2, A3, A4, A18, A20, A21, A22, FUNCOP_1:def 8;

          end;

            suppose

             A23: ( add_ovfl (z1,z2)) = t;

            then ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power m))) = (2 to_power m) by FUNCOP_1:def 8;

            

            then ((( Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) + ( IFEQ (( Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))), FALSE , 0 ,(2 to_power (m + 1))))) - ( IFEQ (( Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))), FALSE , 0 ,(2 to_power (m + 1))))) = ((( Absval z1) + ( Absval z2)) - (2 * (2 to_power m))) by A2, A3, A4, A18, A23

            .= ((( Absval z1) + ( Absval z2)) - ((2 to_power 1) * (2 to_power m))) by POWER: 25

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

            hence thesis by A20;

          end;

        end;

      end;

    end;

    theorem :: BINARI_2:12

    

     Th12: for z1,z2 be Tuple of m, BOOLEAN holds for d1,d2 be Element of BOOLEAN holds ( Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))) = (((( Intval (z1 ^ <*d1*>)) + ( Intval (z2 ^ <*d2*>))) - ( IFEQ (( Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))), FALSE , 0 ,(2 to_power (m + 1))))) + ( IFEQ (( Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))), FALSE , 0 ,(2 to_power (m + 1)))))

    proof

      let z1,z2 be Tuple of m, BOOLEAN ;

      let d1, d2;

      set A = ( Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>))), B = ( IFEQ (( Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))), FALSE , 0 ,(2 to_power (m + 1)))), C = ( IFEQ (( Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>))), FALSE , 0 ,(2 to_power (m + 1)))), D = (( Intval (z1 ^ <*d1*>)) + ( Intval (z2 ^ <*d2*>)));

      ((A + B) - C) = D by Th11;

      hence thesis;

    end;

    theorem :: BINARI_2:13

    

     Th13: for m holds for x be Tuple of m, BOOLEAN holds ( Absval ( 'not' x)) = ((( - ( Absval x)) + (2 to_power m)) - 1)

    proof

      defpred P[ Nat] means for x be Tuple of $1, BOOLEAN holds ( Absval ( 'not' x)) = ((( - ( Absval x)) + (2 to_power $1)) - 1);

      

       A1: P[1]

      proof

        let x be Tuple of 1, BOOLEAN ;

        per cases by BINARITH: 14;

          suppose

           A2: x = <* FALSE *>;

          then

           A3: (x /. 1) = FALSE by FINSEQ_4: 16;

          consider k be Element of BOOLEAN such that

           A4: ( 'not' x) = <*k*> by FINSEQ_2: 97;

          

           A5: (( 'not' x) /. 1) = k by A4, FINSEQ_4: 16;

          1 in ( Seg 1) by FINSEQ_1: 3;

          

          then

           A6: (( 'not' x) /. 1) = ( 'not' FALSE ) by A3, BINARITH:def 1

          .= TRUE ;

          ((( - ( Absval x)) + (2 to_power 1)) - 1) = ((( - 0 ) + (2 to_power 1)) - 1) by A2, BINARITH: 15

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

          .= 1;

          hence thesis by A4, A5, A6, BINARITH: 16;

        end;

          suppose

           A7: x = <* TRUE *>;

          then

           A8: (x /. 1) = TRUE by FINSEQ_4: 16;

          consider k be Element of BOOLEAN such that

           A9: ( 'not' x) = <*k*> by FINSEQ_2: 97;

          

           A10: (( 'not' x) /. 1) = k by A9, FINSEQ_4: 16;

          1 in ( Seg 1) by FINSEQ_1: 3;

          

          then

           A11: (( 'not' x) /. 1) = ( 'not' TRUE ) by A8, BINARITH:def 1

          .= FALSE ;

          ((( - ( Absval x)) + (2 to_power 1)) - 1) = ((( - 1) + (2 to_power 1)) - 1) by A7, BINARITH: 16

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

          .= 0 ;

          hence thesis by A9, A10, A11, BINARITH: 15;

        end;

      end;

       A12:

      now

        let m;

        assume

         A13: P[m];

        now

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

          consider t be Element of (m -tuples_on BOOLEAN ), d be Element of BOOLEAN such that

           A14: x = (t ^ <*d*>) by FINSEQ_2: 117;

          

           A15: ( Absval ( 'not' x)) = ( Absval (( 'not' t) ^ <*( 'not' d)*>)) by A14, Th9

          .= (( Absval ( 'not' t)) + ( IFEQ (( 'not' d), FALSE , 0 ,(2 to_power m)))) by BINARITH: 20

          .= (((( - ( Absval t)) + (2 to_power m)) - 1) + ( IFEQ (( 'not' d), FALSE , 0 ,(2 to_power m)))) by A13;

          

           A16: ((( - ( Absval x)) + (2 to_power (m + 1))) - 1) = ((( - (( Absval t) + ( IFEQ (d, FALSE , 0 ,(2 to_power m))))) + (2 to_power (m + 1))) - 1) by A14, BINARITH: 20;

          thus ( Absval ( 'not' x)) = ((( - ( Absval x)) + (2 to_power (m + 1))) - 1)

          proof

            per cases by XBOOLEAN:def 3;

              suppose

               A17: d = FALSE ;

              

              then

               A18: ( Absval ( 'not' x)) = (((( - ( Absval t)) + (2 to_power m)) - 1) + (2 to_power m)) by A15, FUNCOP_1:def 8

              .= ((( - ( Absval t)) + (2 * (2 to_power m))) - 1)

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

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

              ((( - ( Absval x)) + (2 to_power (m + 1))) - 1) = ((( - (( Absval t) + 0 )) + (2 to_power (m + 1))) - 1) by A16, A17, FUNCOP_1:def 8

              .= ((( - ( Absval t)) + (2 to_power (m + 1))) - 1);

              hence thesis by A18;

            end;

              suppose

               A19: d = TRUE ;

              

              then

               A20: ( Absval ( 'not' x)) = (((( - ( Absval t)) + (2 to_power m)) - 1) + 0 ) by A15, FUNCOP_1:def 8

              .= ((( - ( Absval t)) + (2 to_power m)) - 1);

              ((( - ( Absval x)) + (2 to_power (m + 1))) - 1) = ((( - (( Absval t) + (2 to_power m))) + (2 to_power (m + 1))) - 1) by A16, A19, FUNCOP_1:def 8

              .= (((( - ( Absval t)) - (2 to_power m)) + ((2 to_power 1) * (2 to_power m))) - 1) by POWER: 27

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

              .= ((( - ( Absval t)) + (2 to_power m)) - 1);

              hence thesis by A20;

            end;

          end;

        end;

        hence P[(m + 1)];

      end;

      thus for m holds P[m] from NAT_1:sch 10( A1, A12);

    end;

    theorem :: BINARI_2:14

    

     Th14: for z be Tuple of m, BOOLEAN holds for d be Element of BOOLEAN holds ( Neg2 (z ^ <*d*>)) = (( Neg2 z) ^ <*(( 'not' d) 'xor' ( add_ovfl (( 'not' z),( Bin1 m))))*>)

    proof

      let z be Tuple of m, BOOLEAN ;

      let d;

      

      thus ( Neg2 (z ^ <*d*>)) = ((( 'not' z) ^ <*( 'not' d)*>) + ( Bin1 (m + 1))) by Th9

      .= ((( 'not' z) ^ <*( 'not' d)*>) + (( Bin1 m) ^ <* FALSE *>)) by Th7

      .= ((( 'not' z) + ( Bin1 m)) ^ <*((( 'not' d) 'xor' FALSE ) 'xor' ( add_ovfl (( 'not' z),( Bin1 m))))*>) by BINARITH: 19

      .= (( Neg2 z) ^ <*(( 'not' d) 'xor' ( add_ovfl (( 'not' z),( Bin1 m))))*>);

    end;

    theorem :: BINARI_2:15

    

     Th15: for z be Tuple of m, BOOLEAN holds for d be Element of BOOLEAN holds (( Intval ( Neg2 (z ^ <*d*>))) + ( IFEQ (( Int_add_ovfl (( 'not' (z ^ <*d*>)),( Bin1 (m + 1)))), FALSE , 0 ,(2 to_power (m + 1))))) = ( - ( Intval (z ^ <*d*>)))

    proof

      let z be Tuple of m, BOOLEAN ;

      let d;

      set OV = ( IFEQ (( Int_add_ovfl ((( 'not' z) ^ <*( 'not' d)*>),(( Bin1 m) ^ <* FALSE *>))), FALSE , 0 ,(2 to_power (m + 1)))), UD = ( IFEQ (( Int_add_udfl ((( 'not' z) ^ <*( 'not' d)*>),(( Bin1 m) ^ <* FALSE *>))), FALSE , 0 ,(2 to_power (m + 1))));

      

       A1: ( Int_add_udfl ((( 'not' z) ^ <*( 'not' d)*>),(( Bin1 m) ^ <* FALSE *>))) = ((((( 'not' z) ^ <*( 'not' d)*>) /. (m + 1)) '&' FALSE ) '&' ( 'not' (( carry ((( 'not' z) ^ <*( 'not' d)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) by BINARITH: 2

      .= FALSE ;

      

       A2: (( Intval ( Neg2 (z ^ <*d*>))) + ( IFEQ (( Int_add_ovfl (( 'not' (z ^ <*d*>)),( Bin1 (m + 1)))), FALSE , 0 ,(2 to_power (m + 1))))) = (( Intval ((( 'not' z) ^ <*( 'not' d)*>) + ( Bin1 (m + 1)))) + ( IFEQ (( Int_add_ovfl (( 'not' (z ^ <*d*>)),( Bin1 (m + 1)))), FALSE , 0 ,(2 to_power (m + 1))))) by Th9

      .= (( Intval ((( 'not' z) ^ <*( 'not' d)*>) + ( Bin1 (m + 1)))) + ( IFEQ (( Int_add_ovfl ((( 'not' z) ^ <*( 'not' d)*>),( Bin1 (m + 1)))), FALSE , 0 ,(2 to_power (m + 1))))) by Th9

      .= (( Intval ((( 'not' z) ^ <*( 'not' d)*>) + (( Bin1 m) ^ <* FALSE *>))) + ( IFEQ (( Int_add_ovfl ((( 'not' z) ^ <*( 'not' d)*>),( Bin1 (m + 1)))), FALSE , 0 ,(2 to_power (m + 1))))) by Th7

      .= (( Intval ((( 'not' z) ^ <*( 'not' d)*>) + (( Bin1 m) ^ <* FALSE *>))) + OV) by Th7

      .= ((((( Intval (( 'not' z) ^ <*( 'not' d)*>)) + ( Intval (( Bin1 m) ^ <* FALSE *>))) - OV) + UD) + OV) by Th12

      .= ((((( Intval (( 'not' z) ^ <*( 'not' d)*>)) + 1) - OV) + UD) + OV) by Th8

      .= (((( Intval (( 'not' z) ^ <*( 'not' d)*>)) + 1) + UD) - (OV - OV))

      .= ((( Intval (( 'not' z) ^ <*( 'not' d)*>)) + 1) + 0 ) by A1, FUNCOP_1:def 8

      .= ((( Absval ( 'not' z)) - ( IFEQ (( 'not' d), FALSE , 0 ,(2 to_power m)))) + 1) by Th10

      .= ((((( - ( Absval z)) + (2 to_power m)) - 1) - ( IFEQ (( 'not' d), FALSE , 0 ,(2 to_power m)))) + 1) by Th13

      .= ((( - ( Absval z)) + (2 to_power m)) - ( IFEQ (( 'not' d), FALSE , 0 ,(2 to_power m))));

      

       A3: ( - ( Intval (z ^ <*d*>))) = ( - (( Absval z) - ( IFEQ (d, FALSE , 0 ,(2 to_power m))))) by Th10

      .= (( - ( Absval z)) + ( IFEQ (d, FALSE , 0 ,(2 to_power m))));

      per cases by XBOOLEAN:def 3;

        suppose

         A4: d = FALSE ;

        

        then (( Intval ( Neg2 (z ^ <*d*>))) + ( IFEQ (( Int_add_ovfl (( 'not' (z ^ <*d*>)),( Bin1 (m + 1)))), FALSE , 0 ,(2 to_power (m + 1))))) = ((( - ( Absval z)) + (2 to_power m)) - (2 to_power m)) by A2, FUNCOP_1:def 8

        .= (( - ( Absval z)) + 0 );

        hence thesis by A3, A4, FUNCOP_1:def 8;

      end;

        suppose

         A5: d = TRUE ;

        

        then (( Intval ( Neg2 (z ^ <*d*>))) + ( IFEQ (( Int_add_ovfl (( 'not' (z ^ <*d*>)),( Bin1 (m + 1)))), FALSE , 0 ,(2 to_power (m + 1))))) = ((( - ( Absval z)) + (2 to_power m)) - 0 ) by A2, FUNCOP_1:def 8

        .= (( - ( Absval z)) + (2 to_power m));

        hence thesis by A3, A5, FUNCOP_1:def 8;

      end;

    end;

    theorem :: BINARI_2:16

    for m holds for z be Tuple of m, BOOLEAN holds for d be Element of BOOLEAN holds ( Neg2 ( Neg2 (z ^ <*d*>))) = (z ^ <*d*>)

    proof

      defpred P[ non zero Nat] means for z be Tuple of $1, BOOLEAN holds for d be Element of BOOLEAN holds ( Neg2 ( Neg2 (z ^ <*d*>))) = (z ^ <*d*>);

      

       A1: P[1]

      proof

        let z be Tuple of 1, BOOLEAN ;

        let d be Element of BOOLEAN ;

        set NZD = (( 'not' d) 'xor' ( 'not' (z /. 1)));

        set DPI = (d '&' (z /. 1)), NZ1 = (( 'not' z) /. 1);

        set B1 = (( Bin1 1) /. 1);

        

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

        

         A3: ((( 'not' d) 'xor' FALSE ) 'xor' ( add_ovfl (( 'not' z),( Bin1 1)))) = (( 'not' d) 'xor' (((NZ1 '&' B1) 'or' (NZ1 '&' (( carry (( 'not' z),( Bin1 1))) /. 1))) 'or' (B1 '&' (( carry (( 'not' z),( Bin1 1))) /. 1)))) by BINARITH:def 6

        .= (( 'not' d) 'xor' (((NZ1 '&' B1) 'or' (NZ1 '&' FALSE )) 'or' (B1 '&' (( carry (( 'not' z),( Bin1 1))) /. 1)))) by BINARITH:def 2

        .= (( 'not' d) 'xor' (((NZ1 '&' B1) 'or' FALSE ) 'or' (B1 '&' FALSE ))) by BINARITH:def 2

        .= (( 'not' d) 'xor' ( TRUE '&' NZ1)) by A2, Th5

        .= (( 'not' d) 'xor' ( 'not' (z /. 1))) by A2, BINARITH:def 1;

        

         A4: ((( 'not' NZD) 'xor' FALSE ) 'xor' ( add_ovfl (( 'not' (( 'not' z) + ( Bin1 1))),( Bin1 1)))) = (( 'not' NZD) 'xor' ((((( 'not' (( 'not' z) + ( Bin1 1))) /. 1) '&' B1) 'or' ((( 'not' (( 'not' z) + ( Bin1 1))) /. 1) '&' (( carry (( 'not' (( 'not' z) + ( Bin1 1))),( Bin1 1))) /. 1))) 'or' (B1 '&' (( carry (( 'not' (( 'not' z) + ( Bin1 1))),( Bin1 1))) /. 1)))) by BINARITH:def 6

        .= (( 'not' NZD) 'xor' ((((( 'not' (( 'not' z) + ( Bin1 1))) /. 1) '&' (( Bin1 1) /. 1)) 'or' ((( 'not' (( 'not' z) + ( Bin1 1))) /. 1) '&' FALSE )) 'or' ((( Bin1 1) /. 1) '&' (( carry (( 'not' (( 'not' z) + ( Bin1 1))),( Bin1 1))) /. 1)))) by BINARITH:def 2

        .= (( 'not' NZD) 'xor' ((((( 'not' (( 'not' z) + ( Bin1 1))) /. 1) '&' (( Bin1 1) /. 1)) 'or' FALSE ) 'or' (B1 '&' FALSE ))) by BINARITH:def 2

        .= (( 'not' NZD) 'xor' ( TRUE '&' (( 'not' (( 'not' z) + ( Bin1 1))) /. 1))) by A2, Th5

        .= (( 'not' NZD) 'xor' ( 'not' ((( 'not' z) + ( Bin1 1)) /. 1))) by A2, BINARITH:def 1

        .= (( 'not' NZD) 'xor' ( 'not' (((( 'not' z) /. 1) 'xor' (( Bin1 1) /. 1)) 'xor' (( carry (( 'not' z),( Bin1 1))) /. 1)))) by A2, BINARITH:def 5

        .= (( 'not' NZD) 'xor' ( 'not' (((( 'not' z) /. 1) 'xor' (( Bin1 1) /. 1)) 'xor' FALSE ))) by BINARITH:def 2

        .= (( 'not' NZD) 'xor' ( 'not' (NZ1 'xor' TRUE ))) by A2, Th5

        .= (( 'not' NZD) 'xor' ( 'not' (z /. 1))) by A2, BINARITH:def 1;

        

         A5: ( Neg2 ( Neg2 (z ^ <*d*>))) = (( 'not' ((( 'not' z) ^ <*( 'not' d)*>) + ( Bin1 (1 + 1)))) + ( Bin1 (1 + 1))) by Th9

        .= (( 'not' ((( 'not' z) ^ <*( 'not' d)*>) + (( Bin1 1) ^ <* FALSE *>))) + ( Bin1 (1 + 1))) by Th7

        .= (( 'not' ((( 'not' z) + ( Bin1 1)) ^ <*((( 'not' d) 'xor' FALSE ) 'xor' ( add_ovfl (( 'not' z),( Bin1 1))))*>)) + ( Bin1 (1 + 1))) by BINARITH: 19

        .= ((( 'not' (( 'not' z) + ( Bin1 1))) ^ <*( 'not' NZD)*>) + ( Bin1 (1 + 1))) by A3, Th9

        .= ((( 'not' (( 'not' z) + ( Bin1 1))) ^ <*( 'not' NZD)*>) + (( Bin1 1) ^ <* FALSE *>)) by Th7

        .= ((( 'not' (( 'not' z) + ( Bin1 1))) + ( Bin1 1)) ^ <*(( 'not' NZD) 'xor' ( 'not' (z /. 1)))*>) by A4, BINARITH: 19;

        

        then

         A6: (( Neg2 ( Neg2 (z ^ <*d*>))) /. 1) = ((( 'not' (( 'not' z) + ( Bin1 1))) + ( Bin1 1)) /. 1) by A2, BINARITH: 1

        .= (((( 'not' (( 'not' z) + ( Bin1 1))) /. 1) 'xor' (( Bin1 1) /. 1)) 'xor' (( carry (( 'not' (( 'not' z) + ( Bin1 1))),( Bin1 1))) /. 1)) by A2, BINARITH:def 5

        .= (((( 'not' (( 'not' z) + ( Bin1 1))) /. 1) 'xor' (( Bin1 1) /. 1)) 'xor' FALSE ) by BINARITH:def 2

        .= ((( 'not' (( 'not' z) + ( Bin1 1))) /. 1) 'xor' TRUE ) by A2, Th5

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

        .= (((( 'not' z) /. 1) 'xor' (( Bin1 1) /. 1)) 'xor' (( carry (( 'not' z),( Bin1 1))) /. 1)) by A2, BINARITH:def 5

        .= ((NZ1 'xor' (( Bin1 1) /. 1)) 'xor' FALSE ) by BINARITH:def 2

        .= (NZ1 'xor' TRUE ) by A2, Th5

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

        .= (z /. 1);

        reconsider p = d, q = (z /. 1) as boolean object;

        

         A7: (( Neg2 ( Neg2 (z ^ <*d*>))) /. 2) = (((( 'not' d) 'or' ( 'not' ( 'not' (z /. 1)))) '&' (( 'not' ( 'not' d)) 'or' ( 'not' (z /. 1)))) 'xor' ( 'not' (z /. 1))) by A5, BINARITH: 2

        .= ((((( 'not' p) 'or' q) '&' p) 'or' ((( 'not' p) 'or' q) '&' ( 'not' q))) 'xor' ( 'not' (z /. 1))) by XBOOLEAN: 8

        .= ((((p '&' ( 'not' p)) 'or' (p '&' q)) 'or' (( 'not' q) '&' (( 'not' p) 'or' q))) 'xor' ( 'not' (z /. 1))) by XBOOLEAN: 8

        .= ((((d '&' ( 'not' d)) 'or' (d '&' (z /. 1))) 'or' ((( 'not' (z /. 1)) '&' ( 'not' d)) 'or' (( 'not' (z /. 1)) '&' (z /. 1)))) 'xor' ( 'not' (z /. 1))) by XBOOLEAN: 8

        .= ((( FALSE 'or' (d '&' (z /. 1))) 'or' ((( 'not' (z /. 1)) '&' ( 'not' d)) 'or' (( 'not' (z /. 1)) '&' (z /. 1)))) 'xor' ( 'not' (z /. 1))) by XBOOLEAN: 138

        .= ((DPI 'or' ((( 'not' (z /. 1)) '&' ( 'not' d)) 'or' FALSE )) 'xor' ( 'not' (z /. 1))) by XBOOLEAN: 138

        .= (((( 'not' d) 'or' ( 'not' (z /. 1))) '&' (( 'not' (z /. 1)) '&' ((z /. 1) 'or' d))) 'or' ((DPI 'or' (( 'not' (z /. 1)) '&' ( 'not' d))) '&' ( 'not' ( 'not' (z /. 1)))))

        .= (((( 'not' d) 'or' ( 'not' (z /. 1))) '&' ((( 'not' (z /. 1)) '&' (z /. 1)) 'or' (( 'not' (z /. 1)) '&' d))) 'or' ((DPI 'or' (( 'not' (z /. 1)) '&' ( 'not' d))) '&' ( 'not' ( 'not' (z /. 1))))) by XBOOLEAN: 8

        .= (((( 'not' d) 'or' ( 'not' (z /. 1))) '&' ( FALSE 'or' (( 'not' (z /. 1)) '&' d))) 'or' (((d '&' (z /. 1)) 'or' (( 'not' (z /. 1)) '&' ( 'not' d))) '&' ( 'not' ( 'not' (z /. 1))))) by XBOOLEAN: 138

        .= ((((( 'not' (z /. 1)) '&' d) '&' ( 'not' d)) 'or' ((( 'not' (z /. 1)) '&' d) '&' ( 'not' (z /. 1)))) 'or' ((DPI 'or' (( 'not' (z /. 1)) '&' ( 'not' d))) '&' ( 'not' ( 'not' (z /. 1))))) by XBOOLEAN: 8

        .= (((( 'not' (z /. 1)) '&' (d '&' ( 'not' d))) 'or' ((( 'not' (z /. 1)) '&' d) '&' ( 'not' (z /. 1)))) 'or' ((DPI 'or' (( 'not' (z /. 1)) '&' ( 'not' d))) '&' ( 'not' ( 'not' (z /. 1)))))

        .= (((( 'not' (z /. 1)) '&' FALSE ) 'or' ((( 'not' (z /. 1)) '&' d) '&' ( 'not' (z /. 1)))) 'or' ((DPI 'or' (( 'not' (z /. 1)) '&' ( 'not' d))) '&' ( 'not' ( 'not' (z /. 1))))) by XBOOLEAN: 138

        .= ((d '&' (( 'not' (z /. 1)) '&' ( 'not' (z /. 1)))) 'or' ((DPI 'or' (( 'not' (z /. 1)) '&' ( 'not' d))) '&' ( 'not' ( 'not' (z /. 1)))))

        .= ((d '&' ( 'not' (z /. 1))) 'or' (((z /. 1) '&' ((z /. 1) '&' d)) 'or' ((z /. 1) '&' (( 'not' (z /. 1)) '&' ( 'not' d))))) by XBOOLEAN: 8

        .= ((d '&' ( 'not' (z /. 1))) 'or' ((((z /. 1) '&' (z /. 1)) '&' d) 'or' ((z /. 1) '&' (( 'not' (z /. 1)) '&' ( 'not' d)))))

        .= ((d '&' ( 'not' (z /. 1))) 'or' (((z /. 1) '&' d) 'or' (((z /. 1) '&' ( 'not' (z /. 1))) '&' ( 'not' d))))

        .= ((d '&' ( 'not' (z /. 1))) 'or' (((z /. 1) '&' d) 'or' ( FALSE '&' ( 'not' d)))) by XBOOLEAN: 138

        .= (d '&' (( 'not' (z /. 1)) 'or' (z /. 1))) by XBOOLEAN: 8

        .= ( TRUE '&' d) by XBOOLEAN: 102

        .= d;

        consider k1,k2 be Element of BOOLEAN such that

         A8: ( Neg2 ( Neg2 (z ^ <*d*>))) = <*k1, k2*> by FINSEQ_2: 100;

        

         A9: (( Neg2 ( Neg2 (z ^ <*d*>))) /. 1) = k1 & (( Neg2 ( Neg2 (z ^ <*d*>))) /. 2) = k2 by A8, FINSEQ_4: 17;

        consider k be Element of BOOLEAN such that

         A10: z = <*k*> by FINSEQ_2: 97;

        ( Neg2 ( Neg2 (z ^ <*d*>))) = <*k, d*> by A6, A7, A8, A9, A10, FINSEQ_4: 16;

        hence thesis by A10, FINSEQ_1:def 9;

      end;

       A11:

      now

        let m;

        assume

         A12: P[m];

        now

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

          let d be Element of BOOLEAN ;

          consider t be Element of (m -tuples_on BOOLEAN ), k be Element of BOOLEAN such that

           A13: z = (t ^ <*k*>) by FINSEQ_2: 117;

          set A = ( add_ovfl (( 'not' t),( Bin1 m))), B = ( add_ovfl (( 'not' ( Neg2 t)),( Bin1 m)));

          ( Neg2 ( Neg2 (t ^ <*k*>))) = ( Neg2 (( Neg2 t) ^ <*(( 'not' k) 'xor' ( add_ovfl (( 'not' t),( Bin1 m))))*>)) by Th14

          .= (( Neg2 ( Neg2 t)) ^ <*(( 'not' (( 'not' k) 'xor' ( add_ovfl (( 'not' t),( Bin1 m))))) 'xor' ( add_ovfl (( 'not' ( Neg2 t)),( Bin1 m))))*>) by Th14;

          then

           A14: (( Neg2 ( Neg2 (t ^ <*k*>))) /. (m + 1)) = (( 'not' (( 'not' k) 'xor' ( add_ovfl (( 'not' t),( Bin1 m))))) 'xor' ( add_ovfl (( 'not' ( Neg2 t)),( Bin1 m)))) by BINARITH: 2;

          

           A15: ((t ^ <*k*>) /. (m + 1)) = k by BINARITH: 2;

          reconsider p = k, q = A as boolean object;

          (( 'not' (( 'not' k) 'xor' A)) 'xor' B) = (((p '&' (( 'not' p) 'or' ( 'not' q))) 'or' ((( 'not' p) 'or' ( 'not' q)) '&' q)) 'xor' B) by XBOOLEAN: 8

          .= (((k '&' ( 'not' A)) 'or' (A '&' (( 'not' k) 'or' ( 'not' A)))) 'xor' B) by XBOOLEAN: 11

          .= ((A 'xor' k) 'xor' B) by XBOOLEAN: 11

          .= (k 'xor' (A 'xor' B)) by XBOOLEAN: 73;

          then

           A16: (k 'xor' (A 'xor' B)) = (k 'xor' FALSE ) by A12, A14, A15;

          

           A17: (k 'xor' (k 'xor' (A 'xor' B))) = ((k 'xor' k) 'xor' (A 'xor' B)) by XBOOLEAN: 73

          .= ( FALSE 'xor' (A 'xor' B)) by XBOOLEAN: 138

          .= (A 'xor' B);

          

           A18: (k 'xor' (k 'xor' FALSE )) = FALSE by XBOOLEAN: 138;

          

           A19: (A 'xor' (A 'xor' B)) = ((A 'xor' A) 'xor' B) by XBOOLEAN: 73

          .= ( FALSE 'xor' B) by XBOOLEAN: 138

          .= B;

          

           A20: (m + 1) in ( Seg (m + 1)) by FINSEQ_1: 3;

          

           A21: ( add_ovfl (( 'not' z),( Bin1 (m + 1)))) = ( add_ovfl ((( 'not' t) ^ <*( 'not' k)*>),( Bin1 (m + 1)))) by A13, Th9

          .= ( add_ovfl ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) by Th7

          .= (((((( 'not' t) ^ <*( 'not' k)*>) /. (m + 1)) '&' ((( Bin1 m) ^ <* FALSE *>) /. (m + 1))) 'or' (((( 'not' t) ^ <*( 'not' k)*>) /. (m + 1)) '&' (( carry ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) 'or' (((( Bin1 m) ^ <* FALSE *>) /. (m + 1)) '&' (( carry ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) by BINARITH:def 6

          .= (((((( 'not' t) ^ <*( 'not' k)*>) /. (m + 1)) '&' FALSE ) 'or' (((( 'not' t) ^ <*( 'not' k)*>) /. (m + 1)) '&' (( carry ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) 'or' (((( Bin1 m) ^ <* FALSE *>) /. (m + 1)) '&' (( carry ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) by BINARITH: 2

          .= (( FALSE 'or' (((( 'not' t) ^ <*( 'not' k)*>) /. (m + 1)) '&' (( carry ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) 'or' ( FALSE '&' (( carry ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) by BINARITH: 2

          .= (( 'not' k) '&' (( carry ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by BINARITH: 2

          .= (( 'not' k) '&' A) by BINARITH: 18;

          

           A22: ( add_ovfl (( 'not' ( Neg2 z)),( Bin1 (m + 1)))) = ( add_ovfl (( 'not' ( Neg2 z)),(( Bin1 m) ^ <* FALSE *>))) by Th7

          .= ((((( 'not' ( Neg2 z)) /. (m + 1)) '&' ((( Bin1 m) ^ <* FALSE *>) /. (m + 1))) 'or' ((( 'not' ( Neg2 z)) /. (m + 1)) '&' (( carry (( 'not' ( Neg2 z)),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) 'or' (((( Bin1 m) ^ <* FALSE *>) /. (m + 1)) '&' (( carry (( 'not' ( Neg2 z)),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) by BINARITH:def 6

          .= ((((( 'not' ( Neg2 z)) /. (m + 1)) '&' FALSE ) 'or' ((( 'not' ( Neg2 z)) /. (m + 1)) '&' (( carry (( 'not' ( Neg2 z)),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) 'or' (((( Bin1 m) ^ <* FALSE *>) /. (m + 1)) '&' (( carry (( 'not' ( Neg2 z)),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) by BINARITH: 2

          .= (( FALSE 'or' ((( 'not' ( Neg2 z)) /. (m + 1)) '&' (( carry (( 'not' ( Neg2 z)),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) 'or' ( FALSE '&' (( carry (( 'not' ( Neg2 z)),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) by BINARITH: 2

          .= ((( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + ( Bin1 (m + 1)))) /. (m + 1)) '&' (( carry (( 'not' (( 'not' (t ^ <*k*>)) + ( Bin1 (m + 1)))),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by A13, Th9

          .= ((( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + ( Bin1 (m + 1)))) /. (m + 1)) '&' (( carry (( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + ( Bin1 (m + 1)))),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by Th9

          .= ((( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + (( Bin1 m) ^ <* FALSE *>))) /. (m + 1)) '&' (( carry (( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + ( Bin1 (m + 1)))),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by Th7

          .= ((( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + (( Bin1 m) ^ <* FALSE *>))) /. (m + 1)) '&' (( carry (( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + (( Bin1 m) ^ <* FALSE *>))),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by Th7

          .= (( 'not' (((( 'not' t) ^ <*( 'not' k)*>) + (( Bin1 m) ^ <* FALSE *>)) /. (m + 1))) '&' (( carry (( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + (( Bin1 m) ^ <* FALSE *>))),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by A20, BINARITH:def 1

          .= (( 'not' ((((( 'not' t) ^ <*( 'not' k)*>) /. (m + 1)) 'xor' ((( Bin1 m) ^ <* FALSE *>) /. (m + 1))) 'xor' (( carry ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) '&' (( carry (( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + (( Bin1 m) ^ <* FALSE *>))),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by A20, BINARITH:def 5

          .= (( 'not' ((( 'not' k) 'xor' ((( Bin1 m) ^ <* FALSE *>) /. (m + 1))) 'xor' (( carry ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) '&' (( carry (( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + (( Bin1 m) ^ <* FALSE *>))),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by BINARITH: 2

          .= (( 'not' ((( 'not' k) 'xor' FALSE ) 'xor' (( carry ((( 'not' t) ^ <*( 'not' k)*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1)))) '&' (( carry (( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + (( Bin1 m) ^ <* FALSE *>))),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by BINARITH: 2

          .= (( 'not' ((( 'not' k) 'xor' FALSE ) 'xor' ( add_ovfl (( 'not' t),( Bin1 m))))) '&' (( carry (( 'not' ((( 'not' t) ^ <*( 'not' k)*>) + (( Bin1 m) ^ <* FALSE *>))),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by BINARITH: 18

          .= (( 'not' (( 'not' k) 'xor' ( add_ovfl (( 'not' t),( Bin1 m))))) '&' (( carry (( 'not' ((( 'not' t) + ( Bin1 m)) ^ <*((( 'not' k) 'xor' FALSE ) 'xor' ( add_ovfl (( 'not' t),( Bin1 m))))*>)),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by BINARITH: 19

          .= (( 'not' (( 'not' k) 'xor' ( add_ovfl (( 'not' t),( Bin1 m))))) '&' (( carry ((( 'not' (( 'not' t) + ( Bin1 m))) ^ <*( 'not' ((( 'not' k) 'xor' FALSE ) 'xor' ( add_ovfl (( 'not' t),( Bin1 m)))))*>),(( Bin1 m) ^ <* FALSE *>))) /. (m + 1))) by Th9

          .= (((( 'not' k) 'or' ( 'not' A)) '&' (k 'or' ( 'not' ( 'not' A)))) '&' A) by A16, A17, A18, A19, BINARITH: 18

          .= ((( 'not' k) 'or' ( 'not' A)) '&' (A '&' (k 'or' A)))

          .= (A '&' (( 'not' A) 'or' ( 'not' k))) by XBOOLEAN: 6

          .= (A '&' ( 'not' k)) by XBOOLEAN: 11;

          set C = (( 'not' k) '&' A);

          reconsider p = d, q = C as boolean object;

          

           A23: (( 'not' (( 'not' d) 'xor' C)) 'xor' C) = (((p '&' (( 'not' p) 'or' ( 'not' q))) 'or' ((( 'not' p) 'or' ( 'not' q)) '&' q)) 'xor' C) by XBOOLEAN: 8

          .= (((d '&' ( 'not' C)) 'or' (C '&' (( 'not' d) 'or' ( 'not' C)))) 'xor' C) by XBOOLEAN: 11

          .= ((C 'xor' d) 'xor' C) by XBOOLEAN: 11

          .= (d 'xor' (C 'xor' C)) by XBOOLEAN: 73

          .= (d 'xor' FALSE ) by XBOOLEAN: 138

          .= d;

          

          thus ( Neg2 ( Neg2 (z ^ <*d*>))) = ( Neg2 (( Neg2 z) ^ <*(( 'not' d) 'xor' ( add_ovfl (( 'not' z),( Bin1 (m + 1)))))*>)) by Th14

          .= (( Neg2 ( Neg2 z)) ^ <*(( 'not' (( 'not' d) 'xor' ( add_ovfl (( 'not' z),( Bin1 (m + 1)))))) 'xor' ( add_ovfl (( 'not' ( Neg2 z)),( Bin1 (m + 1)))))*>) by Th14

          .= (z ^ <*d*>) by A12, A13, A21, A22, A23;

        end;

        hence P[(m + 1)];

      end;

      thus for m holds P[m] from NAT_1:sch 10( A1, A11);

    end;

    definition

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

      :: BINARI_2:def6

      func x - y -> Tuple of n, BOOLEAN means

      : Def6: for i st i in ( Seg n) holds (it /. i) = (((x /. i) 'xor' (( Neg2 y) /. i)) 'xor' (( carry (x,( Neg2 y))) /. i));

      existence

      proof

        deffunc F( Nat) = (((x /. $1) 'xor' (( Neg2 y) /. $1)) 'xor' (( carry (x,( Neg2 y))) /. $1));

        consider z be FinSequence of BOOLEAN such that

         A1: ( len z) = n and

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

        

         A3: ( dom z) = ( Seg n) by A1, FINSEQ_1:def 3;

        z is Element of (n -tuples_on BOOLEAN ) by A1, FINSEQ_2: 92;

        then

        reconsider z as Tuple of n, BOOLEAN ;

        take z;

        let i;

        assume

         A4: i in ( Seg n);

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

        

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

        .= (((x /. i) 'xor' (( Neg2 y) /. i)) 'xor' (( carry (x,( Neg2 y))) /. i)) by A2, A3, A4;

      end;

      uniqueness

      proof

        let z1,z2 be Tuple of n, BOOLEAN such that

         A5: for i st i in ( Seg n) holds (z1 /. i) = (((x /. i) 'xor' (( Neg2 y) /. i)) 'xor' (( carry (x,( Neg2 y))) /. i)) and

         A6: for i st i in ( Seg n) holds (z2 /. i) = (((x /. i) 'xor' (( Neg2 y) /. i)) 'xor' (( carry (x,( Neg2 y))) /. i));

        

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

        

         A8: ( len z2) = n by CARD_1:def 7;

        

         A9: ( dom z1) = ( Seg n) by A7, FINSEQ_1:def 3;

        now

          let j be Nat;

          assume

           A10: j in ( dom z1);

          ( Seg n) = ( Seg ( len z2)) by CARD_1:def 7;

          then

           A11: j in ( dom z2) by A9, A10, FINSEQ_1:def 3;

          

          thus (z1 . j) = (z1 /. j) by A10, PARTFUN1:def 6

          .= (((x /. j) 'xor' (( Neg2 y) /. j)) 'xor' (( carry (x,( Neg2 y))) /. j)) by A5, A9, A10

          .= (z2 /. j) by A6, A9, A10

          .= (z2 . j) by A11, PARTFUN1:def 6;

        end;

        hence thesis by A7, A8, FINSEQ_2: 9;

      end;

    end

    theorem :: BINARI_2:17

    

     Th17: for x,y be Tuple of m, BOOLEAN holds (x - y) = (x + ( Neg2 y))

    proof

      let x,y be Tuple of m, BOOLEAN ;

      for i st i in ( Seg m) holds ((x - y) /. i) = (((x /. i) 'xor' (( Neg2 y) /. i)) 'xor' (( carry (x,( Neg2 y))) /. i)) by Def6;

      hence thesis by BINARITH:def 5;

    end;

    theorem :: BINARI_2:18

    for z1,z2 be Tuple of m, BOOLEAN holds for d1,d2 be Element of BOOLEAN holds ((z1 ^ <*d1*>) - (z2 ^ <*d2*>)) = ((z1 + ( Neg2 z2)) ^ <*(((d1 'xor' ( 'not' d2)) 'xor' ( add_ovfl (( 'not' z2),( Bin1 m)))) 'xor' ( add_ovfl (z1,( Neg2 z2))))*>)

    proof

      let z1,z2 be Tuple of m, BOOLEAN ;

      let d1, d2;

      

      thus ((z1 ^ <*d1*>) - (z2 ^ <*d2*>)) = ((z1 ^ <*d1*>) + ( Neg2 (z2 ^ <*d2*>))) by Th17

      .= ((z1 ^ <*d1*>) + (( Neg2 z2) ^ <*(( 'not' d2) 'xor' ( add_ovfl (( 'not' z2),( Bin1 m))))*>)) by Th14

      .= ((z1 + ( Neg2 z2)) ^ <*((d1 'xor' (( 'not' d2) 'xor' ( add_ovfl (( 'not' z2),( Bin1 m))))) 'xor' ( add_ovfl (z1,( Neg2 z2))))*>) by BINARITH: 19

      .= ((z1 + ( Neg2 z2)) ^ <*(((d1 'xor' ( 'not' d2)) 'xor' ( add_ovfl (( 'not' z2),( Bin1 m)))) 'xor' ( add_ovfl (z1,( Neg2 z2))))*>) by XBOOLEAN: 73;

    end;

    theorem :: BINARI_2:19

    for z1,z2 be Tuple of m, BOOLEAN holds for d1,d2 be Element of BOOLEAN holds (((( Intval ((z1 ^ <*d1*>) - (z2 ^ <*d2*>))) + ( IFEQ (( Int_add_ovfl ((z1 ^ <*d1*>),( Neg2 (z2 ^ <*d2*>)))), FALSE , 0 ,(2 to_power (m + 1))))) - ( IFEQ (( Int_add_udfl ((z1 ^ <*d1*>),( Neg2 (z2 ^ <*d2*>)))), FALSE , 0 ,(2 to_power (m + 1))))) + ( IFEQ (( Int_add_ovfl (( 'not' (z2 ^ <*d2*>)),( Bin1 (m + 1)))), FALSE , 0 ,(2 to_power (m + 1))))) = (( Intval (z1 ^ <*d1*>)) - ( Intval (z2 ^ <*d2*>)))

    proof

      let z1,z2 be Tuple of m, BOOLEAN ;

      let d1, d2;

      set OV1 = ( IFEQ (( Int_add_ovfl ((z1 ^ <*d1*>),( Neg2 (z2 ^ <*d2*>)))), FALSE , 0 ,(2 to_power (m + 1)))), UD1 = ( IFEQ (( Int_add_udfl ((z1 ^ <*d1*>),( Neg2 (z2 ^ <*d2*>)))), FALSE , 0 ,(2 to_power (m + 1)))), OV2 = ( IFEQ (( Int_add_ovfl (( 'not' (z2 ^ <*d2*>)),( Bin1 (m + 1)))), FALSE , 0 ,(2 to_power (m + 1)))), NEG = (( Neg2 z2) ^ <*(( 'not' d2) 'xor' ( add_ovfl (( 'not' z2),( Bin1 m))))*>);

      

      thus (((( Intval ((z1 ^ <*d1*>) - (z2 ^ <*d2*>))) + OV1) - UD1) + OV2) = (((( Intval ((z1 ^ <*d1*>) + ( Neg2 (z2 ^ <*d2*>)))) + OV1) - UD1) + OV2) by Th17

      .= (((( Intval ((z1 ^ <*d1*>) + NEG)) + OV1) - UD1) + OV2) by Th14

      .= (((( Intval ((z1 ^ <*d1*>) + NEG)) + ( IFEQ (( Int_add_ovfl ((z1 ^ <*d1*>),NEG)), FALSE , 0 ,(2 to_power (m + 1))))) - UD1) + OV2) by Th14

      .= (((( Intval ((z1 ^ <*d1*>) + NEG)) + ( IFEQ (( Int_add_ovfl ((z1 ^ <*d1*>),NEG)), FALSE , 0 ,(2 to_power (m + 1))))) - ( IFEQ (( Int_add_udfl ((z1 ^ <*d1*>),NEG)), FALSE , 0 ,(2 to_power (m + 1))))) + OV2) by Th14

      .= ((( Intval (z1 ^ <*d1*>)) + ( Intval NEG)) + OV2) by Th11

      .= (( Intval (z1 ^ <*d1*>)) + (( Intval NEG) + OV2))

      .= (( Intval (z1 ^ <*d1*>)) + (( Intval ( Neg2 (z2 ^ <*d2*>))) + OV2)) by Th14

      .= (( Intval (z1 ^ <*d1*>)) + ( - ( Intval (z2 ^ <*d2*>)))) by Th15

      .= (( Intval (z1 ^ <*d1*>)) - ( Intval (z2 ^ <*d2*>)));

    end;