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 st s is stabilizing holds
Result s = Following (s,(stabilization-time s))
let A be non-empty Circuit of S; :: thesis: for s being State of A st s is stabilizing holds
Result s = Following (s,(stabilization-time s))
let s be State of A; :: thesis: ( s is stabilizing implies Result s = Following (s,(stabilization-time s)) )
assume A1: s is stabilizing ; :: thesis: Result s = Following (s,(stabilization-time s))
Following (s,(stabilization-time s)) is stable by A1, Def5;
hence Result s = Following (s,(stabilization-time s)) by A1, Def4; :: thesis: verum