:: deftheorem Def5 defines Following CIRCUIT2:def 5 :
for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for s, b₄ being State of SCS holds
( b₄ = Following s iff for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b₄ . v = s . v ) & ( v in InnerVertices IIG implies b₄ . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) );