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 x being set st x in InputVertices S holds

s is_stable_at x

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

for x being set st x in InputVertices S holds

s is_stable_at x

let s be State of A; :: thesis: for x being set st x in InputVertices S holds

s is_stable_at x

let x be set ; :: thesis: ( x in InputVertices S implies s is_stable_at x )

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

assume A1: x in InputVertices S ; :: thesis: s is_stable_at x

_{1}[ 0 ]
by Th11;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A2); :: according to FACIRC_1:def 9 :: thesis: verum

for s being State of A

for x being set st x in InputVertices S holds

s is_stable_at x

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

for x being set st x in InputVertices S holds

s is_stable_at x

let s be State of A; :: thesis: for x being set st x in InputVertices S holds

s is_stable_at x

let x be set ; :: thesis: ( x in InputVertices S implies s is_stable_at x )

defpred S

assume A1: x in InputVertices S ; :: thesis: s is_stable_at x

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

S_{1}[n + 1]

A4:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

(Following (s,(n + 1))) . x = (Following (Following (s,n))) . x by Th12

.= s . x by A1, A3, CIRCUIT2:def 5 ;

hence S_{1}[n + 1]
; :: thesis: verum

end;assume A3: S

(Following (s,(n + 1))) . x = (Following (Following (s,n))) . x by Th12

.= s . x by A1, A3, CIRCUIT2:def 5 ;

hence S

thus for n being Nat holds S