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 s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable