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 s is stabilizing & n >= stabilization-time s holds
Result s = Following (s,n)
let A be non-empty Circuit of S; :: thesis: for s being State of A
for n being Element of NAT st s is stabilizing & n >= stabilization-time s holds
Result s = Following (s,n)
let s be State of A; :: thesis: for n being Element of NAT st s is stabilizing & n >= stabilization-time s holds
Result s = Following (s,n)
let n be Element of NAT ; :: thesis: ( s is stabilizing & n >= stabilization-time s implies Result s = Following (s,n) )
assume that
A1: s is stabilizing and
A2: n >= stabilization-time s ; :: thesis: Result s = Following (s,n)
Result s is stable by A1, Def4;
then Following (s,(stabilization-time s)) is stable by A1, Th2;
then Following (s,n) is stable by A2, CIRCCMB2:4;
hence Result s = Following (s,n) by Th4; :: thesis: verum