:: 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-2025 Association of Mizar Users


::---------------------------------------------------------------------------
:: 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 func s . v -> Element of BOOLEAN ;
coherence
s . v is Element of BOOLEAN
proof end;
end;

deffunc H1( Element of BOOLEAN , Element of BOOLEAN ) -> Element of BOOLEAN = $1 '&' $2;

notation
synonym and2 for '&' ;
end;

canceled;

::$CD
definition
func and2a -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def1: :: TWOSCOMP:def 1
 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
proof end;
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
proof end;
end;

:: deftheorem Def1 defines and2a TWOSCOMP:def 1 :
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 );

canceled;

::$CD
definition
func nand2 -> 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)
proof end;
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
proof end;
func nand2a -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def3: :: TWOSCOMP:def 3
 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)
proof end;
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
proof end;
end;

:: deftheorem Def2 defines nand2 TWOSCOMP:def 2 :
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 Def3 defines nand2a TWOSCOMP:def 3 :
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) );

notation
synonym or2 for 'or' ;
end;

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

canceled;

canceled;

::$CD 2
definition
func or2a -> 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) '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
proof end;
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
proof end;
end;

:: deftheorem Def4 defines or2a TWOSCOMP:def 4 :
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 );

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

canceled;

::$CD
definition
func nor2 -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def5: :: TWOSCOMP:def 5
 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)
proof end;
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
proof end;
func nor2a -> 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) '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)
proof end;
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
proof end;
end;

:: deftheorem Def5 defines nor2 TWOSCOMP:def 5 :
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 Def6 defines nor2a TWOSCOMP:def 6 :
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) );

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

notation
synonym xor2 for 'xor' ;
end;

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

canceled;

canceled;

::$CD 2
definition
func xor2a -> Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def7: :: TWOSCOMP:def 7
 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
proof end;
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
proof end;
func xor2b -> 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) '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)
proof end;
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
proof end;
end;

:: deftheorem Def7 defines xor2a TWOSCOMP:def 7 :
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 Def8 defines xor2b TWOSCOMP:def 8 :
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 & nor2 . <*x,y*> = ('not' x) '&' ('not' y) ) by FACIRC_1:def 6, Def1, Lm3;

theorem :: TWOSCOMP:2
for x, y being 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 being 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 being 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 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 FACIRC_1:def 4, Def7, Def8;

theorem :: TWOSCOMP:6
for x, y being Element of BOOLEAN holds and2a . <*x,y*> = nor2a . <*y,x*>
proof end;

theorem :: TWOSCOMP:7
for x, y being Element of BOOLEAN holds or2a . <*x,y*> = nand2a . <*y,x*>
proof end;

theorem :: TWOSCOMP:8
for x, y being Element of BOOLEAN holds xor2b . <*x,y*> = xor2 . <*x,y*>
proof 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 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 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 end;

:: 3-Input Operators
definition
func and3 -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def9: :: TWOSCOMP:def 9
 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
proof end;
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
proof end;
func and3a -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def10: :: TWOSCOMP:def 10
 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
proof end;
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
proof end;
func and3b -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def11: :: TWOSCOMP:def 11
 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
proof end;
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
proof end;
end;

:: deftheorem Def9 defines and3 TWOSCOMP:def 9 :
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 Def10 defines and3a TWOSCOMP:def 10 :
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 Def11 defines and3b TWOSCOMP:def 11 :
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 );

canceled;

::$CD
definition
func nand3 -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def12: :: TWOSCOMP:def 12
 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)
proof end;
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
proof end;
func nand3a -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def13: :: TWOSCOMP:def 13
 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)
proof end;
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
proof end;
func nand3b -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def14: :: TWOSCOMP:def 14
 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)
proof end;
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
proof end;
end;

:: deftheorem Def12 defines nand3 TWOSCOMP:def 12 :
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 Def13 defines nand3a TWOSCOMP:def 13 :
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 Def14 defines nand3b TWOSCOMP:def 14 :
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) );

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

canceled;

canceled;

::$CD 2
definition
func or3a -> Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def15: :: TWOSCOMP:def 15
 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
proof end;
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
proof end;
func or3b -> 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*> = (('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
proof end;
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
proof end;
end;

:: deftheorem Def15 defines or3a TWOSCOMP:def 15 :
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 Def16 defines or3b TWOSCOMP:def 16 :
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 );

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

canceled;

::$CD
definition
func nor3 -> 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 '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)
proof end;
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
proof end;
func nor3a -> 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' ((('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)
proof end;
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
proof end;
func nor3b -> 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' ((('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)
proof end;
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
proof end;
end;

:: deftheorem Def17 defines nor3 TWOSCOMP:def 17 :
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 Def18 defines nor3a TWOSCOMP:def 18 :
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 Def19 defines nor3b TWOSCOMP:def 19 :
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) );

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

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

canceled;

