theorem :: FSCIRC_1:25

for x, y, c being non pair set
for s being State of (BitSubtracterWithBorrowCirc (x,y,c)) holds Following (s,2) is stable