:: deftheorem defines BitSubtracterWithBorrowStr FSCIRC_1:def 8 :
for x, y, c being set holds BitSubtracterWithBorrowStr (x,y,c) = (2GatesCircStr (x,y,c,'xor')) +* (BorrowStr (x,y,c));