:: TWOSCOMP semantic presentation

definition

let c₁ be non empty non void unsplit ManySortedSign ;
let c₂ be Boolean Circuit of c₁;
let c₃ be State of c₂;
let c₄ be Vertex of c₁;
redefine func . as c₃ . c₄ -> Element of BOOLEAN ;
coherence

proof end;

end;

deffunc H₁( Element of BOOLEAN , Element of BOOLEAN ) -> Element of BOOLEAN = a₁ '&' a₂;

definition

func and2 -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def1: :: TWOSCOMP:def 1
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = b₁ '&' b₂;
existence

proof end;

uniqueness

proof end;

func and2a -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def2: :: TWOSCOMP:def 2
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = ('not' b₁) '&' b₂;
existence

proof end;

uniqueness

proof end;

func and2b -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def3: :: TWOSCOMP:def 3
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = ('not' b₁) '&' ('not' b₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines and2 TWOSCOMP:def 1 :

:: deftheorem Def2 defines and2a TWOSCOMP:def 2 :

:: deftheorem Def3 defines and2b TWOSCOMP:def 3 :

definition

func nand2 -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def4: :: TWOSCOMP:def 4
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = 'not' (b₁ '&' b₂);
existence

proof end;

uniqueness

proof end;

func nand2a -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def5: :: TWOSCOMP:def 5
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = 'not' (('not' b₁) '&' b₂);
existence

proof end;

uniqueness

proof end;

func nand2b -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def6: :: TWOSCOMP:def 6
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = 'not' (('not' b₁) '&' ('not' b₂));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines nand2 TWOSCOMP:def 4 :

:: deftheorem Def5 defines nand2a TWOSCOMP:def 5 :

:: deftheorem Def6 defines nand2b TWOSCOMP:def 6 :

definition

func or2 -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def7: :: TWOSCOMP:def 7
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = b₁ 'or' b₂;
existence

proof end;

uniqueness

proof end;

func or2a -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def8: :: TWOSCOMP:def 8
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = ('not' b₁) 'or' b₂;
existence

proof end;

uniqueness

proof end;

func or2b -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def9: :: TWOSCOMP:def 9
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = ('not' b₁) 'or' ('not' b₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines or2 TWOSCOMP:def 7 :

:: deftheorem Def8 defines or2a TWOSCOMP:def 8 :

:: deftheorem Def9 defines or2b TWOSCOMP:def 9 :

definition

func nor2 -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def10: :: TWOSCOMP:def 10
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = 'not' (b₁ 'or' b₂);
existence

proof end;

uniqueness

proof end;

func nor2a -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def11: :: TWOSCOMP:def 11
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = 'not' (('not' b₁) 'or' b₂);
existence

proof end;

uniqueness

proof end;

func nor2b -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def12: :: TWOSCOMP:def 12
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = 'not' (('not' b₁) 'or' ('not' b₂));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines nor2 TWOSCOMP:def 10 :

:: deftheorem Def11 defines nor2a TWOSCOMP:def 11 :

:: deftheorem Def12 defines nor2b TWOSCOMP:def 12 :

definition

func xor2 -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def13: :: TWOSCOMP:def 13
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = b₁ 'xor' b₂;
existence

proof end;

uniqueness

proof end;

func xor2a -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def14: :: TWOSCOMP:def 14
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = ('not' b₁) 'xor' b₂;
existence

proof end;

uniqueness

proof end;

func xor2b -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def15: :: TWOSCOMP:def 15
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = ('not' b₁) 'xor' ('not' b₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines xor2 TWOSCOMP:def 13 :

:: deftheorem Def14 defines xor2a TWOSCOMP:def 14 :

:: deftheorem Def15 defines xor2b TWOSCOMP:def 15 :

theorem Th1: :: TWOSCOMP:1

canceled;

theorem Th2: :: TWOSCOMP:2

canceled;

theorem Th3: :: TWOSCOMP:3

for b₁, b₂ being Element of BOOLEAN holds
( and2 . <*b₁,b₂*> = b₁ '&' b₂ & and2a . <*b₁,b₂*> = ('not' b₁) '&' b₂ & and2b . <*b₁,b₂*> = ('not' b₁) '&' ('not' b₂) ) by Def1, Def2, Def3;

theorem Th4: :: TWOSCOMP:4

for b₁, b₂ being Element of BOOLEAN holds
( nand2 . <*b₁,b₂*> = 'not' (b₁ '&' b₂) & nand2a . <*b₁,b₂*> = 'not' (('not' b₁) '&' b₂) & nand2b . <*b₁,b₂*> = 'not' (('not' b₁) '&' ('not' b₂)) ) by Def4, Def5, Def6;

theorem Th5: :: TWOSCOMP:5

for b₁, b₂ being Element of BOOLEAN holds
( or2 . <*b₁,b₂*> = b₁ 'or' b₂ & or2a . <*b₁,b₂*> = ('not' b₁) 'or' b₂ & or2b . <*b₁,b₂*> = ('not' b₁) 'or' ('not' b₂) ) by Def7, Def8, Def9;

theorem Th6: :: TWOSCOMP:6

for b₁, b₂ being Element of BOOLEAN holds
( nor2 . <*b₁,b₂*> = 'not' (b₁ 'or' b₂) & nor2a . <*b₁,b₂*> = 'not' (('not' b₁) 'or' b₂) & nor2b . <*b₁,b₂*> = 'not' (('not' b₁) 'or' ('not' b₂)) ) by Def10, Def11, Def12;

theorem Th7: :: TWOSCOMP:7

for b₁, b₂ being Element of BOOLEAN holds
( xor2 . <*b₁,b₂*> = b₁ 'xor' b₂ & xor2a . <*b₁,b₂*> = ('not' b₁) 'xor' b₂ & xor2b . <*b₁,b₂*> = ('not' b₁) 'xor' ('not' b₂) ) by Def13, Def14, Def15;

theorem Th8: :: TWOSCOMP:8

for b₁, b₂ being Element of BOOLEAN holds
( and2 . <*b₁,b₂*> = nor2b . <*b₁,b₂*> & and2a . <*b₁,b₂*> = nor2a . <*b₂,b₁*> & and2b . <*b₁,b₂*> = nor2 . <*b₁,b₂*> )

proof end;

theorem Th9: :: TWOSCOMP:9

for b₁, b₂ being Element of BOOLEAN holds
( or2 . <*b₁,b₂*> = nand2b . <*b₁,b₂*> & or2a . <*b₁,b₂*> = nand2a . <*b₂,b₁*> & or2b . <*b₁,b₂*> = nand2 . <*b₁,b₂*> )

proof end;

theorem Th10: :: TWOSCOMP:10

for b₁, b₂ being Element of BOOLEAN holds xor2b . <*b₁,b₂*> = xor2 . <*b₁,b₂*>

proof end;

theorem Th11: :: TWOSCOMP:11

( and2 . <*0,0*> = 0 & and2 . <*0,1*> = 0 & and2 . <*1,0*> = 0 & and2 . <*1,1*> = 1 & and2a . <*0,0*> = 0 & and2a . <*0,1*> = 1 & and2a . <*1,0*> = 0 & and2a . <*1,1*> = 0 & and2b . <*0,0*> = 1 & and2b . <*0,1*> = 0 & and2b . <*1,0*> = 0 & and2b . <*1,1*> = 0 )

proof end;

theorem Th12: :: TWOSCOMP:12

( or2 . <*0,0*> = 0 & or2 . <*0,1*> = 1 & or2 . <*1,0*> = 1 & or2 . <*1,1*> = 1 & or2a . <*0,0*> = 1 & or2a . <*0,1*> = 1 & or2a . <*1,0*> = 0 & or2a . <*1,1*> = 1 & or2b . <*0,0*> = 1 & or2b . <*0,1*> = 1 & or2b . <*1,0*> = 1 & or2b . <*1,1*> = 0 )

proof end;

theorem Th13: :: TWOSCOMP:13

( xor2 . <*0,0*> = 0 & xor2 . <*0,1*> = 1 & xor2 . <*1,0*> = 1 & xor2 . <*1,1*> = 0 & xor2a . <*0,0*> = 1 & xor2a . <*0,1*> = 0 & xor2a . <*1,0*> = 0 & xor2a . <*1,1*> = 1 )

proof end;

definition

func and3 -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def16: :: TWOSCOMP:def 16
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = (b₁ '&' b₂) '&' b₃;
existence

proof end;

uniqueness

proof end;

func and3a -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def17: :: TWOSCOMP:def 17
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = (('not' b₁) '&' b₂) '&' b₃;
existence

proof end;

uniqueness

proof end;

func and3b -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def18: :: TWOSCOMP:def 18
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = (('not' b₁) '&' ('not' b₂)) '&' b₃;
existence

proof end;

uniqueness

proof end;

func and3c -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def19: :: TWOSCOMP:def 19
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = (('not' b₁) '&' ('not' b₂)) '&' ('not' b₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines and3 TWOSCOMP:def 16 :

:: deftheorem Def17 defines and3a TWOSCOMP:def 17 :

:: deftheorem Def18 defines and3b TWOSCOMP:def 18 :

:: deftheorem Def19 defines and3c TWOSCOMP:def 19 :

definition

func nand3 -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def20: :: TWOSCOMP:def 20
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = 'not' ((b₁ '&' b₂) '&' b₃);
existence

proof end;

uniqueness

proof end;

func nand3a -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def21: :: TWOSCOMP:def 21
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) '&' b₂) '&' b₃);
existence

proof end;

uniqueness

proof end;

func nand3b -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def22: :: TWOSCOMP:def 22
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) '&' ('not' b₂)) '&' b₃);
existence

