for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for x being set st s is_stable_at x holds
for n being Nat holds Following (s,n) is_stable_at x