:: TWOSCOMP semantic presentation

begin

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
proof
 s . v in the Sorts of A . v by CIRCUIT1:4;
hence  s . v is Element of BOOLEAN ; ::_thesis: verum
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
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H1(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H1(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H1(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) '&' $2;
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) '&' $2;
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) '&' ('not' $2);
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) '&' ('not' $2);
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ($1 '&' $2);
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ($1 '&' $2);
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (('not' $1) '&' $2);
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (('not' $1) '&' $2);
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (('not' $1) '&' ('not' $2));
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (('not' $1) '&' ('not' $2));
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = $1 'or' $2;
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = $1 'or' $2;
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) 'or' $2;
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) 'or' $2;
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) 'or' ('not' $2);
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) 'or' ('not' $2);
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ($1 'or' $2);
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ($1 'or' $2);
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (('not' $1) 'or' $2);
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (('not' $1) 'or' $2);
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (('not' $1) 'or' ('not' $2));
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (('not' $1) 'or' ('not' $2));
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = $1 'xor' $2;
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = $1 'xor' $2;
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) 'xor' $2;
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) 'xor' $2;
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) 'xor' ('not' $2);
thus  ex t being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds t . <*x,y*> = H2(x,y) from FACIRC_1:sch_1(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ('not' $1) 'xor' ('not' $2);
thus  for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H2(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H2(x,y) ) holds
t1 = t2 from FACIRC_1:sch_2(); ::_thesis: verum
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
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*> )
proof
let x, y be Element of BOOLEAN ; ::_thesis: ( and2 . <*x,y*> = nor2b . <*x,y*> & and2a . <*x,y*> = nor2a . <*y,x*> & and2b . <*x,y*> = nor2 . <*x,y*> )
thus and2 . <*x,y*> = 'not' (('not' x) 'or' ('not' y)) by Def1
.= nor2b . <*x,y*> by Def12 ; ::_thesis: ( and2a . <*x,y*> = nor2a . <*y,x*> & and2b . <*x,y*> = nor2 . <*x,y*> )
thus and2a . <*x,y*> = 'not' (('not' ('not' x)) 'or' ('not' y)) by Def2
.= nor2a . <*y,x*> by Def11 ; ::_thesis: and2b . <*x,y*> = nor2 . <*x,y*>
thus and2b . <*x,y*> = 'not' (('not' ('not' x)) 'or' ('not' ('not' y))) by Def3
.= nor2 . <*x,y*> by Def10 ; ::_thesis: verum
end;

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*> )
proof
let x, y be Element of BOOLEAN ; ::_thesis: ( or2 . <*x,y*> = nand2b . <*x,y*> & or2a . <*x,y*> = nand2a . <*y,x*> & or2b . <*x,y*> = nand2 . <*x,y*> )
thus or2 . <*x,y*> = x 'or' y by Def7
.= nand2b . <*x,y*> by Def6 ; ::_thesis: ( or2a . <*x,y*> = nand2a . <*y,x*> & or2b . <*x,y*> = nand2 . <*x,y*> )
thus or2a . <*x,y*> = ('not' x) 'or' y by Def8
.= nand2a . <*y,x*> by Def5 ; ::_thesis: or2b . <*x,y*> = nand2 . <*x,y*>
thus or2b . <*x,y*> = ('not' x) 'or' ('not' y) by Def9
.= nand2 . <*x,y*> by Def4 ; ::_thesis: verum
end;

