:: deftheorem defines BitAdderWithOverflowCirc FACIRC_1:def 23 :
for x, y, c being object holds BitAdderWithOverflowCirc (x,y,c) = (BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c));