for IIG being non empty finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s1, s2 being State of SCS holds (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)