:: deftheorem defines Following CIRCUIT2:def 7 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS holds Following (s,iv) = Following (s +* iv);