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 stable holds

for n being natural Number holds Following (s,n) = s

let A be non-empty Circuit of S; :: thesis: for s being State of A st s is stable holds

for n being natural Number holds Following (s,n) = s

let s be State of A; :: thesis: ( s is stable implies for n being natural Number holds Following (s,n) = s )

assume A1: s is stable ; :: thesis: for n being natural Number holds Following (s,n) = s

let n be natural Number ; :: thesis: Following (s,n) = s

A0: n is Nat by TARSKI:1;

defpred S_{1}[ Nat] means Following (s,$1) = s;

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
by A1, FACIRC_1:12;

A3: S_{1}[ 0 ]
by FACIRC_1:11;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A3, A2);

hence Following (s,n) = s by A0; :: thesis: verum

for s being State of A st s is stable holds

for n being natural Number holds Following (s,n) = s

let A be non-empty Circuit of S; :: thesis: for s being State of A st s is stable holds

for n being natural Number holds Following (s,n) = s

let s be State of A; :: thesis: ( s is stable implies for n being natural Number holds Following (s,n) = s )

assume A1: s is stable ; :: thesis: for n being natural Number holds Following (s,n) = s

let n be natural Number ; :: thesis: Following (s,n) = s

A0: n is Nat by TARSKI:1;

defpred S

A2: for n being Nat st S

S

A3: S

for n being Nat holds S

hence Following (s,n) = s by A0; :: thesis: verum