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 iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Nat
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv)