:: deftheorem Def5 defines -CircuitCharact CIRCTRM1:def 5 :
for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V)
for A being non-empty MSAlgebra over S
for b₅ being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) holds
( b₅ = X -CircuitCharact A iff for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
b₅ . g = the_action_of (g,A) );