let S be non empty finite non void unsplit gate`1=arity gate`2=den ManySortedSign ; :: thesis: for A being non-empty Circuit of S st A is gate`2=den holds
A is with_stabilization-limit
let A be non-empty Circuit of S; :: thesis: ( A is gate`2=den implies A is with_stabilization-limit )
assume A1: A is gate`2=den ; :: thesis: A is with_stabilization-limit
defpred S<sub>1</sub>[ set , set ] means ( $1 = $2 or ( $1 in the carrier' of S & $2 in proj2 ($1 `1 ) ) );
consider R being Relation such that
A2: for a, b being set holds
( [a,b] in R iff ( a in the carrier of S & b in the carrier of S & S₁[a,b] ) ) from RELAT_1:sch 1();
defpred S₂[ set ] means ( $1 in the carrier of S implies ex n being Element of NAT st
for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . $1 = (Following s,n) . $1 );
A3: R is co-well_founded

proof

let Y be set ; :: according to REWRITE1:def 16 :: thesis: ( not Y c= field R or Y = {} or ex b₁ being set st
( b₁ in Y & ( for b₂ being set holds
( not b₂ in Y or b₁ = b₂ or not [b₁,b₂] in R ) ) ) )
assume A4: ( Y c= field R & Y <> {} ) ; :: thesis: ex b₁ being set st
( b₁ in Y & ( for b₂ being set holds
( not b₂ in Y or b₁ = b₂ or not [b₁,b₂] in R ) ) )
defpred S₃[ set , set ] means $2 = the_rank_of $1;
A5: for x, y, z being set st S₃[x,y] & S₃[x,z] holds
y = z ;
consider B being set such that
A6: for x being set holds
( x in B iff ex y being set st
( y in Y & S₃[y,x] ) ) from TARSKI:sch 1(A5);
consider y being Element of Y;
the_rank_of y in B by A4, A6;
then inf B in B by ORDINAL2:25;
then consider y being set such that
A7: ( y in Y & inf B = the_rank_of y ) by A6;
take y ; :: thesis: ( y in Y & ( for b₁ being set holds
( not b₁ in Y or y = b₁ or not [y,b₁] in R ) ) )
thus y in Y by A7; :: thesis: for b₁ being set holds
( not b₁ in Y or y = b₁ or not [y,b₁] in R )
let b be set ; :: thesis: ( not b in Y or y = b or not [y,b] in R )
assume A8: ( b in Y & y <> b & [y,b] in R ) ; :: thesis: contradiction
then A9: ( y in the carrier' of S & b in the carrier of S & b in proj2 (y `1 ) ) by A2;
then consider c being set such that
A10: [c,b] in y `1 by RELAT_1:def 5;
A11: the_rank_of [c,b] in the_rank_of (y `1 ) by A10, CLASSES1:76;
A12: the_rank_of b in the_rank_of [c,b] by Th34;
y = [(y `1 ),(the Charact of A . y)] by A1, A9, CIRCCOMB:def 10;
then A13: the_rank_of (y `1 ) in the_rank_of y by Th34;
the_rank_of b in B by A6, A8;
then inf B c= the_rank_of b by ORDINAL2:22;
hence contradiction by A7, A11, A12, A13, ORDINAL1:19; :: thesis: verum

end;

A14: dom R c= the carrier of S

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in dom R or o in the carrier of S )
assume o in dom R ; :: thesis: o in the carrier of S
then consider q being set such that
A15: [o,q] in R by RELAT_1:def 4;
thus o in the carrier of S by A2, A15; :: thesis: verum

end;

rng R c= the carrier of S

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in rng R or o in the carrier of S )
assume o in rng R ; :: thesis: o in the carrier of S
then consider q being set such that
A16: [q,o] in R by RELAT_1:def 5;
thus o in the carrier of S by A2, A16; :: thesis: verum

end;

then A17: (dom R) \/ (rng R) c= the carrier of S \/ the carrier of S by A14, XBOOLE_1:13;
A18: the carrier of S c= field R

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in the carrier of S or o in field R )
assume o in the carrier of S ; :: thesis: o in field R
then [o,o] in R by A2;
hence o in field R by RELAT_1:30; :: thesis: verum

end;

then A19: the carrier of S = field R by A17, XBOOLE_0:def 10;
A20: for a being set st ( for b being set st [a,b] in R & a <> b holds
S₂[b] ) holds
S₂[a]

proof

let a be set ; :: thesis: ( ( for b being set st [a,b] in R & a <> b holds
S₂[b] ) implies S₂[a] )
assume A21: for b being set st [a,b] in R & a <> b holds
S₂[b] ; :: thesis: S₂[a]
defpred S₃[ set ] means ( a <> $1 & [a,$1] in R );
consider RS being set such that
A22: for b being set holds
( b in RS iff ( b in field R & S₃[b] ) ) from XBOOLE_0:sch 1();
assume A23: a in the carrier of S ; :: thesis: ex n being Element of NAT st
for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . a = (Following s,n) . a
A24: RS c= the carrier of S

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in RS or o in the carrier of S )
assume o in RS ; :: thesis: o in the carrier of S
hence o in the carrier of S by A19, A22; :: thesis: verum