theorem :: TWOSCOMP:8
for x, y being Element of BOOLEAN holds xor2b . <*x,y*> = xor2 . <*x,y*>
proof
let x, y be Element of BOOLEAN ; ::_thesis: xor2b . <*x,y*> = xor2 . <*x,y*>
thus xor2b . <*x,y*> = ('not' x) 'xor' ('not' y) by Def15
.= x 'xor' y
.= xor2 . <*x,y*> by Def13 ; ::_thesis: verum
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 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
proof
thus and2 . <*0,0*> = FALSE '&' FALSE by Def1
.= 0 ; ::_thesis: ( 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 )
thus and2 . <*0,1*> = FALSE '&' TRUE by Def1
.= 0 ; ::_thesis: ( 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 )
thus and2 . <*1,0*> = TRUE '&' FALSE by Def1
.= 0 ; ::_thesis: ( 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 )
thus and2 . <*1,1*> = TRUE '&' TRUE by Def1
.= 1 ; ::_thesis: ( 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 )
thus and2a . <*0,0*> = ('not' FALSE) '&' FALSE by Def2
.= 0 ; ::_thesis: ( 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 )
thus and2a . <*0,1*> = ('not' FALSE) '&' TRUE by Def2
.= 1 ; ::_thesis: ( and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2a . <*1,0*> = ('not' TRUE) '&' FALSE by Def2
.= 0 ; ::_thesis: ( and2a . <*1,1*> = 0 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2a . <*1,1*> = ('not' TRUE) '&' TRUE by Def2
.= 0 ; ::_thesis: ( and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2b . <*0,0*> = TRUE '&' ('not' FALSE) by Def3
.= 1 ; ::_thesis: ( and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2b . <*0,1*> = ('not' FALSE) '&' ('not' TRUE) by Def3
.= 0 ; ::_thesis: ( and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )
thus and2b . <*1,0*> = ('not' TRUE) '&' ('not' FALSE) by Def3
.= 0 ; ::_thesis: and2b . <*1,1*> = 0
thus and2b . <*1,1*> = FALSE '&' ('not' TRUE) by Def3
.= 0 ; ::_thesis: verum
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 & or2b . <*0,0*> = 1 & or2b . <*0,1*> = 1 & or2b . <*1,0*> = 1 & or2b . <*1,1*> = 0 )
proof
thus or2 . <*0,0*> = FALSE 'or' FALSE by Def7
.= 0 ; ::_thesis: ( 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 )
thus or2 . <*0,1*> = FALSE 'or' TRUE by Def7
.= 1 ; ::_thesis: ( 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 )
thus or2 . <*1,0*> = TRUE 'or' FALSE by Def7
.= 1 ; ::_thesis: ( 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 )
thus or2 . <*1,1*> = TRUE 'or' TRUE by Def7
.= 1 ; ::_thesis: ( 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 )
thus or2a . <*0,0*> = TRUE 'or' FALSE by Def8
.= 1 ; ::_thesis: ( 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 )
thus or2a . <*0,1*> = ('not' FALSE) 'or' TRUE by Def8
.= 1 ; ::_thesis: ( or2a . <*1,0*> = 0 & or2a . <*1,1*> = 1 & or2b . <*0,0*> = 1 & or2b . <*0,1*> = 1 & or2b . <*1,0*> = 1 & or2b . <*1,1*> = 0 )
thus or2a . <*1,0*> = ('not' TRUE) 'or' FALSE by Def8
.= 0 ; ::_thesis: ( or2a . <*1,1*> = 1 & or2b . <*0,0*> = 1 & or2b . <*0,1*> = 1 & or2b . <*1,0*> = 1 & or2b . <*1,1*> = 0 )
thus or2a . <*1,1*> = ('not' TRUE) 'or' TRUE by Def8
.= 1 ; ::_thesis: ( or2b . <*0,0*> = 1 & or2b . <*0,1*> = 1 & or2b . <*1,0*> = 1 & or2b . <*1,1*> = 0 )
thus or2b . <*0,0*> = TRUE 'or' ('not' FALSE) by Def9
.= 1 ; ::_thesis: ( or2b . <*0,1*> = 1 & or2b . <*1,0*> = 1 & or2b . <*1,1*> = 0 )
thus or2b . <*0,1*> = TRUE 'or' ('not' TRUE) by Def9
.= 1 ; ::_thesis: ( or2b . <*1,0*> = 1 & or2b . <*1,1*> = 0 )
thus or2b . <*1,0*> = ('not' TRUE) 'or' TRUE by Def9
.= 1 ; ::_thesis: or2b . <*1,1*> = 0
thus or2b . <*1,1*> = FALSE 'or' ('not' TRUE) by Def9
.= 0 ; ::_thesis: verum
end;

theorem :: TWOSCOMP:11
( xor2 . <*0,0*> = 0 & xor2 . <*0,1*> = 1 & xor2 . <*1,0*> = 1 & xor2 . <*1,1*> = 0 & xor2a . <*0,0*> = 1 & xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
proof
thus xor2 . <*0,0*> = FALSE 'xor' FALSE by Def13
.= 0 ; ::_thesis: ( 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 )
thus xor2 . <*0,1*> = FALSE 'xor' TRUE by Def13
.= 1 ; ::_thesis: ( xor2 . <*1,0*> = 1 & xor2 . <*1,1*> = 0 & xor2a . <*0,0*> = 1 & xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2 . <*1,0*> = TRUE 'xor' FALSE by Def13
.= 1 ; ::_thesis: ( xor2 . <*1,1*> = 0 & xor2a . <*0,0*> = 1 & xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2 . <*1,1*> = TRUE 'xor' TRUE by Def13
.= 0 ; ::_thesis: ( xor2a . <*0,0*> = 1 & xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2a . <*0,0*> = ('not' FALSE) 'xor' FALSE by Def14
.= 1 ; ::_thesis: ( xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2a . <*0,1*> = ('not' FALSE) 'xor' TRUE by Def14
.= 0 ; ::_thesis: ( xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )
thus xor2a . <*1,0*> = ('not' TRUE) 'xor' FALSE by Def14
.= 0 ; ::_thesis: xor2a . <*1,1*> = 1
thus xor2a . <*1,1*> = ('not' TRUE) 'xor' TRUE by Def14
.= 1 ; ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ($1 '&' $2) '&' $3;
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ($1 '&' $2) '&' $3;
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) '&' $2) '&' $3;
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) '&' $2) '&' $3;
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) '&' ('not' $2)) '&' $3;
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) '&' ('not' $2)) '&' $3;
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) '&' ('not' $2)) '&' ('not' $3);
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) '&' ('not' $2)) '&' ('not' $3);
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (($1 '&' $2) '&' $3);
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (($1 '&' $2) '&' $3);
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) '&' $2) '&' $3);
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) '&' $2) '&' $3);
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) '&' ('not' $2)) '&' $3);
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) '&' ('not' $2)) '&' $3);
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) '&' ('not' $2)) '&' ('not' $3));
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) '&' ('not' $2)) '&' ('not' $3));
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ($1 'or' $2) 'or' $3;
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ($1 'or' $2) 'or' $3;
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) 'or' $2) 'or' $3;
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) 'or' $2) 'or' $3;
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) 'or' ('not' $2)) 'or' $3;
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) 'or' ('not' $2)) 'or' $3;
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) 'or' ('not' $2)) 'or' ('not' $3);
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = (('not' $1) 'or' ('not' $2)) 'or' ('not' $3);
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (($1 'or' $2) 'or' $3);
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' (($1 'or' $2) 'or' $3);
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) 'or' $2) 'or' $3);
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) 'or' $2) 'or' $3);
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) 'or' ('not' $2)) 'or' $3);
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) 'or' ('not' $2)) 'or' $3);
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) 'or' ('not' $2)) 'or' ('not' $3));
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = 'not' ((('not' $1) 'or' ('not' $2)) 'or' ('not' $3));
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ($1 'xor' $2) 'xor' $3;
thus  ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H2(x,y,z) from FACIRC_1:sch_4(); ::_thesis: verum
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
deffunc H2( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) ->  Element of BOOLEAN = ($1 'xor' $2) 'xor' $3;
thus  for t1, t2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds t1 . <*x,y,z*> = H2(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds t2 . <*x,y,z*> = H2(x,y,z) ) holds
t1 = t2 from FACIRC_1:sch_5(); ::_thesis: verum
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: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*> )
proof
let x, y, z be Element of BOOLEAN ; ::_thesis: ( 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*> )
thus and3 . <*x,y,z*> = 'not' (('not' ('not' (('not' x) 'or' ('not' y)))) 'or' ('not' z)) by Def16
.= nor3c . <*x,y,z*> by Def31 ; ::_thesis: ( and3a . <*x,y,z*> = nor3b . <*z,y,x*> & and3b . <*x,y,z*> = nor3a . <*z,y,x*> & and3c . <*x,y,z*> = nor3 . <*x,y,z*> )
thus and3a . <*x,y,z*> = 'not' (('not' ('not' (('not' ('not' x)) 'or' ('not' y)))) 'or' ('not' z)) by Def17
.= 'not' ((('not' z) 'or' ('not' y)) 'or' x)
.= nor3b . <*z,y,x*> by Def30 ; ::_thesis: ( and3b . <*x,y,z*> = nor3a . <*z,y,x*> & and3c . <*x,y,z*> = nor3 . <*x,y,z*> )
thus and3b . <*x,y,z*> = 'not' (('not' ('not' (('not' ('not' x)) 'or' ('not' ('not' y))))) 'or' ('not' z)) by Def18
.= 'not' ((('not' z) 'or' y) 'or' x)
.= nor3a . <*z,y,x*> by Def29 ; ::_thesis: and3c . <*x,y,z*> = nor3 . <*x,y,z*>
thus and3c . <*x,y,z*> = 'not' (('not' ('not' (('not' ('not' x)) 'or' ('not' ('not' y))))) 'or' ('not' ('not' z))) by Def19
.= nor3 . <*x,y,z*> by Def28 ; ::_thesis: verum
end;

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*> )
proof
let x, y, z be Element of BOOLEAN ; ::_thesis: ( 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*> )
thus or3 . <*x,y,z*> = (x 'or' y) 'or' z by Def24
.= nand3c . <*x,y,z*> by Def23 ; ::_thesis: ( or3a . <*x,y,z*> = nand3b . <*z,y,x*> & or3b . <*x,y,z*> = nand3a . <*z,y,x*> & or3c . <*x,y,z*> = nand3 . <*x,y,z*> )
thus or3a . <*x,y,z*> = (('not' x) 'or' y) 'or' z by Def25
.= 'not' ((('not' z) '&' ('not' y)) '&' x)
.= nand3b . <*z,y,x*> by Def22 ; ::_thesis: ( or3b . <*x,y,z*> = nand3a . <*z,y,x*> & or3c . <*x,y,z*> = nand3 . <*x,y,z*> )
thus or3b . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z by Def26
.= 'not' ((('not' z) '&' y) '&' x)
.= nand3a . <*z,y,x*> by Def21 ; ::_thesis: or3c . <*x,y,z*> = nand3 . <*x,y,z*>
thus or3c . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) by Def27
.= nand3 . <*x,y,z*> by Def20 ; ::_thesis: verum
end;

