binarith.miz



    begin

    theorem :: BINARITH:1

    

     Th1: for i,n be Nat, D be non empty set, d be Element of D, z be Tuple of n, D st i in ( Seg n) holds ((z ^ <*d*>) /. i) = (z /. i)

    proof

      let i,n be Nat, D be non empty set, d be Element of D, z be Tuple of n, D such that

       A1: i in ( Seg n);

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

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

      hence thesis by FINSEQ_4: 68;

    end;

    theorem :: BINARITH:2

    

     Th2: for n be Nat, D be non empty set, d be Element of D, z be Tuple of n, D holds ((z ^ <*d*>) /. (n + 1)) = d

    proof

      let n be Nat, D be non empty set, d be Element of D, z be Tuple of n, D;

      ( len <*d*>) = 1 by FINSEQ_1: 39;

      then ( 0 + 1) in ( Seg ( len <*d*>));

      then

       A1: ( 0 + 1) in ( dom <*d*>) by FINSEQ_1:def 3;

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

      

      hence ((z ^ <*d*>) /. (n + 1)) = ( <*d*> /. 1) by A1, FINSEQ_4: 69

      .= d by FINSEQ_4: 16;

    end;

    definition

      let x,y be Element of BOOLEAN ;

      :: original: 'or'

      redefine

      func x 'or' y -> Element of BOOLEAN ;

      correctness

      proof

        (x 'or' y) = FALSE or (x 'or' y) = TRUE by XBOOLEAN:def 3;

        hence thesis;

      end;

      :: original: 'xor'

      redefine

      func x 'xor' y -> Element of BOOLEAN ;

      correctness

      proof

        (x 'xor' y) = FALSE or (x 'xor' y) = TRUE by XBOOLEAN:def 3;

        hence thesis;

      end;

    end

    reserve x,y,z for boolean object;

    theorem :: BINARITH:3

    (x 'or' FALSE ) = x;

    theorem :: BINARITH:4

    ( 'not' (x '&' y)) = (( 'not' x) 'or' ( 'not' y));

    theorem :: BINARITH:5

    ( 'not' (x 'or' y)) = (( 'not' x) '&' ( 'not' y));

    theorem :: BINARITH:6

    (x '&' y) = ( 'not' (( 'not' x) 'or' ( 'not' y)));

    theorem :: BINARITH:7

    ( TRUE 'xor' x) = ( 'not' x);

    theorem :: BINARITH:8

    ( FALSE 'xor' x) = x;

    theorem :: BINARITH:9

    (x '&' x) = x;

    theorem :: BINARITH:10

    (x 'or' TRUE ) = TRUE ;

    theorem :: BINARITH:11

    ((x 'or' y) 'or' z) = (x 'or' (y 'or' z));

    theorem :: BINARITH:12

    (x 'or' x) = x;

    theorem :: BINARITH:13

    ( TRUE 'xor' FALSE ) = TRUE ;

    reserve i,j,k for Nat;

    reserve n for non zero Nat;

    reserve x,y,z1,z2 for Tuple of n, BOOLEAN ;

    definition

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

      :: BINARITH:def1

      func 'not' x -> Tuple of n, BOOLEAN means for i st i in ( Seg n) holds (it /. i) = ( 'not' (x /. i));

      existence

      proof

        deffunc F( Nat) = ( 'not' (x /. $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;

        reconsider z as Tuple of n, BOOLEAN by A1, CARD_1:def 7;

        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

        .= ( 'not' (x /. i)) by A2, A3, A4;

      end;

      uniqueness

      proof

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

         A5: for i st i in ( Seg n) holds (y /. i) = ( 'not' (x /. i)) and

         A6: for i st i in ( Seg n) holds (z /. i) = ( 'not' (x /. i));

        

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

        then

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

        

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

        now

          let j be Nat;

          assume

           A10: j in ( dom y);

          then

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

          

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

          .= ( 'not' (x /. j)) by A5, A8, A10

          .= (z /. j) by A6, A8, A10

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

        end;

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    definition

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

      :: BINARITH:def2

      func carry (x,y) -> Tuple of n, BOOLEAN means

      : Def2: (it /. 1) = FALSE & for i be Nat st 1 <= i & i < n holds (it /. (i + 1)) = ((((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (it /. i))) 'or' ((y /. i) '&' (it /. i)));

      existence

      proof

        deffunc G( Nat, Element of BOOLEAN ) = ((((x /. ($1 + 1)) '&' (y /. ($1 + 1))) 'or' ((x /. ($1 + 1)) '&' $2)) 'or' ((y /. ($1 + 1)) '&' $2));

        consider f be sequence of BOOLEAN such that

         A1: (f . 0 ) = FALSE and

         A2: for i be Nat holds (f . (i + 1)) = G(i,.) from NAT_1:sch 12;

        deffunc F( Nat) = (f . ($1 - 1));

        consider z be FinSequence such that

         A3: ( len z) = n and

         A4: for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_1:sch 2;

        z is FinSequence of BOOLEAN

        proof

          let a be object;

          assume a in ( rng z);

          then

          consider b be object such that

           A5: b in ( dom z) and

           A6: a = (z . b) by FUNCT_1:def 3;

          

           A7: b in ( Seg n) by A3, A5, FINSEQ_1:def 3;

          reconsider b as Element of NAT by A5;

          b >= 1 by A7, FINSEQ_1: 1;

          then

          reconsider c = (b - 1) as Element of NAT by INT_1: 5;

          (z . b) = (f . c) by A4, A5;

          hence thesis by A6;

        end;

        then

        reconsider z as Tuple of n, BOOLEAN by A3, CARD_1:def 7;

        take z;

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

        then 1 in ( Seg n);

        then

         A8: 1 in ( dom z) by A3, FINSEQ_1:def 3;

        

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

        .= (f . (1 - 1)) by A4, A8

        .= FALSE by A1;

        let i be Nat;

        assume that

         A9: 1 <= i and

         A10: i < n;

        consider j be Nat such that

         A11: (j + 1) = i by A9, NAT_1: 6;

        (j + 1) in ( Seg n) by A9, A10, A11;

        then

         A12: (j + 1) in ( dom z) by A3, FINSEQ_1:def 3;

        

        then

         A13: (z /. (j + 1)) = (z . (j + 1)) by PARTFUN1:def 6

        .= (f . ((j + 1) - 1)) by A4, A12

        .= (f . j);

        

         A14: ((i + 1) - 1) = i;

        1 <= (i + 1) & (i + 1) <= n by A9, A10, NAT_1: 13;

        then

         A15: (i + 1) in ( dom z) by A3, FINSEQ_3: 25;

        

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

        .= (f . (j + 1)) by A4, A11, A14, A15

        .= ((((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z /. i))) 'or' ((y /. i) '&' (z /. i))) by A2, A11, A13;

      end;

      uniqueness

      proof

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

         A16: (z1 /. 1) = FALSE and

         A17: for i be Nat st 1 <= i & i < n holds (z1 /. (i + 1)) = ((((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z1 /. i))) 'or' ((y /. i) '&' (z1 /. i))) and

         A18: (z2 /. 1) = FALSE and

         A19: for i be Nat st 1 <= i & i < n holds (z2 /. (i + 1)) = ((((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' (z2 /. i))) 'or' ((y /. i) '&' (z2 /. i)));

        

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

        

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

        then

         A22: ( dom z1) = ( Seg n) by FINSEQ_1:def 3;

        now

          defpred P[ Nat] means $1 in ( Seg n) implies (z1 /. $1) = (z2 /. $1);

          

           A23: ( dom z1) = ( Seg n) & ( dom z2) = ( Seg n) by A21, A20, FINSEQ_1:def 3;

           A24:

          now

            let k such that

             A25: P[k];

            thus P[(k + 1)]

            proof

              assume

               A26: (k + 1) in ( Seg n);

              per cases ;

                suppose k = 0 ;

                hence thesis by A16, A18;

              end;

                suppose

                 A27: k <> 0 ;

                (k + 1) <= n & k < (k + 1) by A26, FINSEQ_1: 1, XREAL_1: 29;

                then

                 A28: k < n by XXREAL_0: 2;

                

                 A29: k >= ( 0 + 1) by A27, NAT_1: 13;

                

                hence (z1 /. (k + 1)) = ((((x /. k) '&' (y /. k)) 'or' ((x /. k) '&' (z1 /. k))) 'or' ((y /. k) '&' (z1 /. k))) by A17, A28

                .= (z2 /. (k + 1)) by A19, A25, A29, A28;

              end;

            end;

          end;

          

           A30: P[ 0 ] by FINSEQ_1: 1;

          

           A31: for k holds P[k] from NAT_1:sch 2( A30, A24);

          let j be Nat such that

           A32: j in ( dom z1);

          

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

          .= (z2 /. j) by A22, A32, A31

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

        end;

        hence thesis by A21, A20, FINSEQ_2: 9;

      end;

    end

    definition

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

      :: BINARITH:def3

      func Binary (x) -> Tuple of n, NAT means

      : Def3: for i st i in ( Seg n) holds (it /. i) = ( IFEQ ((x /. i), FALSE , 0 ,(2 to_power (i -' 1))));

      existence

      proof

        deffunc F( Nat) = ( IFEQ ((x /. $1), FALSE , 0 ,(2 to_power ($1 -' 1))));

        consider z be FinSequence of NAT 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;

        reconsider z as Tuple of n, NAT by A1, CARD_1:def 7;

        take z;

        let j;

        assume

         A4: j in ( Seg n);

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

        

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

        .= ( IFEQ ((x /. j), FALSE , 0 ,(2 to_power (j -' 1)))) by A2, A3, A4;

      end;

      uniqueness

      proof

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

         A5: for i st i in ( Seg n) holds (z1 /. i) = ( IFEQ ((x /. i), FALSE , 0 ,(2 to_power (i -' 1)))) and

         A6: for i st i in ( Seg n) holds (z2 /. i) = ( IFEQ ((x /. i), FALSE , 0 ,(2 to_power (i -' 1))));

        

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

        then

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

        

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

        then

         A10: ( dom z2) = ( Seg n) by FINSEQ_1:def 3;

        now

          let j be Nat;

          assume

           A11: j in ( dom z1);

          

          hence (z1 . j) = (z1 /. j) by PARTFUN1:def 6

          .= ( IFEQ ((x /. j), FALSE , 0 ,(2 to_power (j -' 1)))) by A5, A8, A11

          .= (z2 /. j) by A6, A8, A11

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

        end;

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    definition

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

      :: BINARITH:def4

      func Absval (x) -> Element of NAT equals ( addnat $$ ( Binary x));

      correctness ;

    end

    definition

      let n, x, y;

      :: BINARITH:def5

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

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

      existence

      proof

        deffunc F( Nat) = (((x /. $1) 'xor' (y /. $1)) 'xor' (( carry (x,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;

        reconsider z as Tuple of n, BOOLEAN by A1, CARD_1:def 7;

        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' (y /. i)) 'xor' (( carry (x,y)) /. i)) by A2, A3, A4;

      end;

      uniqueness

      proof

        let z1, z2 such that

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

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

        

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

        then

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

        

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

        then

         A10: ( dom z2) = ( Seg n) by FINSEQ_1:def 3;

        now

          let j be Nat;

          assume

           A11: j in ( dom z1);

          

          hence (z1 . j) = (z1 /. j) by PARTFUN1:def 6

          .= (((x /. j) 'xor' (y /. j)) 'xor' (( carry (x,y)) /. j)) by A5, A8, A11

          .= (z2 /. j) by A6, A8, A11

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

        end;

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    definition

      let n, z1, z2;

      :: BINARITH:def6

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

      correctness ;

    end

    definition

      let n, z1, z2;

      :: BINARITH:def7

      pred z1,z2 are_summable means ( add_ovfl (z1,z2)) = FALSE ;

    end

    theorem :: BINARITH:14

    

     Th14: for z1 be Tuple of 1, BOOLEAN holds z1 = <* FALSE *> or z1 = <* TRUE *>

    proof

      let z1 be Tuple of 1, BOOLEAN ;

      

       A1: ex B be Element of BOOLEAN st z1 = <*B*> by FINSEQ_2: 97;

      per cases by XBOOLEAN:def 3;

        suppose (z1 /. 1) = FALSE ;

        hence thesis by A1, FINSEQ_4: 16;

      end;

        suppose (z1 /. 1) = TRUE ;

        hence thesis by A1, FINSEQ_4: 16;

      end;

    end;

    theorem :: BINARITH:15

    

     Th15: for z1 be Tuple of 1, BOOLEAN holds z1 = <* FALSE *> implies ( Absval z1) = 0

    proof

      let z1 be Tuple of 1, BOOLEAN ;

      

       A1: ex k be Element of NAT st ( Binary z1) = <*k*> by FINSEQ_2: 97;

      assume z1 = <* FALSE *>;

      then

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

      1 in ( Seg 1);

      

      then (( Binary z1) /. 1) = ( IFEQ ((z1 /. 1), FALSE , 0 ,(2 to_power (1 -' 1)))) by Def3

      .= 0 by A2, FUNCOP_1:def 8;

      

      hence ( Absval z1) = ( addnat $$ <* 0 *>) by A1, FINSEQ_4: 16

      .= 0 by FINSOP_1: 11;

    end;

    theorem :: BINARITH:16

    

     Th16: for z1 be Tuple of 1, BOOLEAN st z1 = <* TRUE *> holds ( Absval z1) = 1

    proof

      let z1 be Tuple of 1, BOOLEAN ;

      

       A1: (1 - 1) = 0 ;

      assume z1 = <* TRUE *>;

      then

       A2: (z1 /. 1) <> FALSE by FINSEQ_4: 16;

      1 in ( Seg 1);

      

      then

       A3: (( Binary z1) /. 1) = ( IFEQ ((z1 /. 1), FALSE , 0 ,(2 to_power (1 -' 1)))) by Def3

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

      ex k be Element of NAT st ( Binary z1) = <*k*> by FINSEQ_2: 97;

      

      hence ( Absval z1) = ( addnat $$ <*(2 to_power (1 -' 1))*>) by A3, FINSEQ_4: 16

      .= (2 to_power (1 -' 1)) by FINSOP_1: 11

      .= (2 to_power 0 ) by A1, XREAL_0:def 2

      .= 1 by POWER: 24;

    end;

    definition

      let n1,n2 be Nat;

      let D be non empty set;

      let z1 be Tuple of n1, D;

      let z2 be Tuple of n2, D;

      :: original: ^

      redefine

      func z1 ^ z2 -> Tuple of (n1 + n2), D ;

      coherence by FINSEQ_2: 107;

    end

    definition

      let D be non empty set;

      let d be Element of D;

      :: original: <*

      redefine

      func <*d*> -> Tuple of 1, D ;

      coherence

      proof

         <*d*> in (1 -tuples_on D) by FINSEQ_2: 98;

        hence thesis;

      end;

    end

    theorem :: BINARITH:17

    

     Th17: for z1,z2 be Tuple of n, BOOLEAN holds for d1,d2 be Element of BOOLEAN holds for i be Nat holds i in ( Seg n) implies (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i) = (( carry (z1,z2)) /. i)

    proof

      let z1,z2 be Tuple of n, BOOLEAN ;

      let d1,d2 be Element of BOOLEAN ;

      defpred P[ Nat] means $1 in ( Seg n) implies (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. $1) = (( carry (z1,z2)) /. $1);

      let i be Nat;

      

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

      proof

        let i be non zero Nat;

        assume

         A2: P[i];

        assume (i + 1) in ( Seg n);

        then (i + 1) > i & (i + 1) <= n by FINSEQ_1: 1, XREAL_1: 29;

        then

         A3: i < n by XXREAL_0: 2;

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

        then

         A4: i < (n + 1) by A3, XXREAL_0: 2;

        

         A5: 1 <= i by NAT_1: 14;

        then i in ( Seg n) by A3;

        then ((z1 ^ <*d1*>) /. i) = (z1 /. i) & ((z2 ^ <*d2*>) /. i) = (z2 /. i) by Th1;

        

        hence (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (i + 1)) = ((((z1 /. i) '&' (z2 /. i)) 'or' ((z1 /. i) '&' (( carry (z1,z2)) /. i))) 'or' ((z2 /. i) '&' (( carry (z1,z2)) /. i))) by A2, A5, A3, A4, Def2

        .= (( carry (z1,z2)) /. (i + 1)) by A5, A3, Def2;

      end;

      

       A6: P[1]

      proof

        assume 1 in ( Seg n);

        

        thus (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. 1) = FALSE by Def2

        .= (( carry (z1,z2)) /. 1) by Def2;

      end;

      

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

      assume

       A8: i in ( Seg n);

      then i is non zero by FINSEQ_1: 1;

      hence thesis by A8, A7;

    end;

    theorem :: BINARITH:18

    

     Th18: for z1,z2 be Tuple of n, BOOLEAN , d1,d2 be Element of BOOLEAN holds ( add_ovfl (z1,z2)) = (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (n + 1))

    proof

      let z1,z2 be Tuple of n, BOOLEAN , d1,d2 be Element of BOOLEAN ;

      

       A1: 1 <= n & n < (n + 1) by NAT_1: 14, XREAL_1: 29;

      

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

      then

       A3: (z2 /. n) = ((z2 ^ <*d2*>) /. n) by Th1;

      (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. n) = (( carry (z1,z2)) /. n) & (z1 /. n) = ((z1 ^ <*d1*>) /. n) by A2, Th1, Th17;

      hence thesis by A3, A1, Def2;

    end;

    theorem :: BINARITH:19

    

     Th19: for z1,z2 be Tuple of n, BOOLEAN , d1,d2 be Element of BOOLEAN holds ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) = ((z1 + z2) ^ <*((d1 'xor' d2) 'xor' ( add_ovfl (z1,z2)))*>)

    proof

      let z1,z2 be Tuple of n, BOOLEAN , d1,d2 be Element of BOOLEAN ;

      for i st i in ( Seg (n + 1)) holds (((z1 + z2) ^ <*((d1 'xor' d2) 'xor' ( add_ovfl (z1,z2)))*>) /. i) = ((((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i))

      proof

        

         A1: ( Seg (n + 1)) = (( Seg n) \/ {.(n + 1).}) by FINSEQ_1: 9;

        let i such that

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

        per cases by A2, A1, XBOOLE_0:def 3;

          suppose

           A3: i in ( Seg n);

          

          hence (((z1 + z2) ^ <*((d1 'xor' d2) 'xor' ( add_ovfl (z1,z2)))*>) /. i) = ((z1 + z2) /. i) by Th1

          .= (((z1 /. i) 'xor' (z2 /. i)) 'xor' (( carry (z1,z2)) /. i)) by A3, Def5

          .= ((((z1 ^ <*d1*>) /. i) 'xor' (z2 /. i)) 'xor' (( carry (z1,z2)) /. i)) by A3, Th1

          .= ((((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' (( carry (z1,z2)) /. i)) by A3, Th1

          .= ((((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i)) by A3, Th17;

        end;

          suppose i in {.(n + 1).};

          then

           A4: i = (n + 1) by TARSKI:def 1;

          

          hence (((z1 + z2) ^ <*((d1 'xor' d2) 'xor' ( add_ovfl (z1,z2)))*>) /. i) = ((d1 'xor' d2) 'xor' ( add_ovfl (z1,z2))) by Th2

          .= ((d1 'xor' d2) 'xor' (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i)) by A4, Th18

          .= ((d1 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i)) by A4, Th2

          .= ((((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' (( carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i)) by A4, Th2;

        end;

      end;

      hence thesis by Def5;

    end;

    theorem :: BINARITH:20

    

     Th20: for z be Tuple of n, BOOLEAN , d be Element of BOOLEAN holds ( Absval (z ^ <*d*>)) = (( Absval z) + ( IFEQ (d, FALSE , 0 ,(2 to_power n))))

    proof

      let z be Tuple of n, BOOLEAN , d be Element of BOOLEAN ;

      for i st i in ( Seg (n + 1)) holds ((( Binary z) ^ <*( IFEQ (d, FALSE , 0 ,(2 to_power n)))*>) /. i) = ( IFEQ (((z ^ <*d*>) /. i), FALSE , 0 ,(2 to_power (i -' 1))))

      proof

        

         A1: ( Seg (n + 1)) = (( Seg n) \/ {.(n + 1).}) by FINSEQ_1: 9;

        let i such that

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

        per cases by A2, A1, XBOOLE_0:def 3;

          suppose

           A3: i in ( Seg n);

          

          hence ((( Binary z) ^ <*( IFEQ (d, FALSE , 0 ,(2 to_power n)))*>) /. i) = (( Binary z) /. i) by Th1

          .= ( IFEQ ((z /. i), FALSE , 0 ,(2 to_power (i -' 1)))) by A3, Def3

          .= ( IFEQ (((z ^ <*d*>) /. i), FALSE , 0 ,(2 to_power (i -' 1)))) by A3, Th1;

        end;

          suppose i in {.(n + 1).};

          then

           A4: i = (n + 1) by TARSKI:def 1;

          

          hence ((( Binary z) ^ <*( IFEQ (d, FALSE , 0 ,(2 to_power n)))*>) /. i) = ( IFEQ (d, FALSE , 0 ,(2 to_power n))) by Th2

          .= ( IFEQ (((z ^ <*d*>) /. i), FALSE , 0 ,(2 to_power n))) by A4, Th2

          .= ( IFEQ (((z ^ <*d*>) /. i), FALSE , 0 ,(2 to_power (i -' 1)))) by A4, NAT_D: 34;

        end;

      end;

      

      hence ( Absval (z ^ <*d*>)) = ( addnat $$ (( Binary z) ^ <*( IFEQ (d, FALSE , 0 ,(2 to_power n)))*>)) by Def3

      .= ( addnat . (( addnat $$ ( Binary z)),( IFEQ (d, FALSE , 0 ,(2 to_power n))))) by FINSOP_1: 4

      .= (( Absval z) + ( IFEQ (d, FALSE , 0 ,(2 to_power n)))) by BINOP_2:def 23;

    end;

    theorem :: BINARITH:21

    

     Th21: for n holds for z1,z2 be Tuple of n, BOOLEAN holds (( Absval (z1 + z2)) + ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power n)))) = (( Absval z1) + ( Absval z2))

    proof

      defpred P[ non zero Nat] means for z1,z2 be Tuple of $1, BOOLEAN holds (( Absval (z1 + z2)) + ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power $1)))) = (( Absval z1) + ( Absval z2));

      set f = FALSE , t = TRUE ;

      

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

      proof

        let n;

        assume

         A2: P[n];

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

        consider t1 be Element of (n -tuples_on BOOLEAN ), d1 be Element of BOOLEAN such that

         A3: z1 = (t1 ^ <*d1*>) by FINSEQ_2: 117;

        consider t2 be Element of (n -tuples_on BOOLEAN ), d2 be Element of BOOLEAN such that

         A4: z2 = (t2 ^ <*d2*>) by FINSEQ_2: 117;

        reconsider C1 = ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power (n + 1)))), C2 = ( IFEQ (((d1 'xor' d2) 'xor' ( add_ovfl (t1,t2))), FALSE , 0 ,(2 to_power n))), C3 = ( IFEQ (d1, FALSE , 0 ,(2 to_power n))), C4 = ( IFEQ (d2, FALSE , 0 ,(2 to_power n))), C5 = ( IFEQ (( add_ovfl (t1,t2)), FALSE , 0 ,(2 to_power n))) as Real;

        

         A5: ( add_ovfl (z1,z2)) = (((d1 '&' ((t2 ^ <*d2*>) /. (n + 1))) 'or' (((t1 ^ <*d1*>) /. (n + 1)) '&' (( carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) 'or' (((t2 ^ <*d2*>) /. (n + 1)) '&' (( carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) by A3, A4, Th2

        .= (((d1 '&' d2) 'or' (((t1 ^ <*d1*>) /. (n + 1)) '&' (( carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) 'or' (((t2 ^ <*d2*>) /. (n + 1)) '&' (( carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) by Th2

        .= (((d1 '&' d2) 'or' (d1 '&' (( carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) 'or' (((t2 ^ <*d2*>) /. (n + 1)) '&' (( carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) by Th2

        .= (((d1 '&' d2) 'or' (d1 '&' (( carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) 'or' (d2 '&' (( carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) by Th2

        .= (((d1 '&' d2) 'or' (d1 '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' (( carry ((t1 ^ <*d1*>),(t2 ^ <*d2*>))) /. (n + 1)))) by Th18

        .= (((d1 '&' d2) 'or' (d1 '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' ( add_ovfl (t1,t2)))) by Th18;

        

         A6: (C2 + C1) = ((C5 + C3) + C4)

        proof

          now

            per cases ;

              suppose

               A7: d1 = f;

              then

               A8: C3 = 0 by FUNCOP_1:def 8;

              now

                per cases ;

                  suppose

                   A9: d2 = f;

                  then C4 = 0 by FUNCOP_1:def 8;

                  hence thesis by A5, A7, A9, FUNCOP_1:def 8;

                end;

                  suppose

                   A10: d2 <> f;

                  then

                   A11: C4 = (2 to_power n) by FUNCOP_1:def 8;

                  now

                    per cases ;

                      suppose

                       A12: ( add_ovfl (t1,t2)) = f;

                      then C5 = 0 by FUNCOP_1:def 8;

                      hence thesis by A5, A7, A12, FUNCOP_1:def 8;

                    end;

                      suppose

                       A13: ( add_ovfl (t1,t2)) <> f;

                      ((d1 'xor' d2) 'xor' ( add_ovfl (t1,t2))) = (t 'xor' ( add_ovfl (t1,t2))) by A7, A10, XBOOLEAN:def 3

                      .= f by A13, XBOOLEAN:def 3;

                      then

                       A14: C2 = 0 by FUNCOP_1:def 8;

                      

                       A15: C5 = (2 to_power n) by A13, FUNCOP_1:def 8;

                      (((d1 '&' d2) 'or' (d1 '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' ( add_ovfl (t1,t2)))) = ((f 'or' f) 'or' (t '&' ( add_ovfl (t1,t2)))) by A7, A10, XBOOLEAN:def 3

                      .= t by A13, XBOOLEAN:def 3;

                      then C1 = (2 to_power (n + 1)) by A5, FUNCOP_1:def 8;

                      

                      hence (C2 + C1) = ((2 to_power n) * (2 to_power 1)) by A14, POWER: 27

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

                      .= ((C5 + C3) + C4) by A8, A11, A15;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

              suppose

               A16: d1 <> f;

              then

               A17: C3 = (2 to_power n) by FUNCOP_1:def 8;

              now

                per cases ;

                  suppose

                   A18: d2 = f;

                  then

                   A19: C4 = 0 by FUNCOP_1:def 8;

                  now

                    per cases ;

                      suppose ( add_ovfl (t1,t2)) = f;

                      hence thesis by A5, A18, A19, FUNCOP_1:def 8;

                    end;

                      suppose

                       A20: ( add_ovfl (t1,t2)) <> f;

                      ((d1 'xor' d2) 'xor' ( add_ovfl (t1,t2))) = (t 'xor' ( add_ovfl (t1,t2))) by A16, A18, XBOOLEAN:def 3

                      .= f by A20, XBOOLEAN:def 3;

                      then

                       A21: C2 = 0 by FUNCOP_1:def 8;

                      

                       A22: C5 = (2 to_power n) by A20, FUNCOP_1:def 8;

                      (((d1 '&' d2) 'or' (d1 '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' ( add_ovfl (t1,t2)))) = ((f 'or' (t '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' ( add_ovfl (t1,t2)))) by A16, A18, XBOOLEAN:def 3

                      .= ((f 'or' (t '&' t)) 'or' (d2 '&' ( add_ovfl (t1,t2)))) by A20, XBOOLEAN:def 3

                      .= t;

                      then C1 = (2 to_power (n + 1)) by A5, FUNCOP_1:def 8;

                      

                      hence (C2 + C1) = ((2 to_power n) * (2 to_power 1)) by A21, POWER: 27

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

                      .= ((C5 + C3) + C4) by A17, A19, A22;

                    end;

                  end;

                  hence thesis;

                end;

                  suppose

                   A23: d2 <> f;

                  then

                   A24: C4 = (2 to_power n) by FUNCOP_1:def 8;

                  now

                    per cases ;

                      suppose

                       A25: ( add_ovfl (t1,t2)) = f;

                      ((d1 'xor' d2) 'xor' ( add_ovfl (t1,t2))) = ((t 'xor' d2) 'xor' ( add_ovfl (t1,t2))) by A16, XBOOLEAN:def 3

                      .= f by A23, A25, XBOOLEAN:def 3;

                      then

                       A26: C2 = 0 by FUNCOP_1:def 8;

                      

                       A27: C5 = 0 by A25, FUNCOP_1:def 8;

                      (((d1 '&' d2) 'or' (d1 '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' ( add_ovfl (t1,t2)))) = (((t '&' d2) 'or' (d1 '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' ( add_ovfl (t1,t2)))) by A16, XBOOLEAN:def 3

                      .= (((t '&' t) 'or' (d1 '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' ( add_ovfl (t1,t2)))) by A23, XBOOLEAN:def 3

                      .= t;

                      then C1 = (2 to_power (n + 1)) by A5, FUNCOP_1:def 8;

                      

                      hence (C2 + C1) = ((2 to_power n) * (2 to_power 1)) by A26, POWER: 27

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

                      .= ((C5 + C3) + C4) by A17, A24, A27;

                    end;

                      suppose

                       A28: ( add_ovfl (t1,t2)) <> f;

                      ((d1 'xor' d2) 'xor' ( add_ovfl (t1,t2))) = ((t 'xor' d2) 'xor' ( add_ovfl (t1,t2))) by A16, XBOOLEAN:def 3

                      .= (f 'xor' ( add_ovfl (t1,t2))) by A23, XBOOLEAN:def 3

                      .= t by A28, XBOOLEAN:def 3;

                      then

                       A29: C2 = (2 to_power n) by FUNCOP_1:def 8;

                      (((d1 '&' d2) 'or' (d1 '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' ( add_ovfl (t1,t2)))) = (((t '&' d2) 'or' (d1 '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' ( add_ovfl (t1,t2)))) by A16, XBOOLEAN:def 3

                      .= (((t '&' t) 'or' (d1 '&' ( add_ovfl (t1,t2)))) 'or' (d2 '&' ( add_ovfl (t1,t2)))) by A23, XBOOLEAN:def 3

                      .= t;

                      then C1 = (2 to_power (n + 1)) by A5, FUNCOP_1:def 8;

                      

                      hence (C2 + C1) = ((2 to_power n) + ((2 to_power n) * (2 to_power 1))) by A29, POWER: 27

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

                      .= (((2 to_power n) + (2 to_power n)) + (2 to_power n))

                      .= ((C5 + C3) + C4) by A17, A24, A28, FUNCOP_1:def 8;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        

        thus (( Absval (z1 + z2)) + ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power (n + 1))))) = (( Absval ((t1 + t2) ^ <*((d1 'xor' d2) 'xor' ( add_ovfl (t1,t2)))*>)) + ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power (n + 1))))) by A3, A4, Th19

        .= ((( Absval (t1 + t2)) + C2) + C1) by Th20

        .= (((( Absval (t1 + t2)) + C5) + C3) + C4) by A6

        .= (((( Absval t1) + ( Absval t2)) + C3) + C4) by A2

        .= ((( Absval t1) + C3) + (( Absval t2) + C4))

        .= ((( Absval t1) + ( IFEQ (d1, FALSE , 0 ,(2 to_power n)))) + ( Absval (t2 ^ <*d2*>))) by Th20

        .= (( Absval z1) + ( Absval z2)) by A3, A4, Th20;

      end;

      

       A30: P[1]

      proof

        reconsider T = <*t*>, F = <*f*> as Tuple of 1, BOOLEAN ;

        let z1,z2 be Tuple of 1, BOOLEAN ;

        

         A31: (( carry (z1,z2)) /. 1) = f by Def2;

        

         A32: ( Absval T) = 1 by Th16;

        

         A33: ( Absval F) = 0 by Th15;

        per cases by Th14;

          suppose

           A34: z1 = <*f*> & z2 = <*f*>;

           A35:

          now

            let i;

            assume

             A36: i in ( Seg 1);

            then

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

            

            thus (F /. i) = (((z1 /. 1) 'xor' f) 'xor' f) by A34, A36, FINSEQ_1: 2, TARSKI:def 1

            .= (((z1 /. 1) 'xor' (z2 /. 1)) 'xor' f) by A34, FINSEQ_4: 16

            .= (((z1 /. i) 'xor' (z2 /. i)) 'xor' (( carry (z1,z2)) /. i)) by A37, Def2;

          end;

          ( add_ovfl (z1,z2)) = f by A31, A34, FINSEQ_4: 16;

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

          hence thesis by A33, A34, A35, Def5;

        end;

          suppose

           A38: z1 = <*t*> & z2 = <*f*>;

           A39:

          now

            let i;

            assume

             A40: i in ( Seg 1);

            then

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

            

            thus (T /. i) = (((z1 /. 1) 'xor' f) 'xor' f) by A38, A40, FINSEQ_1: 2, TARSKI:def 1

            .= (((z1 /. 1) 'xor' (z2 /. 1)) 'xor' f) by A38, FINSEQ_4: 16

            .= (((z1 /. i) 'xor' (z2 /. i)) 'xor' (( carry (z1,z2)) /. i)) by A41, Def2;

          end;

          ( add_ovfl (z1,z2)) = f by A31, A38, FINSEQ_4: 16;

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

          hence thesis by A33, A38, A39, Def5;

        end;

          suppose

           A42: z1 = <*f*> & z2 = <*t*>;

           A43:

          now

            let i;

            assume i in ( Seg 1);

            then

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

            

            hence (T /. i) = ((( 'not' t) 'xor' t) 'xor' f) by FINSEQ_4: 16

            .= (((z1 /. 1) 'xor' t) 'xor' f) by A42, FINSEQ_4: 16

            .= (((z1 /. 1) 'xor' (z2 /. 1)) 'xor' f) by A42, FINSEQ_4: 16

            .= (((z1 /. i) 'xor' (z2 /. i)) 'xor' (( carry (z1,z2)) /. i)) by A44, Def2;

          end;

          ( add_ovfl (z1,z2)) = f by A31, A42, FINSEQ_4: 16;

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

          hence thesis by A33, A42, A43, Def5;

        end;

          suppose

           A45: z1 = <*t*> & z2 = <*t*>;

          now

            let i;

            assume i in ( Seg 1);

            then

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

            

            hence (F /. i) = ((t 'xor' t) 'xor' ( 'not' t)) by FINSEQ_4: 16

            .= (((z1 /. 1) 'xor' t) 'xor' f) by A45, FINSEQ_4: 16

            .= (((z1 /. 1) 'xor' (z2 /. 1)) 'xor' f) by A45, FINSEQ_4: 16

            .= (((z1 /. i) 'xor' (z2 /. i)) 'xor' (( carry (z1,z2)) /. i)) by A46, Def2;

          end;

          then

           A47: (z1 + z2) = <*f*> by Def5;

          ( add_ovfl (z1,z2)) = t by A31, A45, FINSEQ_4: 16;

          

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

          .= 2 by POWER: 25;

          hence thesis by A32, A33, A45, A47;

        end;

      end;

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

    end;

    theorem :: BINARITH:22

    for z1,z2 be Tuple of n, BOOLEAN st (z1,z2) are_summable holds ( Absval (z1 + z2)) = (( Absval z1) + ( Absval z2))

    proof

      let z1,z2 be Tuple of n, BOOLEAN ;

      assume (z1,z2) are_summable ;

      then ( add_ovfl (z1,z2)) = FALSE ;

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

      

      hence ( Absval (z1 + z2)) = (( Absval (z1 + z2)) + ( IFEQ (( add_ovfl (z1,z2)), FALSE , 0 ,(2 to_power n))))

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

    end;