:: TWOSCOMP semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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;

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
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*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' y ) holds
b1 = b2
proof end;
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
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 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)
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) '&' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) '&' ('not' y) ) holds
b1 = b2
proof end;
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)
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 :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)
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;
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))
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) '&' ('not' y)) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (('not' x) '&' ('not' y)) ) holds
b1 = b2
proof end;
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
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*> = x 'or' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'or' y ) holds
b1 = b2
proof end;
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
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 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)
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' ('not' y) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = ('not' x) 'or' ('not' y) ) holds
b1 = b2
proof end;
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)
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 :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)
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;
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))
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' ('not' y)) ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) ) holds
b1 = b2
proof end;
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
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*> = x 'xor' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'xor' y ) holds
b1 = b2
proof end;
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
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 :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)
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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TWOSCOMP:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TWOSCOMP:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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*> )
proof end;

theorem :: TWOSCOMP:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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*> )
proof end;

theorem :: TWOSCOMP:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of BOOLEAN holds xor2b . <*x,y*> = xor2 . <*x,y*>
proof end;

theorem :: TWOSCOMP:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 )
proof end;

theorem :: TWOSCOMP:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 )
proof end;

theorem :: TWOSCOMP:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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;

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
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 :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
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 :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
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;
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)
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)) '&' ('not' z) ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (('not' x) '&' ('not' y)) '&' ('not' z) ) holds
b1 = b2
proof end;
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)
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 :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)
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 :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)
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;
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))
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)) '&' ('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
proof end;
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
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 '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
proof end;
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
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 :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
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;
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)
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' ('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
proof end;
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)
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 :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)
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 :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)
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;
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))
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' ('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
proof end;
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
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 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:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TWOSCOMP:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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*> )
proof end;

theorem :: TWOSCOMP:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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*> )
proof end;

theorem :: TWOSCOMP:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 )
proof end;

theorem :: TWOSCOMP:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 )
proof end;

theorem :: TWOSCOMP:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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;

definition
let x, b be set ;
func CompStr x,b -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: TWOSCOMP:def 33
 1GateCircStr <*x,b*>,xor2a ;
correctness
coherence
1GateCircStr <*x,b*>,xor2a is non empty strict non void 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 ];

definition
let x, b be set ;
func IncrementStr x,b -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: TWOSCOMP:def 36
 1GateCircStr <*x,b*>,and2a ;
correctness
coherence
1GateCircStr <*x,b*>,and2a is non empty strict non void 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 ];

definition
let x, b be set ;
func BitCompStr x,b -> non empty strict non void 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 strict non void 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 Th30: :: TWOSCOMP:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds InnerVertices (CompStr x,b) is Relation by FACIRC_1:38;

theorem Th31: :: TWOSCOMP:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds
( x in the carrier of (CompStr x,b) & b in the carrier of (CompStr x,b) & [<*x,b*>,xor2a ] in the carrier of (CompStr x,b) ) by FACIRC_1:43;

theorem Th32: :: TWOSCOMP:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds the carrier of (CompStr x,b) = {x,b} \/ {[<*x,b*>,xor2a ]}
proof end;

theorem Th33: :: TWOSCOMP:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds InnerVertices (CompStr x,b) = {[<*x,b*>,xor2a ]} by CIRCCOMB:49;

theorem Th34: :: TWOSCOMP:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds [<*x,b*>,xor2a ] in InnerVertices (CompStr x,b)
proof end;

theorem Th35: :: TWOSCOMP:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds InputVertices (CompStr x,b) = {x,b} by FACIRC_1:40;

theorem :: TWOSCOMP:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds
( x in InputVertices (CompStr x,b) & b in InputVertices (CompStr x,b) )
proof end;

theorem :: TWOSCOMP:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds not InputVertices (CompStr x,b) is with_pair
proof end;

theorem Th38: :: TWOSCOMP:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds InnerVertices (IncrementStr x,b) is Relation by FACIRC_1:38;

theorem Th39: :: TWOSCOMP:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds
( x in the carrier of (IncrementStr x,b) & b in the carrier of (IncrementStr x,b) & [<*x,b*>,and2a ] in the carrier of (IncrementStr x,b) ) by FACIRC_1:43;

theorem Th40: :: TWOSCOMP:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds the carrier of (IncrementStr x,b) = {x,b} \/ {[<*x,b*>,and2a ]}
proof end;

theorem Th41: :: TWOSCOMP:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds InnerVertices (IncrementStr x,b) = {[<*x,b*>,and2a ]} by CIRCCOMB:49;

theorem Th42: :: TWOSCOMP:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds [<*x,b*>,and2a ] in InnerVertices (IncrementStr x,b)
proof end;

theorem Th43: :: TWOSCOMP:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds InputVertices (IncrementStr x,b) = {x,b} by FACIRC_1:40;

theorem :: TWOSCOMP:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds
( x in InputVertices (IncrementStr x,b) & b in InputVertices (IncrementStr x,b) )
proof end;

theorem :: TWOSCOMP:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds not InputVertices (IncrementStr x,b) is with_pair
proof end;

theorem :: TWOSCOMP:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds InnerVertices (BitCompStr x,b) is Relation
proof end;

theorem Th47: :: TWOSCOMP:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th48: :: TWOSCOMP:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th49: :: TWOSCOMP:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds InnerVertices (BitCompStr x,b) = {[<*x,b*>,xor2a ],[<*x,b*>,and2a ]}
proof end;

theorem Th50: :: TWOSCOMP:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th51: :: TWOSCOMP:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds InputVertices (BitCompStr x,b) = {x,b}
proof end;

theorem Th52: :: TWOSCOMP:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds
( x in InputVertices (BitCompStr x,b) & b in InputVertices (BitCompStr x,b) )
proof end;

theorem :: TWOSCOMP:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set holds not InputVertices (BitCompStr x,b) is with_pair
proof end;

theorem Th54: :: TWOSCOMP:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th56: :: TWOSCOMP:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th57: :: TWOSCOMP:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th58: :: TWOSCOMP:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th60: :: TWOSCOMP:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th61: :: TWOSCOMP:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th56, Th60;

theorem :: TWOSCOMP:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th57, Th61;

theorem :: TWOSCOMP:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, b being non pair set
for s being State of (BitCompCirc x,b) holds Following s is stable
proof end;