theorem :: TWOSCOMP:53

for x, b being non pair set
for s being State of (BitCompCirc (x,b)) holds Following s is stable