:: deftheorem defines BitAdderCirc FACIRC_1:def 16 :
for x, y, c being object holds BitAdderCirc (x,y,c) = 2GatesCircuit (x,y,c,'xor');