:: deftheorem defines BitAdderWithOverflowStr FACIRC_1:def 22 :
for x, y, c being object holds BitAdderWithOverflowStr (x,y,c) = (2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c));