theorem :: TWOSCOMP:18
( and3 . <*0,0,0*> = 0 & and3 . <*0,0,1*> = 0 & and3 . <*0,1,0*> = 0 & and3 . <*0,1,1*> = 0 & and3 . <*1,0,0*> = 0 & and3 . <*1,0,1*> = 0 & and3 . <*1,1,0*> = 0 & and3 . <*1,1,1*> = 1 )
proof
thus and3 . <*0,0,0*> = (FALSE '&' FALSE) '&' FALSE by Def16
.= 0 ; ::_thesis: ( 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 )
thus and3 . <*0,0,1*> = (FALSE '&' FALSE) '&' TRUE by Def16
.= 0 ; ::_thesis: ( 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 )
thus and3 . <*0,1,0*> = (FALSE '&' TRUE) '&' FALSE by Def16
.= 0 ; ::_thesis: ( 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 )
thus and3 . <*0,1,1*> = FALSE '&' TRUE by Def16
.= 0 ; ::_thesis: ( and3 . <*1,0,0*> = 0 & and3 . <*1,0,1*> = 0 & and3 . <*1,1,0*> = 0 & and3 . <*1,1,1*> = 1 )
thus and3 . <*1,0,0*> = (TRUE '&' FALSE) '&' FALSE by Def16
.= 0 ; ::_thesis: ( and3 . <*1,0,1*> = 0 & and3 . <*1,1,0*> = 0 & and3 . <*1,1,1*> = 1 )
thus and3 . <*1,0,1*> = FALSE '&' TRUE by Def16
.= 0 ; ::_thesis: ( and3 . <*1,1,0*> = 0 & and3 . <*1,1,1*> = 1 )
thus and3 . <*1,1,0*> = (TRUE '&' TRUE) '&' FALSE by Def16
.= 0 ; ::_thesis: and3 . <*1,1,1*> = 1
thus and3 . <*1,1,1*> = TRUE '&' TRUE by Def16
.= 1 ; ::_thesis: verum
end;

theorem :: TWOSCOMP:19
( and3a . <*0,0,0*> = 0 & and3a . <*0,0,1*> = 0 & and3a . <*0,1,0*> = 0 & and3a . <*0,1,1*> = 1 & and3a . <*1,0,0*> = 0 & and3a . <*1,0,1*> = 0 & and3a . <*1,1,0*> = 0 & and3a . <*1,1,1*> = 0 )
proof
thus and3a . <*0,0,0*> = (('not' FALSE) '&' FALSE) '&' FALSE by Def17
.= 0 ; ::_thesis: ( 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 )
thus and3a . <*0,0,1*> = (('not' FALSE) '&' FALSE) '&' TRUE by Def17
.= 0 ; ::_thesis: ( 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 )
thus and3a . <*0,1,0*> = (('not' FALSE) '&' TRUE) '&' FALSE by Def17
.= 0 ; ::_thesis: ( 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 )
thus and3a . <*0,1,1*> = (('not' FALSE) '&' TRUE) '&' TRUE by Def17
.= 1 ; ::_thesis: ( and3a . <*1,0,0*> = 0 & and3a . <*1,0,1*> = 0 & and3a . <*1,1,0*> = 0 & and3a . <*1,1,1*> = 0 )
thus and3a . <*1,0,0*> = (('not' TRUE) '&' FALSE) '&' FALSE by Def17
.= 0 ; ::_thesis: ( and3a . <*1,0,1*> = 0 & and3a . <*1,1,0*> = 0 & and3a . <*1,1,1*> = 0 )
thus and3a . <*1,0,1*> = (('not' TRUE) '&' FALSE) '&' TRUE by Def17
.= 0 ; ::_thesis: ( and3a . <*1,1,0*> = 0 & and3a . <*1,1,1*> = 0 )
thus and3a . <*1,1,0*> = (('not' TRUE) '&' TRUE) '&' FALSE by Def17
.= 0 ; ::_thesis: and3a . <*1,1,1*> = 0
thus and3a . <*1,1,1*> = ('not' TRUE) '&' TRUE by Def17
.= 0 ; ::_thesis: verum
end;

