:: deftheorem defines IGValue CIRCUIT2:def 4 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS holds IGValue (v,iv) = ((Eval SCS) . v) . (IGTree (v,iv));