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