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 v being Vertex of IIG holds s . v in the Sorts of SCS . v