:: 2's Complement Circuit. Part I. Boolean Operators and 2's Complement Circuit Properties :: by Katsumi Wasaki and Pauline N. Kawamoto :: :: Received October 25, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin ::--------------------------------------------------------------------------- :: Preliminaries ::--------------------------------------------------------------------------- definition let S be non empty non void unsplit ManySortedSign ; let A be Boolean Circuit of S; let s be State of A; let v be Vertex of S; :: original:. redefine funcs . v -> Element of BOOLEAN ; coherence s . v is Element of BOOLEAN proofend; end; deffunc H1( Element of BOOLEAN , Element of BOOLEAN ) -> Element of BOOLEAN = $1 '&' $2; definition func and2 -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def1: :: TWOSCOMP:def 1 for x, y being Element of BOOLEAN holds it . <*x,y*> = x '&' y; existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' y ) holds b1 = b2 proofend; func and2a -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def2: :: TWOSCOMP:def 2 for x, y being Element of BOOLEAN holds it . <*x,y*> = ('not' x) '&' y; existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) '&' y proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) '&' y ) holds b1 = b2 proofend; func and2b -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def3: :: TWOSCOMP:def 3 for x, y being Element of BOOLEAN holds it . <*x,y*> = ('not' x) '&' ('not' y); existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) '&' ('not' y) proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) '&' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) '&' ('not' y) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines and2 TWOSCOMP:def_1_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = and2 iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y ); :: deftheorem Def2 defines and2a TWOSCOMP:def_2_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = and2a iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) '&' y ); :: deftheorem Def3 defines and2b TWOSCOMP:def_3_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = and2b iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) '&' ('not' y) ); definition func nand2 -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def4: :: TWOSCOMP:def 4 for x, y being Element of BOOLEAN holds it . <*x,y*> = 'not' (x '&' y); existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (x '&' y) proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (x '&' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (x '&' y) ) holds b1 = b2 proofend; func nand2a -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def5: :: TWOSCOMP:def 5 for x, y being Element of BOOLEAN holds it . <*x,y*> = 'not' (('not' x) '&' y); existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) '&' y) proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) '&' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (('not' x) '&' y) ) holds b1 = b2 proofend; func nand2b -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def6: :: TWOSCOMP:def 6 for x, y being Element of BOOLEAN holds it . <*x,y*> = 'not' (('not' x) '&' ('not' y)); existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) '&' ('not' y)) proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) '&' ('not' y)) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (('not' x) '&' ('not' y)) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines nand2 TWOSCOMP:def_4_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nand2 iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (x '&' y) ); :: deftheorem Def5 defines nand2a TWOSCOMP:def_5_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nand2a iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) '&' y) ); :: deftheorem Def6 defines nand2b TWOSCOMP:def_6_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nand2b iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) '&' ('not' y)) ); definition func or2 -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def7: :: TWOSCOMP:def 7 for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'or' y; existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'or' y ) holds b1 = b2 proofend; func or2a -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def8: :: TWOSCOMP:def 8 for x, y being Element of BOOLEAN holds it . <*x,y*> = ('not' x) 'or' y; existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'or' y proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'or' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) 'or' y ) holds b1 = b2 proofend; func or2b -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def9: :: TWOSCOMP:def 9 for x, y being Element of BOOLEAN holds it . <*x,y*> = ('not' x) 'or' ('not' y); existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'or' ('not' y) proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'or' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) 'or' ('not' y) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines or2 TWOSCOMP:def_7_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = or2 iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y ); :: deftheorem Def8 defines or2a TWOSCOMP:def_8_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = or2a iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'or' y ); :: deftheorem Def9 defines or2b TWOSCOMP:def_9_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = or2b iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'or' ('not' y) ); definition func nor2 -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def10: :: TWOSCOMP:def 10 for x, y being Element of BOOLEAN holds it . <*x,y*> = 'not' (x 'or' y); existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (x 'or' y) proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (x 'or' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (x 'or' y) ) holds b1 = b2 proofend; func nor2a -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def11: :: TWOSCOMP:def 11 for x, y being Element of BOOLEAN holds it . <*x,y*> = 'not' (('not' x) 'or' y); existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) 'or' y) proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) 'or' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (('not' x) 'or' y) ) holds b1 = b2 proofend; func nor2b -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def12: :: TWOSCOMP:def 12 for x, y being Element of BOOLEAN holds it . <*x,y*> = 'not' (('not' x) 'or' ('not' y)); existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines nor2 TWOSCOMP:def_10_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nor2 iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (x 'or' y) ); :: deftheorem Def11 defines nor2a TWOSCOMP:def_11_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nor2a iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) 'or' y) ); :: deftheorem Def12 defines nor2b TWOSCOMP:def_12_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nor2b iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) ); definition func xor2 -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def13: :: TWOSCOMP:def 13 for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'xor' y; existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'xor' y ) holds b1 = b2 proofend; func xor2a -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def14: :: TWOSCOMP:def 14 for x, y being Element of BOOLEAN holds it . <*x,y*> = ('not' x) 'xor' y; existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'xor' y proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'xor' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) 'xor' y ) holds b1 = b2 proofend; func xor2b -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def15: :: TWOSCOMP:def 15 for x, y being Element of BOOLEAN holds it . <*x,y*> = ('not' x) 'xor' ('not' y); existence ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'xor' ('not' y) proofend; uniqueness for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'xor' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) 'xor' ('not' y) ) holds b1 = b2 proofend; end; :: deftheorem Def13 defines xor2 TWOSCOMP:def_13_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = xor2 iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y ); :: deftheorem Def14 defines xor2a TWOSCOMP:def_14_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = xor2a iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'xor' y ); :: deftheorem Def15 defines xor2b TWOSCOMP:def_15_:_ for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = xor2b iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = ('not' x) 'xor' ('not' y) ); theorem :: TWOSCOMP:1 for x, y being Element of BOOLEAN holds ( and2 . <*x,y*> = x '&' y & and2a . <*x,y*> = ('not' x) '&' y & and2b . <*x,y*> = ('not' x) '&' ('not' y) ) by Def1, Def2, Def3; theorem :: TWOSCOMP:2 for x, y being Element of BOOLEAN holds ( nand2 . <*x,y*> = 'not' (x '&' y) & nand2a . <*x,y*> = 'not' (('not' x) '&' y) & nand2b . <*x,y*> = 'not' (('not' x) '&' ('not' y)) ) by Def4, Def5, Def6; theorem :: TWOSCOMP:3 for x, y being Element of BOOLEAN holds ( or2 . <*x,y*> = x 'or' y & or2a . <*x,y*> = ('not' x) 'or' y & or2b . <*x,y*> = ('not' x) 'or' ('not' y) ) by Def7, Def8, Def9; theorem :: TWOSCOMP:4 for x, y being Element of BOOLEAN holds ( nor2 . <*x,y*> = 'not' (x 'or' y) & nor2a . <*x,y*> = 'not' (('not' x) 'or' y) & nor2b . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) ) by Def10, Def11, Def12; theorem :: TWOSCOMP:5 for x, y being 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 Def13, Def14, Def15; theorem :: TWOSCOMP:6 for x, y being Element of BOOLEAN holds ( and2 . <*x,y*> = nor2b . <*x,y*> & and2a . <*x,y*> = nor2a . <*y,x*> & and2b . <*x,y*> = nor2 . <*x,y*> ) proofend; theorem :: TWOSCOMP:7 for x, y being Element of BOOLEAN holds ( or2 . <*x,y*> = nand2b . <*x,y*> & or2a . <*x,y*> = nand2a . <*y,x*> & or2b . <*x,y*> = nand2 . <*x,y*> ) proofend; theorem :: TWOSCOMP:8 for x, y being Element of BOOLEAN holds xor2b . <*x,y*> = xor2 . <*x,y*> proofend; 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 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 ) proofend; 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 & or2b . <*0,0*> = 1 & or2b . <*0,1*> = 1 & or2b . <*1,0*> = 1 & or2b . <*1,1*> = 0 ) proofend; 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 ) proofend; :: 3-Input Operators definition func and3 -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def16: :: TWOSCOMP:def 16 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (x '&' y) '&' z; existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x '&' y) '&' z proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x '&' y) '&' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x '&' y) '&' z ) holds b1 = b2 proofend; func and3a -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def17: :: TWOSCOMP:def 17 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (('not' x) '&' y) '&' z; existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' y) '&' z proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' y) '&' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) '&' y) '&' z ) holds b1 = b2 proofend; func and3b -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def18: :: TWOSCOMP:def 18 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' z; existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' z proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' z ) holds b1 = b2 proofend; func and3c -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def19: :: TWOSCOMP:def 19 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z); existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) ) holds b1 = b2 proofend; end; :: deftheorem Def16 defines and3 TWOSCOMP:def_16_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = and3 iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x '&' y) '&' z ); :: deftheorem Def17 defines and3a TWOSCOMP:def_17_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = and3a iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' y) '&' z ); :: deftheorem Def18 defines and3b TWOSCOMP:def_18_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = and3b iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' z ); :: deftheorem Def19 defines and3c TWOSCOMP:def_19_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = and3c iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) ); definition func nand3 -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def20: :: TWOSCOMP:def 20 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = 'not' ((x '&' y) '&' z); existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((x '&' y) '&' z) proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((x '&' y) '&' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((x '&' y) '&' z) ) holds b1 = b2 proofend; func nand3a -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def21: :: TWOSCOMP:def 21 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = 'not' ((('not' x) '&' y) '&' z); existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' y) '&' z) proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' y) '&' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) '&' y) '&' z) ) holds b1 = b2 proofend; func nand3b -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def22: :: TWOSCOMP:def 22 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z); existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z) proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z) ) holds b1 = b2 proofend; func nand3c -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def23: :: TWOSCOMP:def 23 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)); existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) ) holds b1 = b2 proofend; end; :: deftheorem Def20 defines nand3 TWOSCOMP:def_20_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nand3 iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((x '&' y) '&' z) ); :: deftheorem Def21 defines nand3a TWOSCOMP:def_21_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nand3a iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' y) '&' z) ); :: deftheorem Def22 defines nand3b TWOSCOMP:def_22_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nand3b iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' z) ); :: deftheorem Def23 defines nand3c TWOSCOMP:def_23_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nand3c iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) ); definition func or3 -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def24: :: TWOSCOMP:def 24 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (x 'or' y) 'or' z; existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x 'or' y) 'or' z ) holds b1 = b2 proofend; func or3a -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def25: :: TWOSCOMP:def 25 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (('not' x) 'or' y) 'or' z; existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' y) 'or' z proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) 'or' y) 'or' z ) holds b1 = b2 proofend; func or3b -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def26: :: TWOSCOMP:def 26 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z; existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z ) holds b1 = b2 proofend; func or3c -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def27: :: TWOSCOMP:def 27 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z); existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) ) holds b1 = b2 proofend; end; :: deftheorem Def24 defines or3 TWOSCOMP:def_24_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = or3 iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z ); :: deftheorem Def25 defines or3a TWOSCOMP:def_25_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = or3a iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' y) 'or' z ); :: deftheorem Def26 defines or3b TWOSCOMP:def_26_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = or3b iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z ); :: deftheorem Def27 defines or3c TWOSCOMP:def_27_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = or3c iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) ); definition func nor3 -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def28: :: TWOSCOMP:def 28 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = 'not' ((x 'or' y) 'or' z); existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((x 'or' y) 'or' z) proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((x 'or' y) 'or' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((x 'or' y) 'or' z) ) holds b1 = b2 proofend; func nor3a -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def29: :: TWOSCOMP:def 29 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = 'not' ((('not' x) 'or' y) 'or' z); existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' y) 'or' z) proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' y) 'or' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) 'or' y) 'or' z) ) holds b1 = b2 proofend; func nor3b -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def30: :: TWOSCOMP:def 30 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' z); existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' z) proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' z) ) holds b1 = b2 proofend; func nor3c -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def31: :: TWOSCOMP:def 31 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)); existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)) proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)) ) holds b1 = b2 proofend; end; :: deftheorem Def28 defines nor3 TWOSCOMP:def_28_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nor3 iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((x 'or' y) 'or' z) ); :: deftheorem Def29 defines nor3a TWOSCOMP:def_29_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nor3a iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' y) 'or' z) ); :: deftheorem Def30 defines nor3b TWOSCOMP:def_30_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nor3b iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' z) ); :: deftheorem Def31 defines nor3c TWOSCOMP:def_31_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = nor3c iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)) ); definition func xor3 -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def32: :: TWOSCOMP:def 32 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (x 'xor' y) 'xor' z; existence ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'xor' y) 'xor' z proofend; uniqueness for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'xor' y) 'xor' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x 'xor' y) 'xor' z ) holds b1 = b2 proofend; end; :: deftheorem Def32 defines xor3 TWOSCOMP:def_32_:_ for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds ( b1 = xor3 iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'xor' y) 'xor' z ); theorem :: TWOSCOMP:12 for x, y, z being 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 & and3c . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) ) by Def16, Def17, Def18, Def19; theorem :: TWOSCOMP:13 for x, y, z being 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) & nand3c . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) ) by Def20, Def21, Def22, Def23; theorem :: TWOSCOMP:14 for x, y, z being 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 & or3c . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) ) by Def24, Def25, Def26, Def27; theorem :: TWOSCOMP:15 for x, y, z being 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) & nor3c . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)) ) by Def28, Def29, Def30, Def31; theorem :: TWOSCOMP:16 for x, y, z being Element of BOOLEAN holds ( and3 . <*x,y,z*> = nor3c . <*x,y,z*> & and3a . <*x,y,z*> = nor3b . <*z,y,x*> & and3b . <*x,y,z*> = nor3a . <*z,y,x*> & and3c . <*x,y,z*> = nor3 . <*x,y,z*> ) proofend; theorem :: TWOSCOMP:17 for x, y, z being Element of BOOLEAN holds ( or3 . <*x,y,z*> = nand3c . <*x,y,z*> & or3a . <*x,y,z*> = nand3b . <*z,y,x*> & or3b . <*x,y,z*> = nand3a . <*z,y,x*> & or3c . <*x,y,z*> = nand3 . <*x,y,z*> ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; theorem :: TWOSCOMP:21 ( and3c . <*0,0,0*> = 1 & and3c . <*0,0,1*> = 0 & and3c . <*0,1,0*> = 0 & and3c . <*0,1,1*> = 0 & and3c . <*1,0,0*> = 0 & and3c . <*1,0,1*> = 0 & and3c . <*1,1,0*> = 0 & and3c . <*1,1,1*> = 0 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; theorem :: TWOSCOMP:25 ( or3c . <*0,0,0*> = 1 & or3c . <*0,0,1*> = 1 & or3c . <*0,1,0*> = 1 & or3c . <*0,1,1*> = 1 & or3c . <*1,0,0*> = 1 & or3c . <*1,0,1*> = 1 & or3c . <*1,1,0*> = 1 & or3c . <*1,1,1*> = 0 ) proofend; 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 ) proofend; begin ::--------------------------------------------------------------------------- :: 1bit 2's Complement Circuit (Complementor + Incrementor) ::--------------------------------------------------------------------------- :: Complementor definition let x, b be set ; func CompStr (x,b) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: TWOSCOMP:def 33 1GateCircStr (<*x,b*>,xor2a); correctness coherence 1GateCircStr (<*x,b*>,xor2a) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ; end; :: deftheorem defines CompStr TWOSCOMP:def_33_:_ for x, b being set holds CompStr (x,b) = 1GateCircStr (<*x,b*>,xor2a); definition let x, b be set ; func CompCirc (x,b) -> strict gate`2=den Boolean Circuit of CompStr (x,b) equals :: TWOSCOMP:def 34 1GateCircuit (x,b,xor2a); coherence 1GateCircuit (x,b,xor2a) is strict gate`2=den Boolean Circuit of CompStr (x,b) ; end; :: deftheorem defines CompCirc TWOSCOMP:def_34_:_ for x, b being set holds CompCirc (x,b) = 1GateCircuit (x,b,xor2a); definition let x, b be set ; func CompOutput (x,b) -> Element of InnerVertices (CompStr (x,b)) equals :: TWOSCOMP:def 35 [<*x,b*>,xor2a]; coherence [<*x,b*>,xor2a] is Element of InnerVertices (CompStr (x,b)) by FACIRC_1:47; end; :: deftheorem defines CompOutput TWOSCOMP:def_35_:_ for x, b being set holds CompOutput (x,b) = [<*x,b*>,xor2a]; :: Incrementor definition let x, b be set ; func IncrementStr (x,b) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: TWOSCOMP:def 36 1GateCircStr (<*x,b*>,and2a); correctness coherence 1GateCircStr (<*x,b*>,and2a) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ; end; :: deftheorem defines IncrementStr TWOSCOMP:def_36_:_ for x, b being set holds IncrementStr (x,b) = 1GateCircStr (<*x,b*>,and2a); definition let x, b be set ; func IncrementCirc (x,b) -> strict gate`2=den Boolean Circuit of IncrementStr (x,b) equals :: TWOSCOMP:def 37 1GateCircuit (x,b,and2a); coherence 1GateCircuit (x,b,and2a) is strict gate`2=den Boolean Circuit of IncrementStr (x,b) ; end; :: deftheorem defines IncrementCirc TWOSCOMP:def_37_:_ for x, b being set holds IncrementCirc (x,b) = 1GateCircuit (x,b,and2a); definition let x, b be set ; func IncrementOutput (x,b) -> Element of InnerVertices (IncrementStr (x,b)) equals :: TWOSCOMP:def 38 [<*x,b*>,and2a]; coherence [<*x,b*>,and2a] is Element of InnerVertices (IncrementStr (x,b)) by FACIRC_1:47; end; :: deftheorem defines IncrementOutput TWOSCOMP:def_38_:_ for x, b being set holds IncrementOutput (x,b) = [<*x,b*>,and2a]; :: 2's-BitComplementor definition let x, b be set ; func BitCompStr (x,b) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: TWOSCOMP:def 39 (CompStr (x,b)) +* (IncrementStr (x,b)); correctness coherence (CompStr (x,b)) +* (IncrementStr (x,b)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ; end; :: deftheorem defines BitCompStr TWOSCOMP:def_39_:_ for x, b being set holds BitCompStr (x,b) = (CompStr (x,b)) +* (IncrementStr (x,b)); definition let x, b be set ; func BitCompCirc (x,b) -> strict gate`2=den Boolean Circuit of BitCompStr (x,b) equals :: TWOSCOMP:def 40 (CompCirc (x,b)) +* (IncrementCirc (x,b)); coherence (CompCirc (x,b)) +* (IncrementCirc (x,b)) is strict gate`2=den Boolean Circuit of BitCompStr (x,b) ; end; :: deftheorem defines BitCompCirc TWOSCOMP:def_40_:_ for x, b being set holds BitCompCirc (x,b) = (CompCirc (x,b)) +* (IncrementCirc (x,b)); theorem Th27: :: TWOSCOMP:27 for x, b being non pair set holds the carrier of (CompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a]} proofend; theorem :: TWOSCOMP:28 for x, b being non pair set holds [<*x,b*>,xor2a] in InnerVertices (CompStr (x,b)) proofend; theorem :: TWOSCOMP:29 for x, b being non pair set holds ( x in InputVertices (CompStr (x,b)) & b in InputVertices (CompStr (x,b)) ) proofend; theorem :: TWOSCOMP:30 for x, b being non pair set holds InputVertices (CompStr (x,b)) is without_pairs proofend; theorem Th31: :: TWOSCOMP:31 for x, b being non pair set holds the carrier of (IncrementStr (x,b)) = {x,b} \/ {[<*x,b*>,and2a]} proofend; theorem :: TWOSCOMP:32 for x, b being non pair set holds [<*x,b*>,and2a] in InnerVertices (IncrementStr (x,b)) proofend; theorem :: TWOSCOMP:33 for x, b being non pair set holds ( x in InputVertices (IncrementStr (x,b)) & b in InputVertices (IncrementStr (x,b)) ) proofend; theorem :: TWOSCOMP:34 for x, b being non pair set holds InputVertices (IncrementStr (x,b)) is without_pairs proofend; :: 2's-BitComplementor theorem :: TWOSCOMP:35 for x, b being non pair set holds InnerVertices (BitCompStr (x,b)) is Relation proofend; theorem Th36: :: TWOSCOMP:36 for x, b being 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)) ) proofend; theorem Th37: :: TWOSCOMP:37 for x, b being non pair set holds the carrier of (BitCompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]} proofend; theorem Th38: :: TWOSCOMP:38 for x, b being non pair set holds InnerVertices (BitCompStr (x,b)) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]} proofend; theorem Th39: :: TWOSCOMP:39 for x, b being non pair set holds ( [<*x,b*>,xor2a] in InnerVertices (BitCompStr (x,b)) & [<*x,b*>,and2a] in InnerVertices (BitCompStr (x,b)) ) proofend; theorem Th40: :: TWOSCOMP:40 for x, b being non pair set holds InputVertices (BitCompStr (x,b)) = {x,b} proofend; theorem Th41: :: TWOSCOMP:41 for x, b being non pair set holds ( x in InputVertices (BitCompStr (x,b)) & b in InputVertices (BitCompStr (x,b)) ) proofend; theorem :: TWOSCOMP:42 for x, b being non pair set holds InputVertices (BitCompStr (x,b)) is without_pairs proofend; ::------------------------------------------------------------------------ :: for s being State of BitCompCirc(x,b) holds (Following s) is stable ::------------------------------------------------------------------------ theorem Th43: :: TWOSCOMP:43 for x, b being non pair set for s being 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 ) proofend; theorem :: TWOSCOMP:44 for x, b being non pair set for s being State of (CompCirc (x,b)) for a1, a2 being 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 ) proofend; theorem Th45: :: TWOSCOMP:45 for x, b being non pair set for s being 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 ) proofend; theorem Th46: :: TWOSCOMP:46 for x, b being non pair set for s being State of (BitCompCirc (x,b)) for a1, a2 being 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 ) proofend; theorem Th47: :: TWOSCOMP:47 for x, b being non pair set for s being 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 ) proofend; theorem :: TWOSCOMP:48 for x, b being non pair set for s being State of (IncrementCirc (x,b)) for a1, a2 being 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 ) proofend; theorem Th49: :: TWOSCOMP:49 for x, b being non pair set for s being 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 ) proofend; theorem Th50: :: TWOSCOMP:50 for x, b being non pair set for s being State of (BitCompCirc (x,b)) for a1, a2 being 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 ) proofend; theorem :: TWOSCOMP:51 for x, b being non pair set for s being 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 being non pair set for s being State of (BitCompCirc (x,b)) for a1, a2 being 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 being non pair set for s being State of (BitCompCirc (x,b)) holds Following s is stable proofend;