:: deftheorem defines InitialComp CIRCUIT2:def 8 :
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 holds InitialComp (s,InpFs) = (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS);