theorem :: TWOSCOMP:42

for x, b being non pair set holds InputVertices (BitCompStr (x,b)) is without_pairs