:: deftheorem defines 2GatesCircuit FACIRC_1:def 14 :
for x, y, c being object
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 2GatesCircuit (x,y,c,f) = (1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f));