::$CD
definition
func xor3 -> 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*> = (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
proof end;
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
proof end;
end;

:: deftheorem Def20 defines xor3 TWOSCOMP:def 20 :
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 & nor3 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) ) by Def9, Def10, Def11, Lm7;

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) & or3 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) ) by Def12, Def13, Def14, Lm5;

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 & 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 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) & 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 being Element of BOOLEAN holds
( and3a . <*x,y,z*> = nor3b . <*z,y,x*> & and3b . <*x,y,z*> = nor3a . <*z,y,x*> )
proof end;

theorem :: TWOSCOMP:17
for x, y, z being Element of BOOLEAN holds
( or3a . <*x,y,z*> = nand3b . <*z,y,x*> & or3b . <*x,y,z*> = nand3a . <*z,y,x*> )
proof 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 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 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 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 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 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 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 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 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 end;

::---------------------------------------------------------------------------
:: 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 21
 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 21 :
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 22
 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 22 :
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 23
[<*x,b*>,xor2a];
coherence
[<*x,b*>,xor2a] is Element of InnerVertices (CompStr (x,b)) by FACIRC_1:47;
end;

:: deftheorem defines CompOutput TWOSCOMP:def 23 :
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 24
 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 24 :
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 25
 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 25 :
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 26
[<*x,b*>,and2a];
coherence
[<*x,b*>,and2a] is Element of InnerVertices (IncrementStr (x,b)) by FACIRC_1:47;
end;

:: deftheorem defines IncrementOutput TWOSCOMP:def 26 :
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 27
(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 27 :
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 28
(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 28 :
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]}
proof end;

theorem :: TWOSCOMP:28
for x, b being non pair set holds [<*x,b*>,xor2a] in InnerVertices (CompStr (x,b))
proof end;

theorem :: TWOSCOMP:29
for x, b being non pair set holds
( x in InputVertices (CompStr (x,b)) & b in InputVertices (CompStr (x,b)) )
proof end;

theorem :: TWOSCOMP:30
for x, b being non pair set holds InputVertices (CompStr (x,b)) is without_pairs
proof end;

theorem Th31: :: TWOSCOMP:31
for x, b being non pair set holds the carrier of (IncrementStr (x,b)) = {x,b} \/ {[<*x,b*>,and2a]}
proof end;

theorem :: TWOSCOMP:32
for x, b being non pair set holds [<*x,b*>,and2a] in InnerVertices (IncrementStr (x,b))
proof end;

theorem :: TWOSCOMP:33
for x, b being non pair set holds
( x in InputVertices (IncrementStr (x,b)) & b in InputVertices (IncrementStr (x,b)) )
proof end;

theorem :: TWOSCOMP:34
for x, b being non pair set holds InputVertices (IncrementStr (x,b)) is without_pairs
proof end;

:: 2's-BitComplementor
theorem :: TWOSCOMP:35
for x, b being non pair set holds InnerVertices (BitCompStr (x,b)) is Relation
proof end;

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)) )
proof end;

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]}
proof end;

theorem Th38: :: TWOSCOMP:38
for x, b being non pair set holds InnerVertices (BitCompStr (x,b)) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
proof end;

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)) )
proof end;

theorem Th40: :: TWOSCOMP:40
for x, b being non pair set holds InputVertices (BitCompStr (x,b)) = {x,b}
proof end;

theorem Th41: :: TWOSCOMP:41
for x, b being non pair set holds
( x in InputVertices (BitCompStr (x,b)) & b in InputVertices (BitCompStr (x,b)) )
proof end;

theorem :: TWOSCOMP:42
for x, b being non pair set holds InputVertices (BitCompStr (x,b)) is without_pairs
proof end;

::------------------------------------------------------------------------
:: 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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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
proof end;

theorem :: TWOSCOMP:54
for x, y being Element of BOOLEAN holds nor2 . <*x,y*> = ('not' x) '&' ('not' y) by Lm3;

theorem :: TWOSCOMP:55
for x, y being Element of BOOLEAN holds or2 . <*x,y*> = 'not' (('not' x) '&' ('not' y)) by Lm1;

theorem :: TWOSCOMP:56
for x, y being Element of BOOLEAN holds and2 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) by Lm4;

theorem :: TWOSCOMP:57
for x, y being Element of BOOLEAN holds nand2 . <*x,y*> = ('not' x) 'or' ('not' y) by Lm2;

theorem :: TWOSCOMP:58
for x, y, z being Element of BOOLEAN holds nor3 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) by Lm7;

theorem :: TWOSCOMP:59
for x, y, z being Element of BOOLEAN holds or3 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) by Lm5;

theorem :: TWOSCOMP:60
for x, y, z being 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 being Element of BOOLEAN holds and3 . <*x,y,z*> = 'not' ((('not' x) 'or' ('not' y)) 'or' ('not' z)) by Lm8;