end;

then A25: RS is finite ;
defpred S₄[ set , set ] means ex n being Element of NAT st
( $2 = n & ( for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . $1 = (Following s,n) . $1 ) );
A26: for b being set st b in RS holds
ex z being set st S₄[b,z]

proof

let b be set ; :: thesis: ( b in RS implies ex z being set st S₄[b,z] )
assume A27: b in RS ; :: thesis: ex z being set st S₄[b,z]
then ( b in field R & a <> b & [a,b] in R ) by A22;
then ex n being Element of NAT st
for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . b = (Following s,n) . b by A21, A24, A27;
hence ex z being set st S₄[b,z] ; :: thesis: verum

end;

consider f being Function such that
A28: dom f = RS and
A29: for x being set st x in RS holds
S₄[x,f . x] from CLASSES1:sch 1(A26);

per cases ( RS <> {} or RS = {} ) ;

suppose A30: RS <> {} ; :: thesis: ex n being Element of NAT st
for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . a = (Following s,n) . a

rng f c= NAT

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in rng f or o in NAT )
assume o in rng f ; :: thesis: o in NAT
then consider l being set such that
A31: ( l in dom f & o = f . l ) by FUNCT_1:def 5;
consider n being Element of NAT such that
A32: ( f . l = n & ( for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . l = (Following s,n) . l ) ) by A28, A29, A31;
thus o in NAT by A31, A32; :: thesis: verum

end;

then reconsider C = rng f as non empty finite Subset of NAT by A25, A28, A30, FINSET_1:26, RELAT_1:60, RELAT_1:64;
reconsider mC = max C as Element of NAT by ORDINAL1:def 13;
take n = mC + 1; :: thesis: for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . a = (Following s,n) . a
let s be State of A; :: thesis: for m being Element of NAT st m >= n holds
(Following s,m) . a = (Following s,n) . a
let m be Element of NAT ; :: thesis: ( m >= n implies (Following s,m) . a = (Following s,n) . a )
assume m >= n ; :: thesis: (Following s,m) . a = (Following s,n) . a
then consider k being Nat such that
A33: m = n + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
consider b being Element of RS;
( b in field R & a <> b & [a,b] in R ) by A22, A30;
then reconsider a1 = a as Gate of S by A2;
A34: the_result_sort_of a1 = the ResultSort of S . a1 by MSUALG_1:def 7
.= a by CIRCCOMB:52 ;
for x being set st x in rng (the_arity_of a1) holds
Following s,mC is_stable_at x

proof

let x be set ; :: thesis: ( x in rng (the_arity_of a1) implies Following s,mC is_stable_at x )
assume A35: x in rng (the_arity_of a1) ; :: thesis: Following s,mC is_stable_at x
a1 = [(the Arity of S . a1),(a1 `2 )] by CIRCCOMB:def 8;
then A37: a1 = [(the_arity_of a1),(a1 `2 )] by MSUALG_1:def 6;
then the_rank_of x in the_rank_of a1 by A35, CLASSES1:90;
then A38: x <> a ;
rng (the_arity_of a1) c= the carrier of S by FINSEQ_1:def 4;
then ( x in the carrier of S & x in proj2 (a `1 ) ) by A35, A37, MCART_1:7;
then [a1,x] in R by A2, A23;
then ( x in field R & [a,x] in R ) by RELAT_1:30;
then A39: x in RS by A22, A38;
then consider l being Element of NAT such that
A40: ( f . x = l & ( for s being State of A
for m being Element of NAT st m >= l holds
(Following s,m) . x = (Following s,l) . x ) ) by A29;
l in rng f by A28, A39, A40, FUNCT_1:12;
then A41: max C >= l by XXREAL_2:def 8;

now

let k be Nat; :: thesis: (Following (Following s,mC),k) . x = (Following s,mC) . x
A42: mC + k >= max C by NAT_1:11;
thus (Following (Following s,mC),k) . x = (Following s,(mC + k)) . x by FACIRC_1:13
.= (Following s,l) . x by A40, A41, A42, XXREAL_0:2
.= (Following s,mC) . x by A40, A41 ; :: thesis: verum

end;

hence Following s,mC is_stable_at x by FACIRC_1:def 9; :: thesis: verum

end;

then Following (Following s,mC) is_stable_at a by A34, FACIRC_1:19;
then Following s,n is_stable_at a by FACIRC_1:12;
then (Following (Following s,n),k) . a = (Following s,n) . a by FACIRC_1:def 9;
hence (Following s,m) . a = (Following s,n) . a by A33, FACIRC_1:13; :: thesis: verum

end;

suppose A43: RS = {} ; :: thesis: ex n being Element of NAT st
for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . a = (Following s,n) . a

take n = 1; :: thesis: for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . a = (Following s,n) . a
let s be State of A; :: thesis: for m being Element of NAT st m >= n holds
(Following s,m) . a = (Following s,n) . a
let m be Element of NAT ; :: thesis: ( m >= n implies (Following s,m) . a = (Following s,n) . a )
assume m >= n ; :: thesis: (Following s,m) . a = (Following s,n) . a
then consider k being Nat such that
A44: m = n + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A45: the carrier of S = (InputVertices S) \/ (InnerVertices S) by XBOOLE_1:45;

A46: now

assume a in InputVertices S ; :: thesis: (Following s,m) . a = (Following s,n) . a
then A47: s is_stable_at a by FACIRC_1:18;
hence (Following s,m) . a = s . a by FACIRC_1:def 9
.= (Following s,n) . a by A47, FACIRC_1:def 9 ;
:: thesis: verum

end;

now

assume a in InnerVertices S ; :: thesis: (Following s,m) . a = (Following s,n) . a
then a in rng (id the carrier' of S) by CIRCCOMB:def 7;
then reconsider a1 = a as Gate of S by RELAT_1:71;
A48: the_result_sort_of a1 = the ResultSort of S . a1 by MSUALG_1:def 7
.= a1 by CIRCCOMB:52 ;
for x being set st x in rng (the_arity_of a1) holds
s is_stable_at x

proof

let x be set ; :: thesis: ( x in rng (the_arity_of a1) implies s is_stable_at x )
assume A49: x in rng (the_arity_of a1) ; :: thesis: s is_stable_at x
a1 = [(the Arity of S . a1),(a1 `2 )] by CIRCCOMB:def 8;
then A51: a1 = [(the_arity_of a1),(a1 `2 )] by MSUALG_1:def 6;
then the_rank_of x in the_rank_of a1 by A49, CLASSES1:90;
then A52: x <> a ;
rng (the_arity_of a1) c= the carrier of S by FINSEQ_1:def 4;
then ( x in the carrier of S & x in proj2 (a `1 ) ) by A49, A51, MCART_1:7;
then [a1,x] in R by A2, A23;
then ( x in field R & [a,x] in R ) by RELAT_1:30;
hence s is_stable_at x by A22, A43, A52; :: thesis: verum

