:: deftheorem defines depends_on_in CIRCUIT1:def 3 :
for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS
for o being OperSymbol of IIG holds o depends_on_in s = s * (the_arity_of o);