proof end;

uniqueness

proof end;

func nand3c -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def23: :: TWOSCOMP:def 23
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) '&' ('not' b₂)) '&' ('not' b₃));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines nand3 TWOSCOMP:def 20 :

:: deftheorem Def21 defines nand3a TWOSCOMP:def 21 :

:: deftheorem Def22 defines nand3b TWOSCOMP:def 22 :

:: deftheorem Def23 defines nand3c TWOSCOMP:def 23 :

definition

func or3 -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def24: :: TWOSCOMP:def 24
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = (b₁ 'or' b₂) 'or' b₃;
existence

proof end;

uniqueness

proof end;

func or3a -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def25: :: TWOSCOMP:def 25
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = (('not' b₁) 'or' b₂) 'or' b₃;
existence

proof end;

uniqueness

proof end;

func or3b -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def26: :: TWOSCOMP:def 26
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = (('not' b₁) 'or' ('not' b₂)) 'or' b₃;
existence

proof end;

uniqueness

proof end;

func or3c -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def27: :: TWOSCOMP:def 27
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = (('not' b₁) 'or' ('not' b₂)) 'or' ('not' b₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines or3 TWOSCOMP:def 24 :

:: deftheorem Def25 defines or3a TWOSCOMP:def 25 :

:: deftheorem Def26 defines or3b TWOSCOMP:def 26 :

:: deftheorem Def27 defines or3c TWOSCOMP:def 27 :

definition

func nor3 -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def28: :: TWOSCOMP:def 28
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = 'not' ((b₁ 'or' b₂) 'or' b₃);
existence

proof end;

uniqueness

proof end;

func nor3a -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def29: :: TWOSCOMP:def 29
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) 'or' b₂) 'or' b₃);
existence

