:: deftheorem Def8 defines xor2b TWOSCOMP:def 8 :
for b₁ being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b₁ = xor2b iff for x, y being Element of BOOLEAN holds b₁ . <*x,y*> = ('not' x) 'xor' ('not' y) );