theorem :: TWOSCOMP:20
( and3b . <*0,0,0*> = 0 & and3b . <*0,0,1*> = 1 & and3b . <*0,1,0*> = 0 & and3b . <*0,1,1*> = 0 & and3b . <*1,0,0*> = 0 & and3b . <*1,0,1*> = 0 & and3b . <*1,1,0*> = 0 & and3b . <*1,1,1*> = 0 )
proof
thus and3b . <*0,0,0*> = (('not' FALSE) '&' ('not' FALSE)) '&' FALSE by Def18
.= 0 ; ::_thesis: ( 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 )
thus and3b . <*0,0,1*> = (TRUE '&' ('not' FALSE)) '&' TRUE by Def18
.= 1 ; ::_thesis: ( 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 )
thus and3b . <*0,1,0*> = (('not' FALSE) '&' ('not' TRUE)) '&' FALSE by Def18
.= 0 ; ::_thesis: ( 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 )
thus and3b . <*0,1,1*> = (('not' FALSE) '&' ('not' TRUE)) '&' TRUE by Def18
.= 0 ; ::_thesis: ( and3b . <*1,0,0*> = 0 & and3b . <*1,0,1*> = 0 & and3b . <*1,1,0*> = 0 & and3b . <*1,1,1*> = 0 )
thus and3b . <*1,0,0*> = (('not' TRUE) '&' ('not' FALSE)) '&' FALSE by Def18
.= 0 ; ::_thesis: ( and3b . <*1,0,1*> = 0 & and3b . <*1,1,0*> = 0 & and3b . <*1,1,1*> = 0 )
thus and3b . <*1,0,1*> = (('not' TRUE) '&' ('not' FALSE)) '&' TRUE by Def18
.= 0 ; ::_thesis: ( and3b . <*1,1,0*> = 0 & and3b . <*1,1,1*> = 0 )
thus and3b . <*1,1,0*> = (('not' TRUE) '&' ('not' TRUE)) '&' FALSE by Def18
.= 0 ; ::_thesis: and3b . <*1,1,1*> = 0
thus and3b . <*1,1,1*> = (FALSE '&' ('not' TRUE)) '&' TRUE by Def18
.= 0 ; ::_thesis: verum
end;

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 )
proof
thus and3c . <*0,0,0*> = (TRUE '&' ('not' FALSE)) '&' ('not' FALSE) by Def19
.= 1 ; ::_thesis: ( 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 )
thus and3c . <*0,0,1*> = (('not' FALSE) '&' ('not' FALSE)) '&' ('not' TRUE) by Def19
.= 0 ; ::_thesis: ( 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 )
thus and3c . <*0,1,0*> = (('not' FALSE) '&' ('not' TRUE)) '&' ('not' FALSE) by Def19
.= 0 ; ::_thesis: ( 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 )
thus and3c . <*0,1,1*> = (('not' FALSE) '&' ('not' TRUE)) '&' FALSE by Def19
.= 0 ; ::_thesis: ( and3c . <*1,0,0*> = 0 & and3c . <*1,0,1*> = 0 & and3c . <*1,1,0*> = 0 & and3c . <*1,1,1*> = 0 )
thus and3c . <*1,0,0*> = (('not' TRUE) '&' ('not' FALSE)) '&' ('not' FALSE) by Def19
.= 0 ; ::_thesis: ( and3c . <*1,0,1*> = 0 & and3c . <*1,1,0*> = 0 & and3c . <*1,1,1*> = 0 )
thus and3c . <*1,0,1*> = (('not' TRUE) '&' ('not' FALSE)) '&' FALSE by Def19
.= 0 ; ::_thesis: ( and3c . <*1,1,0*> = 0 & and3c . <*1,1,1*> = 0 )
thus and3c . <*1,1,0*> = (FALSE '&' ('not' TRUE)) '&' ('not' FALSE) by Def19
.= 0 ; ::_thesis: and3c . <*1,1,1*> = 0
thus and3c . <*1,1,1*> = (('not' TRUE) '&' ('not' TRUE)) '&' FALSE by Def19
.= 0 ; ::_thesis: verum
end;

theorem :: TWOSCOMP:22
( or3 . <*0,0,0*> = 0 & or3 . <*0,0,1*> = 1 & or3 . <*0,1,0*> = 1 & or3 . <*0,1,1*> = 1 & or3 . <*1,0,0*> = 1 & or3 . <*1,0,1*> = 1 & or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )
proof
thus or3 . <*0,0,0*> = FALSE 'or' FALSE by Def24
.= 0 ; ::_thesis: ( 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 )
thus or3 . <*0,0,1*> = (FALSE 'or' FALSE) 'or' TRUE by Def24
.= 1 ; ::_thesis: ( 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 )
thus or3 . <*0,1,0*> = TRUE 'or' FALSE by Def24
.= 1 ; ::_thesis: ( 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 )
thus or3 . <*0,1,1*> = (FALSE 'or' TRUE) 'or' TRUE by Def24
.= 1 ; ::_thesis: ( or3 . <*1,0,0*> = 1 & or3 . <*1,0,1*> = 1 & or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )
thus or3 . <*1,0,0*> = TRUE 'or' FALSE by Def24
.= 1 ; ::_thesis: ( or3 . <*1,0,1*> = 1 & or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )
thus or3 . <*1,0,1*> = (TRUE 'or' FALSE) 'or' TRUE by Def24
.= 1 ; ::_thesis: ( or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )
thus or3 . <*1,1,0*> = (TRUE 'or' TRUE) 'or' FALSE by Def24
.= 1 ; ::_thesis: or3 . <*1,1,1*> = 1
thus or3 . <*1,1,1*> = (TRUE 'or' TRUE) 'or' TRUE by Def24
.= 1 ; ::_thesis: verum
end;

theorem :: TWOSCOMP:23
( or3a . <*0,0,0*> = 1 & or3a . <*0,0,1*> = 1 & or3a . <*0,1,0*> = 1 & or3a . <*0,1,1*> = 1 & or3a . <*1,0,0*> = 0 & or3a . <*1,0,1*> = 1 & or3a . <*1,1,0*> = 1 & or3a . <*1,1,1*> = 1 )
proof
thus or3a . <*0,0,0*> = ('not' FALSE) 'or' FALSE by Def25
.= 1 ; ::_thesis: ( 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 )
thus or3a . <*0,0,1*> = (('not' FALSE) 'or' FALSE) 'or' TRUE by Def25
.= 1 ; ::_thesis: ( 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 )
thus or3a . <*0,1,0*> = (('not' FALSE) 'or' TRUE) 'or' FALSE by Def25
.= 1 ; ::_thesis: ( 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 )
thus or3a . <*0,1,1*> = (('not' FALSE) 'or' TRUE) 'or' TRUE by Def25
.= 1 ; ::_thesis: ( or3a . <*1,0,0*> = 0 & or3a . <*1,0,1*> = 1 & or3a . <*1,1,0*> = 1 & or3a . <*1,1,1*> = 1 )
thus or3a . <*1,0,0*> = ('not' TRUE) 'or' FALSE by Def25
.= 0 ; ::_thesis: ( or3a . <*1,0,1*> = 1 & or3a . <*1,1,0*> = 1 & or3a . <*1,1,1*> = 1 )
thus or3a . <*1,0,1*> = (('not' TRUE) 'or' FALSE) 'or' TRUE by Def25
.= 1 ; ::_thesis: ( or3a . <*1,1,0*> = 1 & or3a . <*1,1,1*> = 1 )
thus or3a . <*1,1,0*> = TRUE 'or' FALSE by Def25
.= 1 ; ::_thesis: or3a . <*1,1,1*> = 1
thus or3a . <*1,1,1*> = (('not' TRUE) 'or' TRUE) 'or' TRUE by Def25
.= 1 ; ::_thesis: verum
end;