proof end;

uniqueness

proof end;

func nor3b -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def30: :: TWOSCOMP:def 30
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) 'or' ('not' b₂)) 'or' b₃);
existence

proof end;

uniqueness

proof end;

func nor3c -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def31: :: TWOSCOMP:def 31
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) 'or' ('not' b₂)) 'or' ('not' b₃));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def28 defines nor3 TWOSCOMP:def 28 :

:: deftheorem Def29 defines nor3a TWOSCOMP:def 29 :

:: deftheorem Def30 defines nor3b TWOSCOMP:def 30 :

:: deftheorem Def31 defines nor3c TWOSCOMP:def 31 :

definition

func xor3 -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def32: :: TWOSCOMP:def 32
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = (b₁ 'xor' b₂) 'xor' b₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def32 defines xor3 TWOSCOMP:def 32 :

theorem Th14: :: TWOSCOMP:14

for b₁, b₂, b₃ being Element of BOOLEAN holds
( and3 . <*b₁,b₂,b₃*> = (b₁ '&' b₂) '&' b₃ & and3a . <*b₁,b₂,b₃*> = (('not' b₁) '&' b₂) '&' b₃ & and3b . <*b₁,b₂,b₃*> = (('not' b₁) '&' ('not' b₂)) '&' b₃ & and3c . <*b₁,b₂,b₃*> = (('not' b₁) '&' ('not' b₂)) '&' ('not' b₃) ) by Def16, Def17, Def18, Def19;

