:: deftheorem defines BitGFA2AdderOutput GFACIRC1:def 40 :
for x, y, z being set holds BitGFA2AdderOutput (x,y,z) = 2GatesCircOutput (x,y,z,xor2c);