theorem Th13: :: CIRCUIT2:13

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS
for k being Nat st ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) holds
for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)