theorem Th15: :: TWOSCOMP:15

for b₁, b₂, b₃ being Element of BOOLEAN holds
( nand3 . <*b₁,b₂,b₃*> = 'not' ((b₁ '&' b₂) '&' b₃) & nand3a . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) '&' b₂) '&' b₃) & nand3b . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) '&' ('not' b₂)) '&' b₃) & nand3c . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) '&' ('not' b₂)) '&' ('not' b₃)) ) by Def20, Def21, Def22, Def23;

theorem Th16: :: TWOSCOMP:16

for b₁, b₂, b₃ being Element of BOOLEAN holds
( or3 . <*b₁,b₂,b₃*> = (b₁ 'or' b₂) 'or' b₃ & or3a . <*b₁,b₂,b₃*> = (('not' b₁) 'or' b₂) 'or' b₃ & or3b . <*b₁,b₂,b₃*> = (('not' b₁) 'or' ('not' b₂)) 'or' b₃ & or3c . <*b₁,b₂,b₃*> = (('not' b₁) 'or' ('not' b₂)) 'or' ('not' b₃) ) by Def24, Def25, Def26, Def27;

theorem Th17: :: TWOSCOMP:17

for b₁, b₂, b₃ being Element of BOOLEAN holds
( nor3 . <*b₁,b₂,b₃*> = 'not' ((b₁ 'or' b₂) 'or' b₃) & nor3a . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) 'or' b₂) 'or' b₃) & nor3b . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) 'or' ('not' b₂)) 'or' b₃) & nor3c . <*b₁,b₂,b₃*> = 'not' ((('not' b₁) 'or' ('not' b₂)) 'or' ('not' b₃)) ) by Def28, Def29, Def30, Def31;

theorem Th18: :: TWOSCOMP:18

canceled;

theorem Th19: :: TWOSCOMP:19

for b₁, b₂, b₃ being Element of BOOLEAN holds
( and3 . <*b₁,b₂,b₃*> = nor3c . <*b₁,b₂,b₃*> & and3a . <*b₁,b₂,b₃*> = nor3b . <*b₃,b₂,b₁*> & and3b . <*b₁,b₂,b₃*> = nor3a . <*b₃,b₂,b₁*> & and3c . <*b₁,b₂,b₃*> = nor3 . <*b₁,b₂,b₃*> )

proof end;

theorem Th20: :: TWOSCOMP:20

for b₁, b₂, b₃ being Element of BOOLEAN holds
( or3 . <*b₁,b₂,b₃*> = nand3c . <*b₁,b₂,b₃*> & or3a . <*b₁,b₂,b₃*> = nand3b . <*b₃,b₂,b₁*> & or3b . <*b₁,b₂,b₃*> = nand3a . <*b₃,b₂,b₁*> & or3c . <*b₁,b₂,b₃*> = nand3 . <*b₁,b₂,b₃*> )

proof end;

theorem Th21: :: TWOSCOMP:21

( and3 . <*0,0,0*> = 0 & and3 . <*0,0,1*> = 0 & and3 . <*0,1,0*> = 0 & and3 . <*0,1,1*> = 0 & and3 . <*1,0,0*> = 0 & and3 . <*1,0,1*> = 0 & and3 . <*1,1,0*> = 0 & and3 . <*1,1,1*> = 1 )

proof end;