theorem :: TWOSCOMP:24
( or3b . <*0,0,0*> = 1 & or3b . <*0,0,1*> = 1 & or3b . <*0,1,0*> = 1 & or3b . <*0,1,1*> = 1 & or3b . <*1,0,0*> = 1 & or3b . <*1,0,1*> = 1 & or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )
proof
thus or3b . <*0,0,0*> = (TRUE 'or' ('not' FALSE)) 'or' FALSE by Def26
.= 1 ; ::_thesis: ( 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 )
thus or3b . <*0,0,1*> = (('not' FALSE) 'or' ('not' FALSE)) 'or' TRUE by Def26
.= 1 ; ::_thesis: ( 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 )
thus or3b . <*0,1,0*> = ('not' FALSE) 'or' ('not' TRUE) by Def26
.= 1 ; ::_thesis: ( 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 )
thus or3b . <*0,1,1*> = (('not' FALSE) 'or' ('not' TRUE)) 'or' TRUE by Def26
.= 1 ; ::_thesis: ( or3b . <*1,0,0*> = 1 & or3b . <*1,0,1*> = 1 & or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )
thus or3b . <*1,0,0*> = ('not' TRUE) 'or' ('not' FALSE) by Def26
.= 1 ; ::_thesis: ( or3b . <*1,0,1*> = 1 & or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )
thus or3b . <*1,0,1*> = (('not' TRUE) 'or' ('not' FALSE)) 'or' TRUE by Def26
.= 1 ; ::_thesis: ( or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )
thus or3b . <*1,1,0*> = ('not' TRUE) 'or' ('not' TRUE) by Def26
.= 0 ; ::_thesis: or3b . <*1,1,1*> = 1
thus or3b . <*1,1,1*> = (('not' TRUE) 'or' ('not' TRUE)) 'or' TRUE by Def26
.= 1 ; ::_thesis: verum
end;

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 )
proof
thus or3c . <*0,0,0*> = (('not' FALSE) 'or' ('not' FALSE)) 'or' TRUE by Def27
.= 1 ; ::_thesis: ( 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 )
thus or3c . <*0,0,1*> = (('not' FALSE) 'or' ('not' FALSE)) 'or' FALSE by Def27
.= 1 ; ::_thesis: ( 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 )
thus or3c . <*0,1,0*> = (('not' FALSE) 'or' ('not' TRUE)) 'or' TRUE by Def27
.= 1 ; ::_thesis: ( 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 )
thus or3c . <*0,1,1*> = (TRUE 'or' ('not' TRUE)) 'or' ('not' TRUE) by Def27
.= 1 ; ::_thesis: ( or3c . <*1,0,0*> = 1 & or3c . <*1,0,1*> = 1 & or3c . <*1,1,0*> = 1 & or3c . <*1,1,1*> = 0 )
thus or3c . <*1,0,0*> = (('not' TRUE) 'or' ('not' FALSE)) 'or' TRUE by Def27
.= 1 ; ::_thesis: ( or3c . <*1,0,1*> = 1 & or3c . <*1,1,0*> = 1 & or3c . <*1,1,1*> = 0 )
thus or3c . <*1,0,1*> = (('not' TRUE) 'or' TRUE) 'or' ('not' TRUE) by Def27
.= 1 ; ::_thesis: ( or3c . <*1,1,0*> = 1 & or3c . <*1,1,1*> = 0 )
thus or3c . <*1,1,0*> = (('not' TRUE) 'or' ('not' TRUE)) 'or' TRUE by Def27
.= 1 ; ::_thesis: or3c . <*1,1,1*> = 0
thus or3c . <*1,1,1*> = (FALSE 'or' ('not' TRUE)) 'or' ('not' TRUE) by Def27
.= 0 ; ::_thesis: verum
end;

theorem :: TWOSCOMP:26
( xor3 . <*0,0,0*> = 0 & xor3 . <*0,0,1*> = 1 & xor3 . <*0,1,0*> = 1 & xor3 . <*0,1,1*> = 0 & xor3 . <*1,0,0*> = 1 & xor3 . <*1,0,1*> = 0 & xor3 . <*1,1,0*> = 0 & xor3 . <*1,1,1*> = 1 )
proof
thus xor3 . <*0,0,0*> = FALSE 'xor' FALSE by Def32
.= 0 ; ::_thesis: ( 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 )
thus xor3 . <*0,0,1*> = (FALSE 'xor' FALSE) 'xor' TRUE by Def32
.= 1 ; ::_thesis: ( 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 )
thus  xor3 . <*0,1,0*> = 1 by Def32, BINARITH:13; ::_thesis: ( 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 )
thus xor3 . <*0,1,1*> = TRUE 'xor' TRUE by Def32, BINARITH:13
.= 0 ; ::_thesis: ( xor3 . <*1,0,0*> = 1 & xor3 . <*1,0,1*> = 0 & xor3 . <*1,1,0*> = 0 & xor3 . <*1,1,1*> = 1 )
thus  xor3 . <*1,0,0*> = 1 by Def32, BINARITH:13; ::_thesis: ( xor3 . <*1,0,1*> = 0 & xor3 . <*1,1,0*> = 0 & xor3 . <*1,1,1*> = 1 )
thus xor3 . <*1,0,1*> = TRUE 'xor' TRUE by Def32, BINARITH:13
.= 0 ; ::_thesis: ( xor3 . <*1,1,0*> = 0 & xor3 . <*1,1,1*> = 1 )
thus xor3 . <*1,1,0*> = (TRUE 'xor' TRUE) 'xor' FALSE by Def32
.= 0 ; ::_thesis: xor3 . <*1,1,1*> = 1
thus xor3 . <*1,1,1*> = (TRUE 'xor' TRUE) 'xor' TRUE by Def32
.= 1 ; ::_thesis: verum
end;

begin

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];

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];

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]}
proof
let x, b be non pair set ; ::_thesis: the carrier of (CompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a]}
set p = <*x,b*>;
 rng <*x,b*> = {x,b} by FINSEQ_2:127;
