theorem :: TWOSCOMP:10

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