theorem Th22: :: TWOSCOMP:22

( and3a . <*0,0,0*> = 0 & and3a . <*0,0,1*> = 0 & and3a . <*0,1,0*> = 0 & and3a . <*0,1,1*> = 1 & and3a . <*1,0,0*> = 0 & and3a . <*1,0,1*> = 0 & and3a . <*1,1,0*> = 0 & and3a . <*1,1,1*> = 0 )

proof end;

theorem Th23: :: TWOSCOMP:23

( and3b . <*0,0,0*> = 0 & and3b . <*0,0,1*> = 1 & and3b . <*0,1,0*> = 0 & and3b . <*0,1,1*> = 0 & and3b . <*1,0,0*> = 0 & and3b . <*1,0,1*> = 0 & and3b . <*1,1,0*> = 0 & and3b . <*1,1,1*> = 0 )

proof end;

theorem Th24: :: TWOSCOMP:24

( and3c . <*0,0,0*> = 1 & and3c . <*0,0,1*> = 0 & and3c . <*0,1,0*> = 0 & and3c . <*0,1,1*> = 0 & and3c . <*1,0,0*> = 0 & and3c . <*1,0,1*> = 0 & and3c . <*1,1,0*> = 0 & and3c . <*1,1,1*> = 0 )

proof end;

theorem Th25: :: TWOSCOMP:25

( or3 . <*0,0,0*> = 0 & or3 . <*0,0,1*> = 1 & or3 . <*0,1,0*> = 1 & or3 . <*0,1,1*> = 1 & or3 . <*1,0,0*> = 1 & or3 . <*1,0,1*> = 1 & or3 . <*1,1,0*> = 1 & or3 . <*1,1,1*> = 1 )

proof end;

theorem Th26: :: TWOSCOMP:26

( or3a . <*0,0,0*> = 1 & or3a . <*0,0,1*> = 1 & or3a . <*0,1,0*> = 1 & or3a . <*0,1,1*> = 1 & or3a . <*1,0,0*> = 0 & or3a . <*1,0,1*> = 1 & or3a . <*1,1,0*> = 1 & or3a . <*1,1,1*> = 1 )

proof end;

theorem Th27: :: TWOSCOMP:27

( or3b . <*0,0,0*> = 1 & or3b . <*0,0,1*> = 1 & or3b . <*0,1,0*> = 1 & or3b . <*0,1,1*> = 1 & or3b . <*1,0,0*> = 1 & or3b . <*1,0,1*> = 1 & or3b . <*1,1,0*> = 0 & or3b . <*1,1,1*> = 1 )

proof end;

theorem Th28: :: TWOSCOMP:28

( or3c . <*0,0,0*> = 1 & or3c . <*0,0,1*> = 1 & or3c . <*0,1,0*> = 1 & or3c . <*0,1,1*> = 1 & or3c . <*1,0,0*> = 1 & or3c . <*1,0,1*> = 1 & or3c . <*1,1,0*> = 1 & or3c . <*1,1,1*> = 0 )

proof end;

theorem Th29: :: TWOSCOMP:29

( xor3 . <*0,0,0*> = 0 & xor3 . <*0,0,1*> = 1 & xor3 . <*0,1,0*> = 1 & xor3 . <*0,1,1*> = 0 & xor3 . <*1,0,0*> = 1 & xor3 . <*1,0,1*> = 0 & xor3 . <*1,1,0*> = 0 & xor3 . <*1,1,1*> = 1 )

proof end;

definition

let c₁, c₂ be set ;
func CompStr c₁,c₂ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: TWOSCOMP:def 33
1GateCircStr <*a₁,a₂*>,xor2a ;
correctness ;

end;

:: deftheorem Def33 defines CompStr TWOSCOMP:def 33 :

definition