hence  the carrier of (CompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a]} by CIRCCOMB:def_6; ::_thesis: verum
end;

theorem :: TWOSCOMP:28
for x, b being non pair set holds [<*x,b*>,xor2a] in InnerVertices (CompStr (x,b))
proof
let x, b be non pair set ; ::_thesis: [<*x,b*>,xor2a] in InnerVertices (CompStr (x,b))
 InnerVertices (CompStr (x,b)) = {[<*x,b*>,xor2a]} by CIRCCOMB:42;
hence  [<*x,b*>,xor2a] in InnerVertices (CompStr (x,b)) by TARSKI:def_1; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: ( x in InputVertices (CompStr (x,b)) & b in InputVertices (CompStr (x,b)) )
 InputVertices (CompStr (x,b)) = {x,b} by FACIRC_1:40;
hence  ( x in InputVertices (CompStr (x,b)) & b in InputVertices (CompStr (x,b)) ) by TARSKI:def_2; ::_thesis: verum
end;

theorem :: TWOSCOMP:30
for x, b being non pair set holds InputVertices (CompStr (x,b)) is without_pairs
proof
let x, b be non pair set ; ::_thesis: InputVertices (CompStr (x,b)) is without_pairs
 InputVertices (CompStr (x,b)) = {x,b} by FACIRC_1:40;
hence  InputVertices (CompStr (x,b)) is without_pairs ; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: the carrier of (IncrementStr (x,b)) = {x,b} \/ {[<*x,b*>,and2a]}
set p = <*x,b*>;
 rng <*x,b*> = {x,b} by FINSEQ_2:127;
hence  the carrier of (IncrementStr (x,b)) = {x,b} \/ {[<*x,b*>,and2a]} by CIRCCOMB:def_6; ::_thesis: verum
end;

theorem :: TWOSCOMP:32
for x, b being non pair set holds [<*x,b*>,and2a] in InnerVertices (IncrementStr (x,b))
proof
let x, b be non pair set ; ::_thesis: [<*x,b*>,and2a] in InnerVertices (IncrementStr (x,b))
 InnerVertices (IncrementStr (x,b)) = {[<*x,b*>,and2a]} by CIRCCOMB:42;
hence  [<*x,b*>,and2a] in InnerVertices (IncrementStr (x,b)) by TARSKI:def_1; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: ( x in InputVertices (IncrementStr (x,b)) & b in InputVertices (IncrementStr (x,b)) )
 InputVertices (IncrementStr (x,b)) = {x,b} by FACIRC_1:40;
hence  ( x in InputVertices (IncrementStr (x,b)) & b in InputVertices (IncrementStr (x,b)) ) by TARSKI:def_2; ::_thesis: verum
end;

theorem :: TWOSCOMP:34
for x, b being non pair set holds InputVertices (IncrementStr (x,b)) is without_pairs
proof
let x, b be non pair set ; ::_thesis: InputVertices (IncrementStr (x,b)) is without_pairs
 InputVertices (IncrementStr (x,b)) = {x,b} by FACIRC_1:40;
hence  InputVertices (IncrementStr (x,b)) is without_pairs ; ::_thesis: verum
end;

theorem :: TWOSCOMP:35
for x, b being non pair set holds InnerVertices (BitCompStr (x,b)) is Relation
proof
let x, b be non pair set ; ::_thesis: InnerVertices (BitCompStr (x,b)) is Relation
set S1 = CompStr (x,b);
set S2 = IncrementStr (x,b);
 ( InnerVertices (CompStr (x,b)) is Relation & InnerVertices (IncrementStr (x,b)) is Relation ) by FACIRC_1:38;
hence  InnerVertices (BitCompStr (x,b)) is Relation by FACIRC_1:3; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: ( 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)) )
set p = <*x,b*>;
set S1 = CompStr (x,b);
set S2 = IncrementStr (x,b);
A1: ( [<*x,b*>,xor2a] in the carrier of (CompStr (x,b)) & [<*x,b*>,and2a] in the carrier of (IncrementStr (x,b)) ) by FACIRC_1:43;
 ( x in the carrier of (CompStr (x,b)) & b in the carrier of (CompStr (x,b)) ) by FACIRC_1:43;
hence  ( 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)) ) by A1, FACIRC_1:20; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: the carrier of (BitCompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
set p = <*x,b*>;
set S1 = CompStr (x,b);
set S2 = IncrementStr (x,b);
 ( the carrier of (CompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a]} & the carrier of (IncrementStr (x,b)) = {x,b} \/ {[<*x,b*>,and2a]} ) by Th27, Th31;
then  the carrier of (BitCompStr (x,b)) = ({x,b} \/ {[<*x,b*>,xor2a]}) \/ ({x,b} \/ {[<*x,b*>,and2a]}) by CIRCCOMB:def_2
.= ({x,b} \/ ({x,b} \/ {[<*x,b*>,xor2a]})) \/ {[<*x,b*>,and2a]} by XBOOLE_1:4
.= (({x,b} \/ {x,b}) \/ {[<*x,b*>,xor2a]}) \/ {[<*x,b*>,and2a]} by XBOOLE_1:4
.= {x,b} \/ ({[<*x,b*>,xor2a]} \/ {[<*x,b*>,and2a]}) by XBOOLE_1:4
.= {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]} by ENUMSET1:1 ;
hence  the carrier of (BitCompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]} ; ::_thesis: verum
end;

theorem Th38: :: TWOSCOMP:38
for x, b being non pair set holds InnerVertices (BitCompStr (x,b)) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
proof
let x, b be non pair set ; ::_thesis: InnerVertices (BitCompStr (x,b)) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]}
set p = <*x,b*>;
set S1 = CompStr (x,b);
set S2 = IncrementStr (x,b);
set S = BitCompStr (x,b);
A1: ( InnerVertices (CompStr (x,b)) = {[<*x,b*>,xor2a]} & InnerVertices (IncrementStr (x,b)) = {[<*x,b*>,and2a]} ) by CIRCCOMB:42;
InnerVertices (BitCompStr (x,b)) = (InnerVertices (CompStr (x,b))) \/ (InnerVertices (IncrementStr (x,b))) by FACIRC_1:27
.= {[<*x,b*>,xor2a],[<*x,b*>,and2a]} by A1, ENUMSET1:1 ;
hence  InnerVertices (BitCompStr (x,b)) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]} ; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: ( [<*x,b*>,xor2a] in InnerVertices (BitCompStr (x,b)) & [<*x,b*>,and2a] in InnerVertices (BitCompStr (x,b)) )
 InnerVertices (BitCompStr (x,b)) = {[<*x,b*>,xor2a],[<*x,b*>,and2a]} by Th38;
