:: deftheorem Def4 defines Result CIRCCMB3:def 4 :
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A st s is stabilizing holds
for b₄ being State of A holds
( b₄ = Result s iff ( b₄ is stable & ex n being Element of NAT st b₄ = Following (s,n) ) );