:: deftheorem Def5 defines stabilization-time CIRCCMB3:def 5 :
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 Element of NAT holds
( b₄ = stabilization-time s iff ( Following (s,b₄) is stable & ( for n being Element of NAT st n < b₄ holds
not Following (s,n) is stable ) ) );