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