:: deftheorem Def7 defines one-gate CIRCCMB3:def 7 :
for S being non empty ManySortedSign
for A being MSAlgebra over S holds
( A is one-gate iff ex X being non empty finite set ex n being Element of NAT ex p being FinSeqLen of n ex f being Function of (n -tuples_on X),X st
( S = 1GateCircStr (p,f) & A = 1GateCircuit (p,f) ) );