twoscomp.miz



    begin

    definition

      let S be unsplit non void non empty ManySortedSign;

      let A be Boolean Circuit of S;

      let s be State of A;

      let v be Vertex of S;

      :: original: .

      redefine

      func s . v -> Element of BOOLEAN ;

      coherence

      proof

        (s . v) in (the Sorts of A . v) by CIRCUIT1: 4;

        hence thesis;

      end;

    end

    deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ($1 '&' $2);

    notation

      synonym and2 for '&' ;

    end

    ::$Canceled

    definition

      :: TWOSCOMP:def1

      func and2a -> Function of (2 -tuples_on BOOLEAN ), BOOLEAN means

      : Def1: for x,y be Element of BOOLEAN holds (it . <*x, y*>) = (( 'not' x) '&' y);

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = (( 'not' $1) '&' $2);

        thus ex t be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st for x,y be Element of BOOLEAN holds (t . <*x, y*>) = U(x,y) from FACIRC_1:sch 1;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = (( 'not' $1) '&' $2);

        thus for t1,t2 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st (for x,y be Element of BOOLEAN holds (t1 . <*x, y*>) = U(x,y)) & (for x,y be Element of BOOLEAN holds (t2 . <*x, y*>) = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;

      end;

    end

    ::$Canceled

    definition

      :: TWOSCOMP:def2

      func nand2 -> Function of (2 -tuples_on BOOLEAN ), BOOLEAN means

      : Def2: for x,y be Element of BOOLEAN holds (it . <*x, y*>) = ( 'not' (x '&' y));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ($1 '&' $2));

        thus ex t be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st for x,y be Element of BOOLEAN holds (t . <*x, y*>) = U(x,y) from FACIRC_1:sch 1;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ($1 '&' $2));

        thus for t1,t2 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st (for x,y be Element of BOOLEAN holds (t1 . <*x, y*>) = U(x,y)) & (for x,y be Element of BOOLEAN holds (t2 . <*x, y*>) = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;

      end;

      :: TWOSCOMP:def3

      func nand2a -> Function of (2 -tuples_on BOOLEAN ), BOOLEAN means

      : Def3: for x,y be Element of BOOLEAN holds (it . <*x, y*>) = ( 'not' (( 'not' x) '&' y));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' (( 'not' $1) '&' $2));

        thus ex t be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st for x,y be Element of BOOLEAN holds (t . <*x, y*>) = U(x,y) from FACIRC_1:sch 1;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' (( 'not' $1) '&' $2));

        thus for t1,t2 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st (for x,y be Element of BOOLEAN holds (t1 . <*x, y*>) = U(x,y)) & (for x,y be Element of BOOLEAN holds (t2 . <*x, y*>) = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;

      end;

    end

    notation

      synonym or2 for 'or' ;

    end

    

     Lm1: for x,y be Element of BOOLEAN holds ( or2 . <*x, y*>) = ( 'not' (( 'not' x) '&' ( 'not' y)))

    proof

      let x,y be Element of BOOLEAN ;

      

      thus ( or2 . <*x, y*>) = (x 'or' y) by FACIRC_1:def 5

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

    end;

    ::$Canceled

    definition

      :: TWOSCOMP:def4

      func or2a -> Function of (2 -tuples_on BOOLEAN ), BOOLEAN means

      : Def4: for x,y be Element of BOOLEAN holds (it . <*x, y*>) = (( 'not' x) 'or' y);

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = (( 'not' $1) 'or' $2);

        thus ex t be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st for x,y be Element of BOOLEAN holds (t . <*x, y*>) = U(x,y) from FACIRC_1:sch 1;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = (( 'not' $1) 'or' $2);

        thus for t1,t2 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st (for x,y be Element of BOOLEAN holds (t1 . <*x, y*>) = U(x,y)) & (for x,y be Element of BOOLEAN holds (t2 . <*x, y*>) = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;

      end;

    end

    

     Lm2: for x,y be Element of BOOLEAN holds ( nand2 . <*x, y*>) = (( 'not' x) 'or' ( 'not' y)) by Def2;

    ::$Canceled

    definition

      :: TWOSCOMP:def5

      func nor2 -> Function of (2 -tuples_on BOOLEAN ), BOOLEAN means

      : Def5: for x,y be Element of BOOLEAN holds (it . <*x, y*>) = ( 'not' (x 'or' y));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ($1 'or' $2));

        thus ex t be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st for x,y be Element of BOOLEAN holds (t . <*x, y*>) = U(x,y) from FACIRC_1:sch 1;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ($1 'or' $2));

        thus for t1,t2 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st (for x,y be Element of BOOLEAN holds (t1 . <*x, y*>) = U(x,y)) & (for x,y be Element of BOOLEAN holds (t2 . <*x, y*>) = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;

      end;

      :: TWOSCOMP:def6

      func nor2a -> Function of (2 -tuples_on BOOLEAN ), BOOLEAN means

      : Def6: for x,y be Element of BOOLEAN holds (it . <*x, y*>) = ( 'not' (( 'not' x) 'or' y));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' (( 'not' $1) 'or' $2));

        thus ex t be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st for x,y be Element of BOOLEAN holds (t . <*x, y*>) = U(x,y) from FACIRC_1:sch 1;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' (( 'not' $1) 'or' $2));

        thus for t1,t2 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st (for x,y be Element of BOOLEAN holds (t1 . <*x, y*>) = U(x,y)) & (for x,y be Element of BOOLEAN holds (t2 . <*x, y*>) = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;

      end;

    end

    

     Lm3: for x,y be Element of BOOLEAN holds ( nor2 . <*x, y*>) = (( 'not' x) '&' ( 'not' y))

    proof

      let x,y be Element of BOOLEAN ;

      

      thus ( nor2 . <*x, y*>) = ( 'not' (x 'or' y)) by Def5

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

    end;

    notation

      synonym xor2 for 'xor' ;

    end

    

     Lm4: for x,y be Element of BOOLEAN holds ( and2 . <*x, y*>) = ( 'not' (( 'not' x) 'or' ( 'not' y))) by FACIRC_1:def 6;

    ::$Canceled

    definition

      :: TWOSCOMP:def7

      func xor2a -> Function of (2 -tuples_on BOOLEAN ), BOOLEAN means

      : Def7: for x,y be Element of BOOLEAN holds (it . <*x, y*>) = (( 'not' x) 'xor' y);

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = (( 'not' $1) 'xor' $2);

        thus ex t be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st for x,y be Element of BOOLEAN holds (t . <*x, y*>) = U(x,y) from FACIRC_1:sch 1;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = (( 'not' $1) 'xor' $2);

        thus for t1,t2 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st (for x,y be Element of BOOLEAN holds (t1 . <*x, y*>) = U(x,y)) & (for x,y be Element of BOOLEAN holds (t2 . <*x, y*>) = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;

      end;

      :: TWOSCOMP:def8

      func xor2b -> Function of (2 -tuples_on BOOLEAN ), BOOLEAN means

      : Def8: for x,y be Element of BOOLEAN holds (it . <*x, y*>) = (( 'not' x) 'xor' ( 'not' y));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = (( 'not' $1) 'xor' ( 'not' $2));

        thus ex t be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st for x,y be Element of BOOLEAN holds (t . <*x, y*>) = U(x,y) from FACIRC_1:sch 1;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = (( 'not' $1) 'xor' ( 'not' $2));

        thus for t1,t2 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st (for x,y be Element of BOOLEAN holds (t1 . <*x, y*>) = U(x,y)) & (for x,y be Element of BOOLEAN holds (t2 . <*x, y*>) = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;

      end;

    end

    theorem :: TWOSCOMP:1

    for x,y be Element of BOOLEAN holds ( and2 . <*x, y*>) = (x '&' y) & ( and2a . <*x, y*>) = (( 'not' x) '&' y) & ( nor2 . <*x, y*>) = (( 'not' x) '&' ( 'not' y)) by FACIRC_1:def 6, Def1, Lm3;

    theorem :: TWOSCOMP:2

    for x,y be Element of BOOLEAN holds ( nand2 . <*x, y*>) = ( 'not' (x '&' y)) & ( nand2a . <*x, y*>) = ( 'not' (( 'not' x) '&' y)) & ( or2 . <*x, y*>) = ( 'not' (( 'not' x) '&' ( 'not' y))) by Def2, Def3, Lm1;

    theorem :: TWOSCOMP:3

    for x,y be Element of BOOLEAN holds ( or2 . <*x, y*>) = (x 'or' y) & ( or2a . <*x, y*>) = (( 'not' x) 'or' y) & ( nand2 . <*x, y*>) = (( 'not' x) 'or' ( 'not' y)) by FACIRC_1:def 5, Def4, Lm2;

    theorem :: TWOSCOMP:4

    for x,y be Element of BOOLEAN holds ( nor2 . <*x, y*>) = ( 'not' (x 'or' y)) & ( nor2a . <*x, y*>) = ( 'not' (( 'not' x) 'or' y)) & ( and2 . <*x, y*>) = ( 'not' (( 'not' x) 'or' ( 'not' y))) by Def5, Def6, Lm4;

    theorem :: TWOSCOMP:5

    for x,y be Element of BOOLEAN holds ( xor2 . <*x, y*>) = (x 'xor' y) & ( xor2a . <*x, y*>) = (( 'not' x) 'xor' y) & ( xor2b . <*x, y*>) = (( 'not' x) 'xor' ( 'not' y)) by FACIRC_1:def 4, Def7, Def8;

    theorem :: TWOSCOMP:6

    for x,y be Element of BOOLEAN holds ( and2a . <*x, y*>) = ( nor2a . <*y, x*>)

    proof

      let x,y be Element of BOOLEAN ;

      

      thus ( and2a . <*x, y*>) = ( 'not' (( 'not' ( 'not' x)) 'or' ( 'not' y))) by Def1

      .= ( nor2a . <*y, x*>) by Def6;

    end;

    theorem :: TWOSCOMP:7

    for x,y be Element of BOOLEAN holds ( or2a . <*x, y*>) = ( nand2a . <*y, x*>)

    proof

      let x,y be Element of BOOLEAN ;

      

      thus ( or2a . <*x, y*>) = (( 'not' x) 'or' y) by Def4

      .= ( nand2a . <*y, x*>) by Def3;

    end;

    theorem :: TWOSCOMP:8

    for x,y be Element of BOOLEAN holds ( xor2b . <*x, y*>) = ( xor2 . <*x, y*>)

    proof

      let x,y be Element of BOOLEAN ;

      

      thus ( xor2b . <*x, y*>) = (( 'not' x) 'xor' ( 'not' y)) by Def8

      .= (x 'xor' y)

      .= ( xor2 . <*x, y*>) by FACIRC_1:def 4;

    end;

    theorem :: TWOSCOMP:9

    ( and2 . <* 0 , 0 *>) = 0 & ( and2 . <* 0 , 1*>) = 0 & ( and2 . <*1, 0 *>) = 0 & ( and2 . <*1, 1*>) = 1 & ( and2a . <* 0 , 0 *>) = 0 & ( and2a . <* 0 , 1*>) = 1 & ( and2a . <*1, 0 *>) = 0 & ( and2a . <*1, 1*>) = 0 & ( nor2 . <* 0 , 0 *>) = 1 & ( nor2 . <* 0 , 1*>) = 0 & ( nor2 . <*1, 0 *>) = 0 & ( nor2 . <*1, 1*>) = 0

    proof

      

      thus ( and2 . <* 0 , 0 *>) = ( FALSE '&' FALSE ) by FACIRC_1:def 6

      .= 0 ;

      

      thus ( and2 . <* 0 , 1*>) = ( FALSE '&' TRUE ) by FACIRC_1:def 6

      .= 0 ;

      

      thus ( and2 . <*1, 0 *>) = ( TRUE '&' FALSE ) by FACIRC_1:def 6

      .= 0 ;

      

      thus ( and2 . <*1, 1*>) = ( TRUE '&' TRUE ) by FACIRC_1:def 6

      .= 1;

      

      thus ( and2a . <* 0 , 0 *>) = (( 'not' FALSE ) '&' FALSE ) by Def1

      .= 0 ;

      

      thus ( and2a . <* 0 , 1*>) = (( 'not' FALSE ) '&' TRUE ) by Def1

      .= 1;

      

      thus ( and2a . <*1, 0 *>) = (( 'not' TRUE ) '&' FALSE ) by Def1

      .= 0 ;

      

      thus ( and2a . <*1, 1*>) = (( 'not' TRUE ) '&' TRUE ) by Def1

      .= 0 ;

      

      thus ( nor2 . <* 0 , 0 *>) = ( TRUE '&' ( 'not' FALSE )) by Lm3

      .= 1;

      

      thus ( nor2 . <* 0 , 1*>) = (( 'not' FALSE ) '&' ( 'not' TRUE )) by Lm3

      .= 0 ;

      

      thus ( nor2 . <*1, 0 *>) = (( 'not' TRUE ) '&' ( 'not' FALSE )) by Lm3

      .= 0 ;

      

      thus ( nor2 . <*1, 1*>) = ( FALSE '&' ( 'not' TRUE )) by Lm3

      .= 0 ;

    end;

    theorem :: TWOSCOMP:10

    ( or2 . <* 0 , 0 *>) = 0 & ( or2 . <* 0 , 1*>) = 1 & ( or2 . <*1, 0 *>) = 1 & ( or2 . <*1, 1*>) = 1 & ( or2a . <* 0 , 0 *>) = 1 & ( or2a . <* 0 , 1*>) = 1 & ( or2a . <*1, 0 *>) = 0 & ( or2a . <*1, 1*>) = 1 & ( nand2 . <* 0 , 0 *>) = 1 & ( nand2 . <* 0 , 1*>) = 1 & ( nand2 . <*1, 0 *>) = 1 & ( nand2 . <*1, 1*>) = 0

    proof

      

      thus ( or2 . <* 0 , 0 *>) = ( FALSE 'or' FALSE ) by FACIRC_1:def 5

      .= 0 ;

      

      thus ( or2 . <* 0 , 1*>) = ( FALSE 'or' TRUE ) by FACIRC_1:def 5

      .= 1;

      

      thus ( or2 . <*1, 0 *>) = ( TRUE 'or' FALSE ) by FACIRC_1:def 5

      .= 1;

      

      thus ( or2 . <*1, 1*>) = ( TRUE 'or' TRUE ) by FACIRC_1:def 5

      .= 1;

      

      thus ( or2a . <* 0 , 0 *>) = ( TRUE 'or' FALSE ) by Def4

      .= 1;

      

      thus ( or2a . <* 0 , 1*>) = (( 'not' FALSE ) 'or' TRUE ) by Def4

      .= 1;

      

      thus ( or2a . <*1, 0 *>) = (( 'not' TRUE ) 'or' FALSE ) by Def4

      .= 0 ;

      

      thus ( or2a . <*1, 1*>) = (( 'not' TRUE ) 'or' TRUE ) by Def4

      .= 1;

      

      thus ( nand2 . <* 0 , 0 *>) = ( TRUE 'or' ( 'not' FALSE )) by Lm2

      .= 1;

      

      thus ( nand2 . <* 0 , 1*>) = ( TRUE 'or' ( 'not' TRUE )) by Lm2

      .= 1;

      

      thus ( nand2 . <*1, 0 *>) = (( 'not' TRUE ) 'or' TRUE ) by Lm2

      .= 1;

      

      thus ( nand2 . <*1, 1*>) = ( FALSE 'or' ( 'not' TRUE )) by Lm2

      .= 0 ;

    end;

    theorem :: TWOSCOMP:11

    ( xor2 . <* 0 , 0 *>) = 0 & ( xor2 . <* 0 , 1*>) = 1 & ( xor2 . <*1, 0 *>) = 1 & ( xor2 . <*1, 1*>) = 0 & ( xor2a . <* 0 , 0 *>) = 1 & ( xor2a . <* 0 , 1*>) = 0 & ( xor2a . <*1, 0 *>) = 0 & ( xor2a . <*1, 1*>) = 1

    proof

      

      thus ( xor2 . <* 0 , 0 *>) = ( FALSE 'xor' FALSE ) by FACIRC_1:def 4

      .= 0 ;

      

      thus ( xor2 . <* 0 , 1*>) = ( FALSE 'xor' TRUE ) by FACIRC_1:def 4

      .= 1;

      

      thus ( xor2 . <*1, 0 *>) = ( TRUE 'xor' FALSE ) by FACIRC_1:def 4

      .= 1;

      

      thus ( xor2 . <*1, 1*>) = ( TRUE 'xor' TRUE ) by FACIRC_1:def 4

      .= 0 ;

      

      thus ( xor2a . <* 0 , 0 *>) = (( 'not' FALSE ) 'xor' FALSE ) by Def7

      .= 1;

      

      thus ( xor2a . <* 0 , 1*>) = (( 'not' FALSE ) 'xor' TRUE ) by Def7

      .= 0 ;

      

      thus ( xor2a . <*1, 0 *>) = (( 'not' TRUE ) 'xor' FALSE ) by Def7

      .= 0 ;

      

      thus ( xor2a . <*1, 1*>) = (( 'not' TRUE ) 'xor' TRUE ) by Def7

      .= 1;

    end;

    definition

      :: TWOSCOMP:def9

      func and3 -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def9: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ((x '&' y) '&' z);

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = (($1 '&' $2) '&' $3);

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = (($1 '&' $2) '&' $3);

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

      :: TWOSCOMP:def10

      func and3a -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def10: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ((( 'not' x) '&' y) '&' z);

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ((( 'not' $1) '&' $2) '&' $3);

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ((( 'not' $1) '&' $2) '&' $3);

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

      :: TWOSCOMP:def11

      func and3b -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def11: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ((( 'not' x) '&' ( 'not' y)) '&' z);

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ((( 'not' $1) '&' ( 'not' $2)) '&' $3);

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ((( 'not' $1) '&' ( 'not' $2)) '&' $3);

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

    end

    ::$Canceled

    definition

      :: TWOSCOMP:def12

      func nand3 -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def12: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ( 'not' ((x '&' y) '&' z));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' (($1 '&' $2) '&' $3));

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' (($1 '&' $2) '&' $3));

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

      :: TWOSCOMP:def13

      func nand3a -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def13: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ( 'not' ((( 'not' x) '&' y) '&' z));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ((( 'not' $1) '&' $2) '&' $3));

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ((( 'not' $1) '&' $2) '&' $3));

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

      :: TWOSCOMP:def14

      func nand3b -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def14: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ( 'not' ((( 'not' x) '&' ( 'not' y)) '&' z));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ((( 'not' $1) '&' ( 'not' $2)) '&' $3));

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ((( 'not' $1) '&' ( 'not' $2)) '&' $3));

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

    end

    

     Lm5: for x,y,z be Element of BOOLEAN holds ( or3 . <*x, y, z*>) = ( 'not' ((( 'not' x) '&' ( 'not' y)) '&' ( 'not' z)))

    proof

      let x,y,z be Element of BOOLEAN ;

      

      thus ( or3 . <*x, y, z*>) = ((x 'or' y) 'or' z) by FACIRC_1:def 7

      .= ( 'not' ((( 'not' x) '&' ( 'not' y)) '&' ( 'not' z)));

    end;

    ::$Canceled

    definition

      :: TWOSCOMP:def15

      func or3a -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def15: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ((( 'not' x) 'or' y) 'or' z);

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ((( 'not' $1) 'or' $2) 'or' $3);

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ((( 'not' $1) 'or' $2) 'or' $3);

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

      :: TWOSCOMP:def16

      func or3b -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def16: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ((( 'not' x) 'or' ( 'not' y)) 'or' z);

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ((( 'not' $1) 'or' ( 'not' $2)) 'or' $3);

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ((( 'not' $1) 'or' ( 'not' $2)) 'or' $3);

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

    end

    

     Lm6: for x,y,z be Element of BOOLEAN holds ( nand3 . <*x, y, z*>) = ((( 'not' x) 'or' ( 'not' y)) 'or' ( 'not' z)) by Def12;

    ::$Canceled

    definition

      :: TWOSCOMP:def17

      func nor3 -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def17: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ( 'not' ((x 'or' y) 'or' z));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' (($1 'or' $2) 'or' $3));

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' (($1 'or' $2) 'or' $3));

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

      :: TWOSCOMP:def18

      func nor3a -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def18: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ( 'not' ((( 'not' x) 'or' y) 'or' z));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ((( 'not' $1) 'or' $2) 'or' $3));

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ((( 'not' $1) 'or' $2) 'or' $3));

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

      :: TWOSCOMP:def19

      func nor3b -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def19: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ( 'not' ((( 'not' x) 'or' ( 'not' y)) 'or' z));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ((( 'not' $1) 'or' ( 'not' $2)) 'or' $3));

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = ( 'not' ((( 'not' $1) 'or' ( 'not' $2)) 'or' $3));

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

    end

    

     Lm7: for x,y,z be Element of BOOLEAN holds ( nor3 . <*x, y, z*>) = ((( 'not' x) '&' ( 'not' y)) '&' ( 'not' z))

    proof

      let x,y,z be Element of BOOLEAN ;

      

      thus ( nor3 . <*x, y, z*>) = ( 'not' ((x 'or' y) 'or' z)) by Def17

      .= ((( 'not' x) '&' ( 'not' y)) '&' ( 'not' z));

    end;

    

     Lm8: for x,y,z be Element of BOOLEAN holds ( and3 . <*x, y, z*>) = ( 'not' ((( 'not' x) 'or' ( 'not' y)) 'or' ( 'not' z))) by Def9;

    ::$Canceled

    definition

      :: TWOSCOMP:def20

      func xor3 -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def20: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ((x 'xor' y) 'xor' z);

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = (($1 'xor' $2) 'xor' $3);

        thus ex t be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st for x,y,z be Element of BOOLEAN holds (t . <*x, y, z*>) = U(x,y,z) from FACIRC_1:sch 4;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = (($1 'xor' $2) 'xor' $3);

        thus for t1,t2 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN st (for x,y,z be Element of BOOLEAN holds (t1 . <*x, y, z*>) = U(x,y,z)) & (for x,y,z be Element of BOOLEAN holds (t2 . <*x, y, z*>) = U(x,y,z)) holds t1 = t2 from FACIRC_1:sch 5;

      end;

    end

    theorem :: TWOSCOMP:12

    for x,y,z be Element of BOOLEAN holds ( and3 . <*x, y, z*>) = ((x '&' y) '&' z) & ( and3a . <*x, y, z*>) = ((( 'not' x) '&' y) '&' z) & ( and3b . <*x, y, z*>) = ((( 'not' x) '&' ( 'not' y)) '&' z) & ( nor3 . <*x, y, z*>) = ((( 'not' x) '&' ( 'not' y)) '&' ( 'not' z)) by Def9, Def10, Def11, Lm7;

    theorem :: TWOSCOMP:13

    for x,y,z be Element of BOOLEAN holds ( nand3 . <*x, y, z*>) = ( 'not' ((x '&' y) '&' z)) & ( nand3a . <*x, y, z*>) = ( 'not' ((( 'not' x) '&' y) '&' z)) & ( nand3b . <*x, y, z*>) = ( 'not' ((( 'not' x) '&' ( 'not' y)) '&' z)) & ( or3 . <*x, y, z*>) = ( 'not' ((( 'not' x) '&' ( 'not' y)) '&' ( 'not' z))) by Def12, Def13, Def14, Lm5;

    theorem :: TWOSCOMP:14

    for x,y,z be Element of BOOLEAN holds ( or3 . <*x, y, z*>) = ((x 'or' y) 'or' z) & ( or3a . <*x, y, z*>) = ((( 'not' x) 'or' y) 'or' z) & ( or3b . <*x, y, z*>) = ((( 'not' x) 'or' ( 'not' y)) 'or' z) & ( nand3 . <*x, y, z*>) = ((( 'not' x) 'or' ( 'not' y)) 'or' ( 'not' z)) by FACIRC_1:def 7, Def15, Def16, Lm6;

    theorem :: TWOSCOMP:15

    for x,y,z be Element of BOOLEAN holds ( nor3 . <*x, y, z*>) = ( 'not' ((x 'or' y) 'or' z)) & ( nor3a . <*x, y, z*>) = ( 'not' ((( 'not' x) 'or' y) 'or' z)) & ( nor3b . <*x, y, z*>) = ( 'not' ((( 'not' x) 'or' ( 'not' y)) 'or' z)) & ( and3 . <*x, y, z*>) = ( 'not' ((( 'not' x) 'or' ( 'not' y)) 'or' ( 'not' z))) by Def17, Def18, Def19, Lm8;

    theorem :: TWOSCOMP:16

    for x,y,z be Element of BOOLEAN holds ( and3a . <*x, y, z*>) = ( nor3b . <*z, y, x*>) & ( and3b . <*x, y, z*>) = ( nor3a . <*z, y, x*>)

    proof

      let x,y,z be Element of BOOLEAN ;

      

      thus ( and3a . <*x, y, z*>) = ( 'not' (( 'not' ( 'not' (( 'not' ( 'not' x)) 'or' ( 'not' y)))) 'or' ( 'not' z))) by Def10

      .= ( 'not' ((( 'not' z) 'or' ( 'not' y)) 'or' x))

      .= ( nor3b . <*z, y, x*>) by Def19;

      

      thus ( and3b . <*x, y, z*>) = ( 'not' (( 'not' ( 'not' (( 'not' ( 'not' x)) 'or' ( 'not' ( 'not' y))))) 'or' ( 'not' z))) by Def11

      .= ( 'not' ((( 'not' z) 'or' y) 'or' x))

      .= ( nor3a . <*z, y, x*>) by Def18;

    end;

    theorem :: TWOSCOMP:17

    for x,y,z be Element of BOOLEAN holds ( or3a . <*x, y, z*>) = ( nand3b . <*z, y, x*>) & ( or3b . <*x, y, z*>) = ( nand3a . <*z, y, x*>)

    proof

      let x,y,z be Element of BOOLEAN ;

      

      thus ( or3a . <*x, y, z*>) = ((( 'not' x) 'or' y) 'or' z) by Def15

      .= ( 'not' ((( 'not' z) '&' ( 'not' y)) '&' x))

      .= ( nand3b . <*z, y, x*>) by Def14;

      

      thus ( or3b . <*x, y, z*>) = ((( 'not' x) 'or' ( 'not' y)) 'or' z) by Def16

      .= ( 'not' ((( 'not' z) '&' y) '&' x))

      .= ( nand3a . <*z, y, x*>) by Def13;

    end;

    theorem :: TWOSCOMP:18

    ( and3 . <* 0 , 0 , 0 *>) = 0 & ( and3 . <* 0 , 0 , 1*>) = 0 & ( and3 . <* 0 , 1, 0 *>) = 0 & ( and3 . <* 0 , 1, 1*>) = 0 & ( and3 . <*1, 0 , 0 *>) = 0 & ( and3 . <*1, 0 , 1*>) = 0 & ( and3 . <*1, 1, 0 *>) = 0 & ( and3 . <*1, 1, 1*>) = 1

    proof

      

      thus ( and3 . <* 0 , 0 , 0 *>) = (( FALSE '&' FALSE ) '&' FALSE ) by Def9

      .= 0 ;

      

      thus ( and3 . <* 0 , 0 , 1*>) = (( FALSE '&' FALSE ) '&' TRUE ) by Def9

      .= 0 ;

      

      thus ( and3 . <* 0 , 1, 0 *>) = (( FALSE '&' TRUE ) '&' FALSE ) by Def9

      .= 0 ;

      

      thus ( and3 . <* 0 , 1, 1*>) = ( FALSE '&' TRUE ) by Def9

      .= 0 ;

      

      thus ( and3 . <*1, 0 , 0 *>) = (( TRUE '&' FALSE ) '&' FALSE ) by Def9

      .= 0 ;

      

      thus ( and3 . <*1, 0 , 1*>) = ( FALSE '&' TRUE ) by Def9

      .= 0 ;

      

      thus ( and3 . <*1, 1, 0 *>) = (( TRUE '&' TRUE ) '&' FALSE ) by Def9

      .= 0 ;

      

      thus ( and3 . <*1, 1, 1*>) = ( TRUE '&' TRUE ) by Def9

      .= 1;

    end;

    theorem :: TWOSCOMP:19

    ( and3a . <* 0 , 0 , 0 *>) = 0 & ( and3a . <* 0 , 0 , 1*>) = 0 & ( and3a . <* 0 , 1, 0 *>) = 0 & ( and3a . <* 0 , 1, 1*>) = 1 & ( and3a . <*1, 0 , 0 *>) = 0 & ( and3a . <*1, 0 , 1*>) = 0 & ( and3a . <*1, 1, 0 *>) = 0 & ( and3a . <*1, 1, 1*>) = 0

    proof

      

      thus ( and3a . <* 0 , 0 , 0 *>) = ((( 'not' FALSE ) '&' FALSE ) '&' FALSE ) by Def10

      .= 0 ;

      

      thus ( and3a . <* 0 , 0 , 1*>) = ((( 'not' FALSE ) '&' FALSE ) '&' TRUE ) by Def10

      .= 0 ;

      

      thus ( and3a . <* 0 , 1, 0 *>) = ((( 'not' FALSE ) '&' TRUE ) '&' FALSE ) by Def10

      .= 0 ;

      

      thus ( and3a . <* 0 , 1, 1*>) = ((( 'not' FALSE ) '&' TRUE ) '&' TRUE ) by Def10

      .= 1;

      

      thus ( and3a . <*1, 0 , 0 *>) = ((( 'not' TRUE ) '&' FALSE ) '&' FALSE ) by Def10

      .= 0 ;

      

      thus ( and3a . <*1, 0 , 1*>) = ((( 'not' TRUE ) '&' FALSE ) '&' TRUE ) by Def10

      .= 0 ;

      

      thus ( and3a . <*1, 1, 0 *>) = ((( 'not' TRUE ) '&' TRUE ) '&' FALSE ) by Def10

      .= 0 ;

      

      thus ( and3a . <*1, 1, 1*>) = (( 'not' TRUE ) '&' TRUE ) by Def10

      .= 0 ;

    end;

    theorem :: TWOSCOMP:20

    ( and3b . <* 0 , 0 , 0 *>) = 0 & ( and3b . <* 0 , 0 , 1*>) = 1 & ( and3b . <* 0 , 1, 0 *>) = 0 & ( and3b . <* 0 , 1, 1*>) = 0 & ( and3b . <*1, 0 , 0 *>) = 0 & ( and3b . <*1, 0 , 1*>) = 0 & ( and3b . <*1, 1, 0 *>) = 0 & ( and3b . <*1, 1, 1*>) = 0

    proof

      

      thus ( and3b . <* 0 , 0 , 0 *>) = ((( 'not' FALSE ) '&' ( 'not' FALSE )) '&' FALSE ) by Def11

      .= 0 ;

      

      thus ( and3b . <* 0 , 0 , 1*>) = (( TRUE '&' ( 'not' FALSE )) '&' TRUE ) by Def11

      .= 1;

      

      thus ( and3b . <* 0 , 1, 0 *>) = ((( 'not' FALSE ) '&' ( 'not' TRUE )) '&' FALSE ) by Def11

      .= 0 ;

      

      thus ( and3b . <* 0 , 1, 1*>) = ((( 'not' FALSE ) '&' ( 'not' TRUE )) '&' TRUE ) by Def11

      .= 0 ;

      

      thus ( and3b . <*1, 0 , 0 *>) = ((( 'not' TRUE ) '&' ( 'not' FALSE )) '&' FALSE ) by Def11

      .= 0 ;

      

      thus ( and3b . <*1, 0 , 1*>) = ((( 'not' TRUE ) '&' ( 'not' FALSE )) '&' TRUE ) by Def11

      .= 0 ;

      

      thus ( and3b . <*1, 1, 0 *>) = ((( 'not' TRUE ) '&' ( 'not' TRUE )) '&' FALSE ) by Def11

      .= 0 ;

      

      thus ( and3b . <*1, 1, 1*>) = (( FALSE '&' ( 'not' TRUE )) '&' TRUE ) by Def11

      .= 0 ;

    end;

    theorem :: TWOSCOMP:21

    ( nor3 . <* 0 , 0 , 0 *>) = 1 & ( nor3 . <* 0 , 0 , 1*>) = 0 & ( nor3 . <* 0 , 1, 0 *>) = 0 & ( nor3 . <* 0 , 1, 1*>) = 0 & ( nor3 . <*1, 0 , 0 *>) = 0 & ( nor3 . <*1, 0 , 1*>) = 0 & ( nor3 . <*1, 1, 0 *>) = 0 & ( nor3 . <*1, 1, 1*>) = 0

    proof

      

      thus ( nor3 . <* 0 , 0 , 0 *>) = (( TRUE '&' ( 'not' FALSE )) '&' ( 'not' FALSE )) by Lm7

      .= 1;

      

      thus ( nor3 . <* 0 , 0 , 1*>) = ((( 'not' FALSE ) '&' ( 'not' FALSE )) '&' ( 'not' TRUE )) by Lm7

      .= 0 ;

      

      thus ( nor3 . <* 0 , 1, 0 *>) = ((( 'not' FALSE ) '&' ( 'not' TRUE )) '&' ( 'not' FALSE )) by Lm7

      .= 0 ;

      

      thus ( nor3 . <* 0 , 1, 1*>) = ((( 'not' FALSE ) '&' ( 'not' TRUE )) '&' FALSE ) by Lm7

      .= 0 ;

      

      thus ( nor3 . <*1, 0 , 0 *>) = ((( 'not' TRUE ) '&' ( 'not' FALSE )) '&' ( 'not' FALSE )) by Lm7

      .= 0 ;

      

      thus ( nor3 . <*1, 0 , 1*>) = ((( 'not' TRUE ) '&' ( 'not' FALSE )) '&' FALSE ) by Lm7

      .= 0 ;

      

      thus ( nor3 . <*1, 1, 0 *>) = (( FALSE '&' ( 'not' TRUE )) '&' ( 'not' FALSE )) by Lm7

      .= 0 ;

      

      thus ( nor3 . <*1, 1, 1*>) = ((( 'not' TRUE ) '&' ( 'not' TRUE )) '&' FALSE ) by Lm7

      .= 0 ;

    end;

    theorem :: TWOSCOMP:22

    ( or3 . <* 0 , 0 , 0 *>) = 0 & ( or3 . <* 0 , 0 , 1*>) = 1 & ( or3 . <* 0 , 1, 0 *>) = 1 & ( or3 . <* 0 , 1, 1*>) = 1 & ( or3 . <*1, 0 , 0 *>) = 1 & ( or3 . <*1, 0 , 1*>) = 1 & ( or3 . <*1, 1, 0 *>) = 1 & ( or3 . <*1, 1, 1*>) = 1

    proof

      

      thus ( or3 . <* 0 , 0 , 0 *>) = ( FALSE 'or' FALSE ) by FACIRC_1:def 7

      .= 0 ;

      

      thus ( or3 . <* 0 , 0 , 1*>) = (( FALSE 'or' FALSE ) 'or' TRUE ) by FACIRC_1:def 7

      .= 1;

      

      thus ( or3 . <* 0 , 1, 0 *>) = ( TRUE 'or' FALSE ) by FACIRC_1:def 7

      .= 1;

      

      thus ( or3 . <* 0 , 1, 1*>) = (( FALSE 'or' TRUE ) 'or' TRUE ) by FACIRC_1:def 7

      .= 1;

      

      thus ( or3 . <*1, 0 , 0 *>) = ( TRUE 'or' FALSE ) by FACIRC_1:def 7

      .= 1;

      

      thus ( or3 . <*1, 0 , 1*>) = (( TRUE 'or' FALSE ) 'or' TRUE ) by FACIRC_1:def 7

      .= 1;

      

      thus ( or3 . <*1, 1, 0 *>) = (( TRUE 'or' TRUE ) 'or' FALSE ) by FACIRC_1:def 7

      .= 1;

      

      thus ( or3 . <*1, 1, 1*>) = (( TRUE 'or' TRUE ) 'or' TRUE ) by FACIRC_1:def 7

      .= 1;

    end;

    theorem :: TWOSCOMP:23

    ( or3a . <* 0 , 0 , 0 *>) = 1 & ( or3a . <* 0 , 0 , 1*>) = 1 & ( or3a . <* 0 , 1, 0 *>) = 1 & ( or3a . <* 0 , 1, 1*>) = 1 & ( or3a . <*1, 0 , 0 *>) = 0 & ( or3a . <*1, 0 , 1*>) = 1 & ( or3a . <*1, 1, 0 *>) = 1 & ( or3a . <*1, 1, 1*>) = 1

    proof

      

      thus ( or3a . <* 0 , 0 , 0 *>) = (( 'not' FALSE ) 'or' FALSE ) by Def15

      .= 1;

      

      thus ( or3a . <* 0 , 0 , 1*>) = ((( 'not' FALSE ) 'or' FALSE ) 'or' TRUE ) by Def15

      .= 1;

      

      thus ( or3a . <* 0 , 1, 0 *>) = ((( 'not' FALSE ) 'or' TRUE ) 'or' FALSE ) by Def15

      .= 1;

      

      thus ( or3a . <* 0 , 1, 1*>) = ((( 'not' FALSE ) 'or' TRUE ) 'or' TRUE ) by Def15

      .= 1;

      

      thus ( or3a . <*1, 0 , 0 *>) = (( 'not' TRUE ) 'or' FALSE ) by Def15

      .= 0 ;

      

      thus ( or3a . <*1, 0 , 1*>) = ((( 'not' TRUE ) 'or' FALSE ) 'or' TRUE ) by Def15

      .= 1;

      

      thus ( or3a . <*1, 1, 0 *>) = ( TRUE 'or' FALSE ) by Def15

      .= 1;

      

      thus ( or3a . <*1, 1, 1*>) = ((( 'not' TRUE ) 'or' TRUE ) 'or' TRUE ) by Def15

      .= 1;

    end;

    theorem :: TWOSCOMP:24

    ( or3b . <* 0 , 0 , 0 *>) = 1 & ( or3b . <* 0 , 0 , 1*>) = 1 & ( or3b . <* 0 , 1, 0 *>) = 1 & ( or3b . <* 0 , 1, 1*>) = 1 & ( or3b . <*1, 0 , 0 *>) = 1 & ( or3b . <*1, 0 , 1*>) = 1 & ( or3b . <*1, 1, 0 *>) = 0 & ( or3b . <*1, 1, 1*>) = 1

    proof

      

      thus ( or3b . <* 0 , 0 , 0 *>) = (( TRUE 'or' ( 'not' FALSE )) 'or' FALSE ) by Def16

      .= 1;

      

      thus ( or3b . <* 0 , 0 , 1*>) = ((( 'not' FALSE ) 'or' ( 'not' FALSE )) 'or' TRUE ) by Def16

      .= 1;

      

      thus ( or3b . <* 0 , 1, 0 *>) = (( 'not' FALSE ) 'or' ( 'not' TRUE )) by Def16

      .= 1;

      

      thus ( or3b . <* 0 , 1, 1*>) = ((( 'not' FALSE ) 'or' ( 'not' TRUE )) 'or' TRUE ) by Def16

      .= 1;

      

      thus ( or3b . <*1, 0 , 0 *>) = (( 'not' TRUE ) 'or' ( 'not' FALSE )) by Def16

      .= 1;

      

      thus ( or3b . <*1, 0 , 1*>) = ((( 'not' TRUE ) 'or' ( 'not' FALSE )) 'or' TRUE ) by Def16

      .= 1;

      

      thus ( or3b . <*1, 1, 0 *>) = (( 'not' TRUE ) 'or' ( 'not' TRUE )) by Def16

      .= 0 ;

      

      thus ( or3b . <*1, 1, 1*>) = ((( 'not' TRUE ) 'or' ( 'not' TRUE )) 'or' TRUE ) by Def16

      .= 1;

    end;

    theorem :: TWOSCOMP:25

    ( nand3 . <* 0 , 0 , 0 *>) = 1 & ( nand3 . <* 0 , 0 , 1*>) = 1 & ( nand3 . <* 0 , 1, 0 *>) = 1 & ( nand3 . <* 0 , 1, 1*>) = 1 & ( nand3 . <*1, 0 , 0 *>) = 1 & ( nand3 . <*1, 0 , 1*>) = 1 & ( nand3 . <*1, 1, 0 *>) = 1 & ( nand3 . <*1, 1, 1*>) = 0

    proof

      

      thus ( nand3 . <* 0 , 0 , 0 *>) = ((( 'not' FALSE ) 'or' ( 'not' FALSE )) 'or' TRUE ) by Lm6

      .= 1;

      

      thus ( nand3 . <* 0 , 0 , 1*>) = ((( 'not' FALSE ) 'or' ( 'not' FALSE )) 'or' FALSE ) by Lm6

      .= 1;

      

      thus ( nand3 . <* 0 , 1, 0 *>) = ((( 'not' FALSE ) 'or' ( 'not' TRUE )) 'or' TRUE ) by Lm6

      .= 1;

      

      thus ( nand3 . <* 0 , 1, 1*>) = (( TRUE 'or' ( 'not' TRUE )) 'or' ( 'not' TRUE )) by Lm6

      .= 1;

      

      thus ( nand3 . <*1, 0 , 0 *>) = ((( 'not' TRUE ) 'or' ( 'not' FALSE )) 'or' TRUE ) by Lm6

      .= 1;

      

      thus ( nand3 . <*1, 0 , 1*>) = ((( 'not' TRUE ) 'or' TRUE ) 'or' ( 'not' TRUE )) by Lm6

      .= 1;

      

      thus ( nand3 . <*1, 1, 0 *>) = ((( 'not' TRUE ) 'or' ( 'not' TRUE )) 'or' TRUE ) by Lm6

      .= 1;

      

      thus ( nand3 . <*1, 1, 1*>) = (( FALSE 'or' ( 'not' TRUE )) 'or' ( 'not' TRUE )) by Lm6

      .= 0 ;

    end;

    theorem :: TWOSCOMP:26

    ( xor3 . <* 0 , 0 , 0 *>) = 0 & ( xor3 . <* 0 , 0 , 1*>) = 1 & ( xor3 . <* 0 , 1, 0 *>) = 1 & ( xor3 . <* 0 , 1, 1*>) = 0 & ( xor3 . <*1, 0 , 0 *>) = 1 & ( xor3 . <*1, 0 , 1*>) = 0 & ( xor3 . <*1, 1, 0 *>) = 0 & ( xor3 . <*1, 1, 1*>) = 1

    proof

      

      thus ( xor3 . <* 0 , 0 , 0 *>) = ( FALSE 'xor' FALSE ) by Def20

      .= 0 ;

      

      thus ( xor3 . <* 0 , 0 , 1*>) = (( FALSE 'xor' FALSE ) 'xor' TRUE ) by Def20

      .= 1;

      thus ( xor3 . <* 0 , 1, 0 *>) = 1 by Def20, BINARITH: 13;

      

      thus ( xor3 . <* 0 , 1, 1*>) = ( TRUE 'xor' TRUE ) by Def20, BINARITH: 13

      .= 0 ;

      thus ( xor3 . <*1, 0 , 0 *>) = 1 by Def20, BINARITH: 13;

      

      thus ( xor3 . <*1, 0 , 1*>) = ( TRUE 'xor' TRUE ) by Def20, BINARITH: 13

      .= 0 ;

      

      thus ( xor3 . <*1, 1, 0 *>) = (( TRUE 'xor' TRUE ) 'xor' FALSE ) by Def20

      .= 0 ;

      

      thus ( xor3 . <*1, 1, 1*>) = (( TRUE 'xor' TRUE ) 'xor' TRUE ) by Def20

      .= 1;

    end;

    begin

    definition

      let x,b be set;

      :: TWOSCOMP:def21

      func CompStr (x,b) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ( 1GateCircStr ( <*x, b*>, xor2a ));

      correctness ;

    end

    definition

      let x,b be set;

      :: TWOSCOMP:def22

      func CompCirc (x,b) -> strict Boolean gate`2=den Circuit of ( CompStr (x,b)) equals ( 1GateCircuit (x,b, xor2a ));

      coherence ;

    end

    definition

      let x,b be set;

      :: TWOSCOMP:def23

      func CompOutput (x,b) -> Element of ( InnerVertices ( CompStr (x,b))) equals [ <*x, b*>, xor2a ];

      coherence by FACIRC_1: 47;

    end

    definition

      let x,b be set;

      :: TWOSCOMP:def24

      func IncrementStr (x,b) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ( 1GateCircStr ( <*x, b*>, and2a ));

      correctness ;

    end

    definition

      let x,b be set;

      :: TWOSCOMP:def25

      func IncrementCirc (x,b) -> strict Boolean gate`2=den Circuit of ( IncrementStr (x,b)) equals ( 1GateCircuit (x,b, and2a ));

      coherence ;

    end

    definition

      let x,b be set;

      :: TWOSCOMP:def26

      func IncrementOutput (x,b) -> Element of ( InnerVertices ( IncrementStr (x,b))) equals [ <*x, b*>, and2a ];

      coherence by FACIRC_1: 47;

    end

    definition

      let x,b be set;

      :: TWOSCOMP:def27

      func BitCompStr (x,b) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( CompStr (x,b)) +* ( IncrementStr (x,b)));

      correctness ;

    end

    definition

      let x,b be set;

      :: TWOSCOMP:def28

      func BitCompCirc (x,b) -> strict Boolean gate`2=den Circuit of ( BitCompStr (x,b)) equals (( CompCirc (x,b)) +* ( IncrementCirc (x,b)));

      coherence ;

    end

    theorem :: TWOSCOMP:27

    

     Th27: for x,b be non pair set holds the carrier of ( CompStr (x,b)) = ( {x, b} \/ { [ <*x, b*>, xor2a ]})

    proof

      let x,b be non pair set;

      set p = <*x, b*>;

      ( rng p) = {x, b} by FINSEQ_2: 127;

      hence thesis by CIRCCOMB:def 6;

    end;

    theorem :: TWOSCOMP:28

    for x,b be non pair set holds [ <*x, b*>, xor2a ] in ( InnerVertices ( CompStr (x,b)))

    proof

      let x,b be non pair set;

      ( InnerVertices ( CompStr (x,b))) = { [ <*x, b*>, xor2a ]} by CIRCCOMB: 42;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: TWOSCOMP:29

    for x,b be non pair set holds x in ( InputVertices ( CompStr (x,b))) & b in ( InputVertices ( CompStr (x,b)))

    proof

      let x,b be non pair set;

      ( InputVertices ( CompStr (x,b))) = {x, b} by FACIRC_1: 40;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: TWOSCOMP:30

    for x,b be non pair set holds ( InputVertices ( CompStr (x,b))) is without_pairs

    proof

      let x,b be non pair set;

      ( InputVertices ( CompStr (x,b))) = {x, b} by FACIRC_1: 40;

      hence thesis;

    end;

    theorem :: TWOSCOMP:31

    

     Th31: for x,b be non pair set holds the carrier of ( IncrementStr (x,b)) = ( {x, b} \/ { [ <*x, b*>, and2a ]})

    proof

      let x,b be non pair set;

      set p = <*x, b*>;

      ( rng p) = {x, b} by FINSEQ_2: 127;

      hence thesis by CIRCCOMB:def 6;

    end;

    theorem :: TWOSCOMP:32

    for x,b be non pair set holds [ <*x, b*>, and2a ] in ( InnerVertices ( IncrementStr (x,b)))

    proof

      let x,b be non pair set;

      ( InnerVertices ( IncrementStr (x,b))) = { [ <*x, b*>, and2a ]} by CIRCCOMB: 42;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: TWOSCOMP:33

    for x,b be non pair set holds x in ( InputVertices ( IncrementStr (x,b))) & b in ( InputVertices ( IncrementStr (x,b)))

    proof

      let x,b be non pair set;

      ( InputVertices ( IncrementStr (x,b))) = {x, b} by FACIRC_1: 40;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: TWOSCOMP:34

    for x,b be non pair set holds ( InputVertices ( IncrementStr (x,b))) is without_pairs

    proof

      let x,b be non pair set;

      ( InputVertices ( IncrementStr (x,b))) = {x, b} by FACIRC_1: 40;

      hence thesis;

    end;

    theorem :: TWOSCOMP:35

    for x,b be non pair set holds ( InnerVertices ( BitCompStr (x,b))) is Relation

    proof

      let x,b be non pair set;

      set S1 = ( CompStr (x,b));

      set S2 = ( IncrementStr (x,b));

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by FACIRC_1: 38;

      hence thesis by FACIRC_1: 3;

    end;

    theorem :: TWOSCOMP:36

    

     Th36: for x,b be non pair set holds x in the carrier of ( BitCompStr (x,b)) & b in the carrier of ( BitCompStr (x,b)) & [ <*x, b*>, xor2a ] in the carrier of ( BitCompStr (x,b)) & [ <*x, b*>, and2a ] in the carrier of ( BitCompStr (x,b))

    proof

      let x,b be non pair set;

      set p = <*x, b*>;

      set S1 = ( CompStr (x,b));

      set S2 = ( IncrementStr (x,b));

      

       A1: [p, xor2a ] in the carrier of S1 & [p, and2a ] in the carrier of S2 by FACIRC_1: 43;

      x in the carrier of S1 & b in the carrier of S1 by FACIRC_1: 43;

      hence thesis by A1, FACIRC_1: 20;

    end;

    theorem :: TWOSCOMP:37

    

     Th37: for x,b be non pair set holds the carrier of ( BitCompStr (x,b)) = ( {x, b} \/ { [ <*x, b*>, xor2a ], [ <*x, b*>, and2a ]})

    proof

      let x,b be non pair set;

      set p = <*x, b*>;

      set S1 = ( CompStr (x,b));

      set S2 = ( IncrementStr (x,b));

      the carrier of S1 = ( {x, b} \/ { [p, xor2a ]}) & the carrier of S2 = ( {x, b} \/ { [p, and2a ]}) by Th27, Th31;

      

      then the carrier of ( BitCompStr (x,b)) = (( {x, b} \/ { [p, xor2a ]}) \/ ( {x, b} \/ { [p, and2a ]})) by CIRCCOMB:def 2

      .= (( {x, b} \/ ( {x, b} \/ { [p, xor2a ]})) \/ { [p, and2a ]}) by XBOOLE_1: 4

      .= ((( {x, b} \/ {x, b}) \/ { [p, xor2a ]}) \/ { [p, and2a ]}) by XBOOLE_1: 4

      .= ( {x, b} \/ ( { [p, xor2a ]} \/ { [p, and2a ]})) by XBOOLE_1: 4

      .= ( {x, b} \/ { [p, xor2a ], [p, and2a ]}) by ENUMSET1: 1;

      hence thesis;

    end;

    theorem :: TWOSCOMP:38

    

     Th38: for x,b be non pair set holds ( InnerVertices ( BitCompStr (x,b))) = { [ <*x, b*>, xor2a ], [ <*x, b*>, and2a ]}

    proof

      let x,b be non pair set;

      set p = <*x, b*>;

      set S1 = ( CompStr (x,b));

      set S2 = ( IncrementStr (x,b));

      set S = ( BitCompStr (x,b));

      

       A1: ( InnerVertices S1) = { [p, xor2a ]} & ( InnerVertices S2) = { [p, and2a ]} by CIRCCOMB: 42;

      ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by FACIRC_1: 27

      .= { [p, xor2a ], [p, and2a ]} by A1, ENUMSET1: 1;

      hence thesis;

    end;

    theorem :: TWOSCOMP:39

    

     Th39: for x,b be non pair set holds [ <*x, b*>, xor2a ] in ( InnerVertices ( BitCompStr (x,b))) & [ <*x, b*>, and2a ] in ( InnerVertices ( BitCompStr (x,b)))

    proof

      let x,b be non pair set;

      ( InnerVertices ( BitCompStr (x,b))) = { [ <*x, b*>, xor2a ], [ <*x, b*>, and2a ]} by Th38;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: TWOSCOMP:40

    

     Th40: for x,b be non pair set holds ( InputVertices ( BitCompStr (x,b))) = {x, b}

    proof

      let x,b be non pair set;

      set S1 = ( CompStr (x,b));

      set S2 = ( IncrementStr (x,b));

      set S = ( BitCompStr (x,b));

      

       A1: ( InputVertices S1) = {x, b} & ( InputVertices S2) = {x, b} by FACIRC_1: 40;

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by FACIRC_1: 38;

      

      then ( InputVertices S) = ( {x, b} \/ {x, b}) by A1, FACIRC_1: 7

      .= {x, b};

      hence thesis;

    end;

    theorem :: TWOSCOMP:41

    

     Th41: for x,b be non pair set holds x in ( InputVertices ( BitCompStr (x,b))) & b in ( InputVertices ( BitCompStr (x,b)))

    proof

      let x,b be non pair set;

      ( InputVertices ( BitCompStr (x,b))) = {x, b} by Th40;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: TWOSCOMP:42

    for x,b be non pair set holds ( InputVertices ( BitCompStr (x,b))) is without_pairs

    proof

      let x,b be non pair set;

      ( InputVertices ( BitCompStr (x,b))) = {x, b} by Th40;

      hence thesis;

    end;

    theorem :: TWOSCOMP:43

    

     Th43: for x,b be non pair set holds for s be State of ( CompCirc (x,b)) holds (( Following s) . ( CompOutput (x,b))) = ( xor2a . <*(s . x), (s . b)*>) & (( Following s) . x) = (s . x) & (( Following s) . b) = (s . b)

    proof

      let x,b be non pair set;

      let s be State of ( CompCirc (x,b));

      set p = <*x, b*>;

      set S = ( CompStr (x,b));

      

       A1: ( dom s) = the carrier of S & x in the carrier of S by CIRCUIT1: 3, FACIRC_1: 43;

      

       A2: b in the carrier of S by FACIRC_1: 43;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      

      hence (( Following s) . ( CompOutput (x,b))) = ( xor2a . (s * p)) by FACIRC_1: 35

      .= ( xor2a . <*(s . x), (s . b)*>) by A1, A2, FINSEQ_2: 125;

      ( InputVertices S) = {x, b} by FACIRC_1: 40;

      then x in ( InputVertices S) & b in ( InputVertices S) by TARSKI:def 2;

      hence thesis by CIRCUIT2:def 5;

    end;

    theorem :: TWOSCOMP:44

    for x,b be non pair set holds for s be State of ( CompCirc (x,b)) holds for a1,a2 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . b) holds (( Following s) . ( CompOutput (x,b))) = (( 'not' a1) 'xor' a2) & (( Following s) . x) = a1 & (( Following s) . b) = a2

    proof

      let x,b be non pair set;

      let s be State of ( CompCirc (x,b));

      let a1,a2 be Element of BOOLEAN ;

      assume

       A1: a1 = (s . x) & a2 = (s . b);

      

      thus (( Following s) . ( CompOutput (x,b))) = ( xor2a . <*(s . x), (s . b)*>) by Th43

      .= (( 'not' a1) 'xor' a2) by A1, Def7;

      thus thesis by A1, Th43;

    end;

    theorem :: TWOSCOMP:45

    

     Th45: for x,b be non pair set holds for s be State of ( BitCompCirc (x,b)) holds (( Following s) . ( CompOutput (x,b))) = ( xor2a . <*(s . x), (s . b)*>) & (( Following s) . x) = (s . x) & (( Following s) . b) = (s . b)

    proof

      let x,b be non pair set;

      let s be State of ( BitCompCirc (x,b));

      set p = <*x, b*>;

      set S = ( BitCompStr (x,b));

      

       A1: ( dom s) = the carrier of S & x in the carrier of S by Th36, CIRCUIT1: 3;

      

       A2: b in the carrier of S by Th36;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      

      hence (( Following s) . ( CompOutput (x,b))) = ( xor2a . (s * p)) by Th39, FACIRC_1: 35

      .= ( xor2a . <*(s . x), (s . b)*>) by A1, A2, FINSEQ_2: 125;

      x in ( InputVertices S) & b in ( InputVertices S) by Th41;

      hence thesis by CIRCUIT2:def 5;

    end;

    theorem :: TWOSCOMP:46

    

     Th46: for x,b be non pair set holds for s be State of ( BitCompCirc (x,b)) holds for a1,a2 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . b) holds (( Following s) . ( CompOutput (x,b))) = (( 'not' a1) 'xor' a2) & (( Following s) . x) = a1 & (( Following s) . b) = a2

    proof

      let x,b be non pair set;

      let s be State of ( BitCompCirc (x,b));

      let a1,a2 be Element of BOOLEAN ;

      assume

       A1: a1 = (s . x) & a2 = (s . b);

      

      thus (( Following s) . ( CompOutput (x,b))) = ( xor2a . <*(s . x), (s . b)*>) by Th45

      .= (( 'not' a1) 'xor' a2) by A1, Def7;

      thus thesis by A1, Th45;

    end;

    theorem :: TWOSCOMP:47

    

     Th47: for x,b be non pair set holds for s be State of ( IncrementCirc (x,b)) holds (( Following s) . ( IncrementOutput (x,b))) = ( and2a . <*(s . x), (s . b)*>) & (( Following s) . x) = (s . x) & (( Following s) . b) = (s . b)

    proof

      let x,b be non pair set;

      let s be State of ( IncrementCirc (x,b));

      set p = <*x, b*>;

      set S = ( IncrementStr (x,b));

      

       A1: ( dom s) = the carrier of S & x in the carrier of S by CIRCUIT1: 3, FACIRC_1: 43;

      

       A2: b in the carrier of S by FACIRC_1: 43;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      

      hence (( Following s) . ( IncrementOutput (x,b))) = ( and2a . (s * p)) by FACIRC_1: 35

      .= ( and2a . <*(s . x), (s . b)*>) by A1, A2, FINSEQ_2: 125;

      ( InputVertices S) = {x, b} by FACIRC_1: 40;

      then x in ( InputVertices S) & b in ( InputVertices S) by TARSKI:def 2;

      hence thesis by CIRCUIT2:def 5;

    end;

    theorem :: TWOSCOMP:48

    for x,b be non pair set holds for s be State of ( IncrementCirc (x,b)) holds for a1,a2 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . b) holds (( Following s) . ( IncrementOutput (x,b))) = (( 'not' a1) '&' a2) & (( Following s) . x) = a1 & (( Following s) . b) = a2

    proof

      let x,b be non pair set;

      let s be State of ( IncrementCirc (x,b));

      let a1,a2 be Element of BOOLEAN ;

      assume

       A1: a1 = (s . x) & a2 = (s . b);

      

      thus (( Following s) . ( IncrementOutput (x,b))) = ( and2a . <*(s . x), (s . b)*>) by Th47

      .= (( 'not' a1) '&' a2) by A1, Def1;

      thus thesis by A1, Th47;

    end;

    theorem :: TWOSCOMP:49

    

     Th49: for x,b be non pair set holds for s be State of ( BitCompCirc (x,b)) holds (( Following s) . ( IncrementOutput (x,b))) = ( and2a . <*(s . x), (s . b)*>) & (( Following s) . x) = (s . x) & (( Following s) . b) = (s . b)

    proof

      let x,b be non pair set;

      let s be State of ( BitCompCirc (x,b));

      set p = <*x, b*>;

      set S = ( BitCompStr (x,b));

      

       A1: ( dom s) = the carrier of S & x in the carrier of S by Th36, CIRCUIT1: 3;

      

       A2: b in the carrier of S by Th36;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      

      hence (( Following s) . ( IncrementOutput (x,b))) = ( and2a . (s * p)) by Th39, FACIRC_1: 35

      .= ( and2a . <*(s . x), (s . b)*>) by A1, A2, FINSEQ_2: 125;

      ( InputVertices S) = {x, b} by Th40;

      then x in ( InputVertices S) & b in ( InputVertices S) by TARSKI:def 2;

      hence thesis by CIRCUIT2:def 5;

    end;

    theorem :: TWOSCOMP:50

    

     Th50: for x,b be non pair set holds for s be State of ( BitCompCirc (x,b)) holds for a1,a2 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . b) holds (( Following s) . ( IncrementOutput (x,b))) = (( 'not' a1) '&' a2) & (( Following s) . x) = a1 & (( Following s) . b) = a2

    proof

      let x,b be non pair set;

      let s be State of ( BitCompCirc (x,b));

      let a1,a2 be Element of BOOLEAN ;

      assume

       A1: a1 = (s . x) & a2 = (s . b);

      

      thus (( Following s) . ( IncrementOutput (x,b))) = ( and2a . <*(s . x), (s . b)*>) by Th49

      .= (( 'not' a1) '&' a2) by A1, Def1;

      thus thesis by A1, Th49;

    end;

    theorem :: TWOSCOMP:51

    for x,b be non pair set holds for s be State of ( BitCompCirc (x,b)) holds (( Following s) . ( CompOutput (x,b))) = ( xor2a . <*(s . x), (s . b)*>) & (( Following s) . ( IncrementOutput (x,b))) = ( and2a . <*(s . x), (s . b)*>) & (( Following s) . x) = (s . x) & (( Following s) . b) = (s . b) by Th45, Th49;

    theorem :: TWOSCOMP:52

    for x,b be non pair set holds for s be State of ( BitCompCirc (x,b)) holds for a1,a2 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . b) holds (( Following s) . ( CompOutput (x,b))) = (( 'not' a1) 'xor' a2) & (( Following s) . ( IncrementOutput (x,b))) = (( 'not' a1) '&' a2) & (( Following s) . x) = a1 & (( Following s) . b) = a2 by Th46, Th50;

    theorem :: TWOSCOMP:53

    for x,b be non pair set holds for s be State of ( BitCompCirc (x,b)) holds ( Following s) is stable

    proof

      let x,b be non pair set;

      set p = <*x, b*>;

      set S = ( BitCompStr (x,b));

      let s be State of ( BitCompCirc (x,b));

      set s1 = ( Following s), s2 = ( Following s1);

      

       A1: the carrier of S = ( {x, b} \/ { [p, xor2a ], [p, and2a ]}) by Th37;

       A2:

      now

        let a be object;

        

         A3: (s1 . [p, xor2a ]) = (s1 . ( CompOutput (x,b)))

        .= ( xor2a . <*(s . x), (s . b)*>) by Th45;

        assume a in the carrier of S;

        then a in {x, b} or a in { [p, xor2a ], [p, and2a ]} by A1, XBOOLE_0:def 3;

        then

         A4: a = x or a = b or a = [p, xor2a ] or a = [p, and2a ] by TARSKI:def 2;

        

         A5: (s2 . [p, and2a ]) = (s2 . ( IncrementOutput (x,b)))

        .= ( and2a . <*(s1 . x), (s1 . b)*>) by Th49;

        

         A6: (s2 . [p, xor2a ]) = (s2 . ( CompOutput (x,b)))

        .= ( xor2a . <*(s1 . x), (s1 . b)*>) by Th45;

        

         A7: (s1 . [p, and2a ]) = (s1 . ( IncrementOutput (x,b)))

        .= ( and2a . <*(s . x), (s . b)*>) by Th49;

        (s1 . x) = (s . x) by Th45;

        hence (s2 . a) = (s1 . a) by A4, A3, A7, A6, A5, Th45;

      end;

      ( dom s1) = the carrier of S & ( dom s2) = the carrier of S by CIRCUIT1: 3;

      hence ( Following s) = ( Following ( Following s)) by A2, FUNCT_1: 2;

    end;

    theorem :: TWOSCOMP:54

    for x,y be Element of BOOLEAN holds ( nor2 . <*x, y*>) = (( 'not' x) '&' ( 'not' y)) by Lm3;

    theorem :: TWOSCOMP:55

    for x,y be Element of BOOLEAN holds ( or2 . <*x, y*>) = ( 'not' (( 'not' x) '&' ( 'not' y))) by Lm1;

    theorem :: TWOSCOMP:56

    for x,y be Element of BOOLEAN holds ( and2 . <*x, y*>) = ( 'not' (( 'not' x) 'or' ( 'not' y))) by Lm4;

    theorem :: TWOSCOMP:57

    for x,y be Element of BOOLEAN holds ( nand2 . <*x, y*>) = (( 'not' x) 'or' ( 'not' y)) by Lm2;

    theorem :: TWOSCOMP:58

    for x,y,z be Element of BOOLEAN holds ( nor3 . <*x, y, z*>) = ((( 'not' x) '&' ( 'not' y)) '&' ( 'not' z)) by Lm7;

    theorem :: TWOSCOMP:59

    for x,y,z be Element of BOOLEAN holds ( or3 . <*x, y, z*>) = ( 'not' ((( 'not' x) '&' ( 'not' y)) '&' ( 'not' z))) by Lm5;

    theorem :: TWOSCOMP:60

    for x,y,z be Element of BOOLEAN holds ( nand3 . <*x, y, z*>) = ((( 'not' x) 'or' ( 'not' y)) 'or' ( 'not' z)) by Lm6;

    theorem :: TWOSCOMP:61

    for x,y,z be Element of BOOLEAN holds ( and3 . <*x, y, z*>) = ( 'not' ((( 'not' x) 'or' ( 'not' y)) 'or' ( 'not' z))) by Lm8;