let c₁, c₂ be set ;
func CompCirc c₁,c₂ -> strict gate`2=den Boolean Circuit of CompStr a₁,a₂ equals :: TWOSCOMP:def 34
1GateCircuit a₁,a₂,xor2a ;
coherence ;

end;

:: deftheorem Def34 defines CompCirc TWOSCOMP:def 34 :

definition

let c₁, c₂ be set ;
func CompOutput c₁,c₂ -> Element of InnerVertices (CompStr a₁,a₂) equals :: TWOSCOMP:def 35
[<*a₁,a₂*>,xor2a ];
coherence by FACIRC_1:47;

end;

:: deftheorem Def35 defines CompOutput TWOSCOMP:def 35 :

definition

let c₁, c₂ be set ;
func IncrementStr c₁,c₂ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: TWOSCOMP:def 36
1GateCircStr <*a₁,a₂*>,and2a ;
correctness ;

end;

:: deftheorem Def36 defines IncrementStr TWOSCOMP:def 36 :

definition

let c₁, c₂ be set ;
func IncrementCirc c₁,c₂ -> strict gate`2=den Boolean Circuit of IncrementStr a₁,a₂ equals :: TWOSCOMP:def 37
1GateCircuit a₁,a₂,and2a ;
coherence ;

end;

:: deftheorem Def37 defines IncrementCirc TWOSCOMP:def 37 :

definition

let c₁, c₂ be set ;
func IncrementOutput c₁,c₂ -> Element of InnerVertices (IncrementStr a₁,a₂) equals :: TWOSCOMP:def 38
[<*a₁,a₂*>,and2a ];
coherence by FACIRC_1:47;

end;

:: deftheorem Def38 defines IncrementOutput TWOSCOMP:def 38 :

definition

let c₁, c₂ be set ;
func BitCompStr c₁,c₂ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: TWOSCOMP:def 39
(CompStr a₁,a₂) +* (IncrementStr a₁,a₂);
correctness ;

end;

:: deftheorem Def39 defines BitCompStr TWOSCOMP:def 39 :

definition