hence  ( [<*x,b*>,xor2a] in InnerVertices (BitCompStr (x,b)) & [<*x,b*>,and2a] in InnerVertices (BitCompStr (x,b)) ) by TARSKI:def_2; ::_thesis: verum
end;

theorem Th40: :: TWOSCOMP:40
for x, b being non pair set holds InputVertices (BitCompStr (x,b)) = {x,b}
proof
let x, b be non pair set ; ::_thesis: InputVertices (BitCompStr (x,b)) = {x,b}
set S1 = CompStr (x,b);
set S2 = IncrementStr (x,b);
set S = BitCompStr (x,b);
A1: ( InputVertices (CompStr (x,b)) = {x,b} & InputVertices (IncrementStr (x,b)) = {x,b} ) by FACIRC_1:40;
 ( InnerVertices (CompStr (x,b)) is Relation & InnerVertices (IncrementStr (x,b)) is Relation ) by FACIRC_1:38;
then  InputVertices (BitCompStr (x,b)) = {x,b} \/ {x,b} by A1, FACIRC_1:7
.= {x,b} ;
hence  InputVertices (BitCompStr (x,b)) = {x,b} ; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: ( x in InputVertices (BitCompStr (x,b)) & b in InputVertices (BitCompStr (x,b)) )
 InputVertices (BitCompStr (x,b)) = {x,b} by Th40;
hence  ( x in InputVertices (BitCompStr (x,b)) & b in InputVertices (BitCompStr (x,b)) ) by TARSKI:def_2; ::_thesis: verum
end;

theorem :: TWOSCOMP:42
for x, b being non pair set holds InputVertices (BitCompStr (x,b)) is without_pairs
proof
let x, b be non pair set ; ::_thesis: InputVertices (BitCompStr (x,b)) is without_pairs
 InputVertices (BitCompStr (x,b)) = {x,b} by Th40;
hence  InputVertices (BitCompStr (x,b)) is without_pairs ; ::_thesis: verum
end;

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
let x, b be non pair set ; ::_thesis: 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 )
let s be State of (CompCirc (x,b)); ::_thesis: ( (Following s) . (CompOutput (x,b)) = xor2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )
set p = <*x,b*>;
set S = CompStr (x,b);
A1: ( dom s = the carrier of (CompStr (x,b)) & x in the carrier of (CompStr (x,b)) ) by CIRCUIT1:3, FACIRC_1:43;
A2: b in the carrier of (CompStr (x,b)) by FACIRC_1:43;
 InnerVertices (CompStr (x,b)) = the carrier' of (CompStr (x,b)) by FACIRC_1:37;
hence (Following s) . (CompOutput (x,b)) = xor2a . (s * <*x,b*>) by FACIRC_1:35
.= xor2a . <*(s . x),(s . b)*> by A1, A2, FINSEQ_2:125 ;
::_thesis: ( (Following s) . x = s . x & (Following s) . b = s . b )
 InputVertices (CompStr (x,b)) = {x,b} by FACIRC_1:40;
then  ( x in InputVertices (CompStr (x,b)) & b in InputVertices (CompStr (x,b)) ) by TARSKI:def_2;
hence  ( (Following s) . x = s . x & (Following s) . b = s . b ) by CIRCUIT2:def_5; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: 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 )
let s be State of (CompCirc (x,b)); ::_thesis: 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 )
let a1, a2 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . b implies ( (Following s) . (CompOutput (x,b)) = ('not' a1) 'xor' a2 & (Following s) . x = a1 & (Following s) . b = a2 ) )
assume A1: ( a1 = s . x & a2 = s . b ) ; ::_thesis: ( (Following s) . (CompOutput (x,b)) = ('not' a1) 'xor' a2 & (Following s) . x = a1 & (Following s) . b = a2 )
thus (Following s) . (CompOutput (x,b)) = xor2a . <*(s . x),(s . b)*> by Th43
.= ('not' a1) 'xor' a2 by A1, Def14 ; ::_thesis: ( (Following s) . x = a1 & (Following s) . b = a2 )
thus  ( (Following s) . x = a1 & (Following s) . b = a2 ) by A1, Th43; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: 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 )
let s be State of (BitCompCirc (x,b)); ::_thesis: ( (Following s) . (CompOutput (x,b)) = xor2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )
set p = <*x,b*>;
set S = BitCompStr (x,b);
A1: ( dom s = the carrier of (BitCompStr (x,b)) & x in the carrier of (BitCompStr (x,b)) ) by Th36, CIRCUIT1:3;
A2: b in the carrier of (BitCompStr (x,b)) by Th36;
 InnerVertices (BitCompStr (x,b)) = the carrier' of (BitCompStr (x,b)) by FACIRC_1:37;
hence (Following s) . (CompOutput (x,b)) = xor2a . (s * <*x,b*>) by Th39, FACIRC_1:35
.= xor2a . <*(s . x),(s . b)*> by A1, A2, FINSEQ_2:125 ;
::_thesis: ( (Following s) . x = s . x & (Following s) . b = s . b )
 ( x in InputVertices (BitCompStr (x,b)) & b in InputVertices (BitCompStr (x,b)) ) by Th41;
hence  ( (Following s) . x = s . x & (Following s) . b = s . b ) by CIRCUIT2:def_5; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: 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 )
let s be State of (BitCompCirc (x,b)); ::_thesis: 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 )
let a1, a2 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . b implies ( (Following s) . (CompOutput (x,b)) = ('not' a1) 'xor' a2 & (Following s) . x = a1 & (Following s) . b = a2 ) )
assume A1: ( a1 = s . x & a2 = s . b ) ; ::_thesis: ( (Following s) . (CompOutput (x,b)) = ('not' a1) 'xor' a2 & (Following s) . x = a1 & (Following s) . b = a2 )
thus (Following s) . (CompOutput (x,b)) = xor2a . <*(s . x),(s . b)*> by Th45
.= ('not' a1) 'xor' a2 by A1, Def14 ; ::_thesis: ( (Following s) . x = a1 & (Following s) . b = a2 )
thus  ( (Following s) . x = a1 & (Following s) . b = a2 ) by A1, Th45; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: 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 )
let s be State of (IncrementCirc (x,b)); ::_thesis: ( (Following s) . (IncrementOutput (x,b)) = and2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )
set p = <*x,b*>;
set S = IncrementStr (x,b);
A1: ( dom s = the carrier of (IncrementStr (x,b)) & x in the carrier of (IncrementStr (x,b)) ) by CIRCUIT1:3, FACIRC_1:43;
A2: b in the carrier of (IncrementStr (x,b)) by FACIRC_1:43;
 InnerVertices (IncrementStr (x,b)) = the carrier' of (IncrementStr (x,b)) by FACIRC_1:37;
