theorem Th31: :: FACIRC_2:31

for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] holds
for s being State of (BitAdderWithOverflowCirc (x,y,c)) holds Following (s,2) is stable