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 )