let c₁, c₂ be set ;
func BitCompCirc c₁,c₂ -> strict gate`2=den Boolean Circuit of BitCompStr a₁,a₂ equals :: TWOSCOMP:def 40
(CompCirc a₁,a₂) +* (IncrementCirc a₁,a₂);
coherence ;

end;

:: deftheorem Def40 defines BitCompCirc TWOSCOMP:def 40 :

theorem Th30: :: TWOSCOMP:30

for b₁, b₂ being non pair set holds InnerVertices (CompStr b₁,b₂) is Relation by FACIRC_1:38;

theorem Th31: :: TWOSCOMP:31

for b₁, b₂ being non pair set holds
( b₁ in the carrier of (CompStr b₁,b₂) & b₂ in the carrier of (CompStr b₁,b₂) & [<*b₁,b₂*>,xor2a ] in the carrier of (CompStr b₁,b₂) ) by FACIRC_1:43;

theorem Th32: :: TWOSCOMP:32

for b₁, b₂ being non pair set holds the carrier of (CompStr b₁,b₂) = {b₁,b₂} \/ {[<*b₁,b₂*>,xor2a ]}

proof end;

theorem Th33: :: TWOSCOMP:33

for b₁, b₂ being non pair set holds InnerVertices (CompStr b₁,b₂) = {[<*b₁,b₂*>,xor2a ]} by CIRCCOMB:49;

theorem Th34: :: TWOSCOMP:34

for b₁, b₂ being non pair set holds [<*b₁,b₂*>,xor2a ] in InnerVertices (CompStr b₁,b₂)

proof end;

theorem Th35: :: TWOSCOMP:35

for b₁, b₂ being non pair set holds InputVertices (CompStr b₁,b₂) = {b₁,b₂} by FACIRC_1:40;

theorem Th36: :: TWOSCOMP:36

for b₁, b₂ being non pair set holds
( b₁ in InputVertices (CompStr b₁,b₂) & b₂ in InputVertices (CompStr b₁,b₂) )

proof end;

theorem Th37: :: TWOSCOMP:37

for b₁, b₂ being non pair set holds not InputVertices (CompStr b₁,b₂) is with_pair

proof end;

theorem Th38: :: TWOSCOMP:38

for b₁, b₂ being non pair set holds InnerVertices (IncrementStr b₁,b₂) is Relation by FACIRC_1:38;

theorem Th39: :: TWOSCOMP:39

for b₁, b₂ being non pair set holds
( b₁ in the carrier of (IncrementStr b₁,b₂) & b₂ in the carrier of (IncrementStr b₁,b₂) & [<*b₁,b₂*>,and2a ] in the carrier of (IncrementStr b₁,b₂) ) by FACIRC_1:43;

theorem Th40: :: TWOSCOMP:40

for b₁, b₂ being non pair set holds the carrier of (IncrementStr b₁,b₂) = {b₁,b₂} \/ {[<*b₁,b₂*>,and2a ]}

proof end;

theorem Th41: :: TWOSCOMP:41

for b₁, b₂ being non pair set holds InnerVertices (IncrementStr b₁,b₂) = {[<*b₁,b₂*>,and2a ]} by CIRCCOMB:49;

theorem Th42: :: TWOSCOMP:42

for b₁, b₂ being non pair set holds [<*b₁,b₂*>,and2a ] in InnerVertices (IncrementStr b₁,b₂)

proof end;

theorem Th43: :: TWOSCOMP:43

for b₁, b₂ being non pair set holds InputVertices (IncrementStr b₁,b₂) = {b₁,b₂} by FACIRC_1:40;

theorem Th44: :: TWOSCOMP:44

for b₁, b₂ being non pair set holds
( b₁ in InputVertices (IncrementStr b₁,b₂) & b₂ in InputVertices (IncrementStr b₁,b₂) )

proof end;

theorem Th45: :: TWOSCOMP:45

for b₁, b₂ being non pair set holds not InputVertices (IncrementStr b₁,b₂) is with_pair

proof end;

theorem Th46: :: TWOSCOMP:46

for b₁, b₂ being non pair set holds InnerVertices (BitCompStr b₁,b₂) is Relation

proof end;

theorem Th47: :: TWOSCOMP:47

for b₁, b₂ being non pair set holds
( b₁ in the carrier of (BitCompStr b₁,b₂) & b₂ in the carrier of (BitCompStr b₁,b₂) & [<*b₁,b₂*>,xor2a ] in the carrier of (BitCompStr b₁,b₂) & [<*b₁,b₂*>,and2a ] in the carrier of (BitCompStr b₁,b₂) )

proof end;

theorem Th48: :: TWOSCOMP:48

for b₁, b₂ being non pair set holds the carrier of (BitCompStr b₁,b₂) = {b₁,b₂} \/ {[<*b₁,b₂*>,xor2a ],[<*b₁,b₂*>,and2a ]}

proof end;

theorem Th49: :: TWOSCOMP:49

for b₁, b₂ being non pair set holds InnerVertices (BitCompStr b₁,b₂) = {[<*b₁,b₂*>,xor2a ],[<*b₁,b₂*>,and2a ]}

proof end;

theorem Th50: :: TWOSCOMP:50

for b₁, b₂ being non pair set holds
( [<*b₁,b₂*>,xor2a ] in InnerVertices (BitCompStr b₁,b₂) & [<*b₁,b₂*>,and2a ] in InnerVertices (BitCompStr b₁,b₂) )

proof end;

theorem Th51: :: TWOSCOMP:51

for b₁, b₂ being non pair set holds InputVertices (BitCompStr b₁,b₂) = {b₁,b₂}

proof end;

theorem Th52: :: TWOSCOMP:52

for b₁, b₂ being non pair set holds
( b₁ in InputVertices (BitCompStr b₁,b₂) & b₂ in InputVertices (BitCompStr b₁,b₂) )

proof end;

theorem Th53: :: TWOSCOMP:53

for b₁, b₂ being non pair set holds not InputVertices (BitCompStr b₁,b₂) is with_pair

proof end;

theorem Th54: :: TWOSCOMP:54

for b₁, b₂ being non pair set
for b₃ being State of (CompCirc b₁,b₂) holds
( (Following b₃) . (CompOutput b₁,b₂) = xor2a . <*(b₃ . b₁),(b₃ . b₂)*> & (Following b₃) . b₁ = b₃ . b₁ & (Following b₃) . b₂ = b₃ . b₂ )

proof end;

theorem Th55: :: TWOSCOMP:55

for b₁, b₂ being non pair set
for b₃ being State of (CompCirc b₁,b₂)
for b₄, b₅ being Element of BOOLEAN st b₄ = b₃ . b₁ & b₅ = b₃ . b₂ holds
( (Following b₃) . (CompOutput b₁,b₂) = ('not' b₄) 'xor' b₅ & (Following b₃) . b₁ = b₄ & (Following b₃) . b₂ = b₅ )

proof end;

theorem Th56: :: TWOSCOMP:56

for b₁, b₂ being non pair set
for b₃ being State of (BitCompCirc b₁,b₂) holds
( (Following b₃) . (CompOutput b₁,b₂) = xor2a . <*(b₃ . b₁),(b₃ . b₂)*> & (Following b₃) . b₁ = b₃ . b₁ & (Following b₃) . b₂ = b₃ . b₂ )

proof end;

theorem Th57: :: TWOSCOMP:57

for b₁, b₂ being non pair set
for b₃ being State of (BitCompCirc b₁,b₂)
for b₄, b₅ being Element of BOOLEAN st b₄ = b₃ . b₁ & b₅ = b₃ . b₂ holds
( (Following b₃) . (CompOutput b₁,b₂) = ('not' b₄) 'xor' b₅ & (Following b₃) . b₁ = b₄ & (Following b₃) . b₂ = b₅ )

proof end;

theorem Th58: :: TWOSCOMP:58

for b₁, b₂ being non pair set
for b₃ being State of (IncrementCirc b₁,b₂) holds
( (Following b₃) . (IncrementOutput b₁,b₂) = and2a . <*(b₃ . b₁),(b₃ . b₂)*> & (Following b₃) . b₁ = b₃ . b₁ & (Following b₃) . b₂ = b₃ . b₂ )

proof end;

theorem Th59: :: TWOSCOMP:59

for b₁, b₂ being non pair set
for b₃ being State of (IncrementCirc b₁,b₂)
for b₄, b₅ being Element of BOOLEAN st b₄ = b₃ . b₁ & b₅ = b₃ . b₂ holds
( (Following b₃) . (IncrementOutput b₁,b₂) = ('not' b₄) '&' b₅ & (Following b₃) . b₁ = b₄ & (Following b₃) . b₂ = b₅ )

proof end;

theorem Th60: :: TWOSCOMP:60

for b₁, b₂ being non pair set
for b₃ being State of (BitCompCirc b₁,b₂) holds
( (Following b₃) . (IncrementOutput b₁,b₂) = and2a . <*(b₃ . b₁),(b₃ . b₂)*> & (Following b₃) . b₁ = b₃ . b₁ & (Following b₃) . b₂ = b₃ . b₂ )

proof end;

theorem Th61: :: TWOSCOMP:61

for b₁, b₂ being non pair set
for b₃ being State of (BitCompCirc b₁,b₂)
for b₄, b₅ being Element of BOOLEAN st b₄ = b₃ . b₁ & b₅ = b₃ . b₂ holds
( (Following b₃) . (IncrementOutput b₁,b₂) = ('not' b₄) '&' b₅ & (Following b₃) . b₁ = b₄ & (Following b₃) . b₂ = b₅ )

proof end;

theorem Th62: :: TWOSCOMP:62

for b₁, b₂ being non pair set
for b₃ being State of (BitCompCirc b₁,b₂) holds
( (Following b₃) . (CompOutput b₁,b₂) = xor2a . <*(b₃ . b₁),(b₃ . b₂)*> & (Following b₃) . (IncrementOutput b₁,b₂) = and2a . <*(b₃ . b₁),(b₃ . b₂)*> & (Following b₃) . b₁ = b₃ . b₁ & (Following b₃) . b₂ = b₃ . b₂ ) by Th56, Th60;

theorem Th63: :: TWOSCOMP:63

theorem Th64: :: TWOSCOMP:64

for b₁, b₂ being non pair set
for b₃ being State of (BitCompCirc b₁,b₂) holds Following b₃ is stable

proof end;