:: deftheorem Def9 defines Computation CIRCUIT2:def 9 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for s being State of SCS
for b₅ being sequence of (product the Sorts of SCS) holds
( b₅ = Computation (s,InpFs) iff ( b₅ . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b₅ . (i + 1) = Following ((b₅ . i),((i + 1) -th_InputValues InpFs)) ) ) );