for x, b being non pair set
for s being State of (BitCompCirc (x,b)) holds
( (Following s) . (IncrementOutput (x,b)) = and2a . <*(s . x),(s . b)*> & (Following s) . x = s . x & (Following s) . b = s . b )