end;

then Following s is_stable_at the_result_sort_of a1 by FACIRC_1:19;
then Following s,n is_stable_at a1 by A48, FACIRC_1:14;
then (Following (Following s,n),k) . a = (Following s,n) . a by FACIRC_1:def 9;
hence (Following s,m) . a = (Following s,n) . a by A44, FACIRC_1:13; :: thesis: verum

end;

hence (Following s,m) . a = (Following s,n) . a by A23, A45, A46, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

A53: for a being set st a in field R holds
S₂[a] from REWRITE1:sch 2(A3, A20);
defpred S₃[ set , set ] means ex n being Element of NAT st
( $2 = n & ( for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . $1 = (Following s,n) . $1 ) );
A54: for a being set st a in field R holds
ex b being set st S₃[a,b]

proof

let a be set ; :: thesis: ( a in field R implies ex b being set st S₃[a,b] )
assume a in field R ; :: thesis: ex b being set st S₃[a,b]
then ex n being Element of NAT st
for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . a = (Following s,n) . a by A17, A53;
hence ex b being set st S₃[a,b] ; :: thesis: verum

end;

consider f being Function such that
A55: dom f = field R and
A56: for x being set st x in field R holds
S₃[x,f . x] from CLASSES1:sch 1(A54);
rng f c= NAT

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in rng f or o in NAT )
assume o in rng f ; :: thesis: o in NAT
then consider l being set such that
A57: ( l in dom f & o = f . l ) by FUNCT_1:def 5;
consider n being Element of NAT such that
A58: ( f . l = n & ( for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . l = (Following s,n) . l ) ) by A55, A56, A57;
thus o in NAT by A57, A58; :: thesis: verum

end;

then reconsider C = rng f as non empty finite Subset of NAT by A19, A55, FINSET_1:26, RELAT_1:60, RELAT_1:64;
reconsider N = max C as Element of NAT by ORDINAL1:def 13;
take N ; :: according to CIRCCMB3:def 3 :: thesis: for s being State of A holds Following s,N is stable
let s be State of A; :: thesis: Following s,N is stable
A59: ( dom (Following s,N) = the carrier of S & dom (Following (Following s,N)) = the carrier of S ) by CIRCUIT1:4;

now

let x be set ; :: thesis: ( x in the carrier of S implies (Following s,N) . x = (Following (Following s,N)) . x )
assume A60: x in the carrier of S ; :: thesis: (Following s,N) . x = (Following (Following s,N)) . x
then consider n being Element of NAT such that
A61: ( f . x = n & ( for s being State of A
for m being Element of NAT st m >= n holds
(Following s,m) . x = (Following s,n) . x ) ) by A18, A56;
n in C by A18, A55, A60, A61, FUNCT_1:12;
then A62: N >= n by XXREAL_2:def 8;
then A63: N + 1 >= n by NAT_1:13;
thus (Following s,N) . x = (Following s,n) . x by A61, A62
.= (Following s,(N + 1)) . x by A61, A63
.= (Following (Following s,N)) . x by FACIRC_1:12 ; :: thesis: verum

end;

hence Following s,N = Following (Following s,N) by A59, FUNCT_1:9; :: according to CIRCUIT2:def 6 :: thesis: verum