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₁[ Nat] means Following (s,$1) = s;
A2: for n being Nat st S₁[n] holds
S₁[n + 1] by A1, FACIRC_1:12;
A3: S₁[ 0 ] by FACIRC_1:11;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A2);
hence Following (s,n) = s by A0; :: thesis: verum