hence (Following s) . (IncrementOutput (x,b)) = and2a . (s * <*x,b*>) by FACIRC_1:35
.= and2a . <*(s . x),(s . b)*> by A1, A2, FINSEQ_2:125 ;
::_thesis: ( (Following s) . x = s . x & (Following s) . b = s . b )
 InputVertices (IncrementStr (x,b)) = {x,b} by FACIRC_1:40;
then  ( x in InputVertices (IncrementStr (x,b)) & b in InputVertices (IncrementStr (x,b)) ) by TARSKI:def_2;
hence  ( (Following s) . x = s . x & (Following s) . b = s . b ) by CIRCUIT2:def_5; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: 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 )
let s be State of (IncrementCirc (x,b)); ::_thesis: 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 )
let a1, a2 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . b implies ( (Following s) . (IncrementOutput (x,b)) = ('not' a1) '&' a2 & (Following s) . x = a1 & (Following s) . b = a2 ) )
assume A1: ( a1 = s . x & a2 = s . b ) ; ::_thesis: ( (Following s) . (IncrementOutput (x,b)) = ('not' a1) '&' a2 & (Following s) . x = a1 & (Following s) . b = a2 )
thus (Following s) . (IncrementOutput (x,b)) = and2a . <*(s . x),(s . b)*> by Th47
.= ('not' a1) '&' a2 by A1, Def2 ; ::_thesis: ( (Following s) . x = a1 & (Following s) . b = a2 )
thus  ( (Following s) . x = a1 & (Following s) . b = a2 ) by A1, Th47; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: 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 )
let s be State of (BitCompCirc (x,b)); ::_thesis: ( (Following s) . (IncrementOutput (x,b)) = and2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )
set p = <*x,b*>;
set S = BitCompStr (x,b);
A1: ( dom s = the carrier of (BitCompStr (x,b)) & x in the carrier of (BitCompStr (x,b)) ) by Th36, CIRCUIT1:3;
A2: b in the carrier of (BitCompStr (x,b)) by Th36;
 InnerVertices (BitCompStr (x,b)) = the carrier' of (BitCompStr (x,b)) by FACIRC_1:37;
hence (Following s) . (IncrementOutput (x,b)) = and2a . (s * <*x,b*>) by Th39, FACIRC_1:35
.= and2a . <*(s . x),(s . b)*> by A1, A2, FINSEQ_2:125 ;
::_thesis: ( (Following s) . x = s . x & (Following s) . b = s . b )
 InputVertices (BitCompStr (x,b)) = {x,b} by Th40;
then  ( x in InputVertices (BitCompStr (x,b)) & b in InputVertices (BitCompStr (x,b)) ) by TARSKI:def_2;
hence  ( (Following s) . x = s . x & (Following s) . b = s . b ) by CIRCUIT2:def_5; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: 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 )
let s be State of (BitCompCirc (x,b)); ::_thesis: 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 )
let a1, a2 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . b implies ( (Following s) . (IncrementOutput (x,b)) = ('not' a1) '&' a2 & (Following s) . x = a1 & (Following s) . b = a2 ) )
assume A1: ( a1 = s . x & a2 = s . b ) ; ::_thesis: ( (Following s) . (IncrementOutput (x,b)) = ('not' a1) '&' a2 & (Following s) . x = a1 & (Following s) . b = a2 )
thus (Following s) . (IncrementOutput (x,b)) = and2a . <*(s . x),(s . b)*> by Th49
.= ('not' a1) '&' a2 by A1, Def2 ; ::_thesis: ( (Following s) . x = a1 & (Following s) . b = a2 )
thus  ( (Following s) . x = a1 & (Following s) . b = a2 ) by A1, Th49; ::_thesis: verum
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
let x, b be non pair set ; ::_thesis: for s being State of (BitCompCirc (x,b)) holds Following s is stable
set p = <*x,b*>;
set S = BitCompStr (x,b);
let s be State of (BitCompCirc (x,b)); ::_thesis: Following s is stable
set s1 = Following s;
set s2 = Following (Following s);
A1: the carrier of (BitCompStr (x,b)) = {x,b} \/ {[<*x,b*>,xor2a],[<*x,b*>,and2a]} by Th37;
A2: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(BitCompStr_(x,b))_holds_
(Following_(Following_s))_._a_=_(Following_s)_._a
let a be set ; ::_thesis: ( a in the carrier of (BitCompStr (x,b)) implies (Following (Following s)) . a = (Following s) . a )
A3: (Following s) . [<*x,b*>,xor2a] = (Following s) . (CompOutput (x,b))
.= xor2a . <*(s . x),(s . b)*> by Th45 ;
assume  a in the carrier of (BitCompStr (x,b)) ; ::_thesis: (Following (Following s)) . a = (Following s) . a
then  ( a in {x,b} or a in {[<*x,b*>,xor2a],[<*x,b*>,and2a]} ) by A1, XBOOLE_0:def_3;
then A4: ( a = x or a = b or a = [<*x,b*>,xor2a] or a = [<*x,b*>,and2a] ) by TARSKI:def_2;
A5: (Following (Following s)) . [<*x,b*>,and2a] = (Following (Following s)) . (IncrementOutput (x,b))
.= and2a . <*((Following s) . x),((Following s) . b)*> by Th49 ;
A6: (Following (Following s)) . [<*x,b*>,xor2a] = (Following (Following s)) . (CompOutput (x,b))
.= xor2a . <*((Following s) . x),((Following s) . b)*> by Th45 ;
A7: (Following s) . [<*x,b*>,and2a] = (Following s) . (IncrementOutput (x,b))
.= and2a . <*(s . x),(s . b)*> by Th49 ;
 (Following s) . x = s . x by Th45;
hence  (Following (Following s)) . a = (Following s) . a by A4, A3, A7, A6, A5, Th45; ::_thesis: verum
end;
 ( dom (Following s) = the carrier of (BitCompStr (x,b)) & dom (Following (Following s)) = the carrier of (BitCompStr (x,b)) ) by CIRCUIT1:3;
hence  Following s = Following (Following s) by A2, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;