let S be non empty non void Circuit-like ManySortedSign ; :: thesis: for A being non-empty Circuit of S
for s being State of A
for n being Element of NAT st Following (s,n) is stable holds
stabilization-time s <= n
let A be non-empty Circuit of S; :: thesis: for s being State of A
for n being Element of NAT st Following (s,n) is stable holds
stabilization-time s <= n
let s be State of A; :: thesis: for n being Element of NAT st Following (s,n) is stable holds
stabilization-time s <= n
let n be Element of NAT ; :: thesis: ( Following (s,n) is stable implies stabilization-time s <= n )
assume A1: Following (s,n) is stable ; :: thesis: stabilization-time s <= n
then s is stabilizing ;
hence stabilization-time s <= n by A1, Def5; :: thesis: verum