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
defpred S1[ object , object ] means ( $1 = $2 or ( $1 in the carrier' of S & $2 in proj2 ($1 `1) ) );
consider R being Relation such that
A1: for a, b being object holds
( [a,b] in R iff ( a in the carrier of S & b in the carrier of S & S1[a,b] ) ) from RELAT_1:sch 1();
 let A be non-empty Circuit of S; :: thesis: ( A is gate`2=den implies A is with_stabilization-limit )
assume A2: A is gate`2=den ; :: thesis: A is with_stabilization-limit
A3: R is co-well_founded
proof
defpred S2[ object , object ] means ex x being set st
( x = $1 & $2 = the_rank_of x );
let Y be set ; :: according to REWRITE1:def 16 :: thesis: ( not Y c= field R or Y = {} or ex b1 being object st
( b1 in Y & ( for b2 being object holds
( not b2 in Y or b1 = b2 or not [b1,b2] in R ) ) ) )
assume that
Y c= field R and
A4: Y <> {} ; :: thesis: ex b1 being object st
( b1 in Y & ( for b2 being object holds
( not b2 in Y or b1 = b2 or not [b1,b2] in R ) ) )
set y = the Element of Y;
A5: for x, y, z being object st S2[x,y] & S2[x,z] holds
y = z ;
consider B being set such that
A6: for x being object holds
( x in B iff ex y being object st
( y in Y & S2[y,x] ) ) from TARSKI:sch 1(A5);
 the_rank_of the Element of Y in B by A4, A6;
then inf B in B by ORDINAL2:17;
then consider y being object such that
A7: y in Y and
A8: S2[y, inf B] by A6;
reconsider y = y as set by TARSKI:1;
take y ; :: thesis: ( y in Y & ( for b1 being object holds
( not b1 in Y or y = b1 or not [y,b1] in R ) ) )
thus y in Y by A7; :: thesis: for b1 being object holds
( not b1 in Y or y = b1 or not [y,b1] in R )
let b be object ; :: thesis: ( not b in Y or y = b or not [y,b] in R )
assume that
A9: b in Y and
A10: ( y <> b & [y,b] in R ) ; :: thesis: contradiction
the_rank_of b in B by A6, A9;
then A11: inf B c= the_rank_of b by ORDINAL2:14;
y in the carrier' of S by A1, A10;
then y = [(y `1),( the Charact of A . y)] by A2;
then A12: the_rank_of (y `1) in the_rank_of y by Th31;
b in proj2 (y `1) by A1, A10;
then consider c being object such that
A13: [c,b] in y `1 by XTUPLE_0:def 13;
A14: the_rank_of b in the_rank_of [c,b] by Th31;
the_rank_of [c,b] in the_rank_of (y `1) by A13, CLASSES1:68;
hence contradiction by A8, A14, A12, A11, ORDINAL1:10; :: thesis: verum
end;
defpred S2[ object , object ] 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 ) );
defpred S3[ object ] 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 );
A15: rng R c= the carrier of S
proof
let o be object ; :: 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 ex q being object st [q,o] in R by XTUPLE_0:def 13;
hence o in the carrier of S by A1; :: thesis: verum
end;
A16: the carrier of S c= field R
proof
let o be object ; :: 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 A1;
hence o in field R by RELAT_1:15; :: thesis: verum
end;
dom R c= the carrier of S
proof
let o be object ; :: 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 ex q being object st [o,q] in R by XTUPLE_0:def 12;
hence o in the carrier of S by A1; :: thesis: verum
end;
then A17: (dom R) \/ (rng R) c= the carrier of S \/ the carrier of S by A15, XBOOLE_1:13;
then A18: the carrier of S = field R by A16, XBOOLE_0:def 10;
A19: for a being object st ( for b being object st [a,b] in R & a <> b holds
S3[b] ) holds
S3[a]
proof
defpred S4[ object , object ] 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 ) );
let a be object ; :: thesis: ( ( for b being object st [a,b] in R & a <> b holds
S3[b] ) implies S3[a] )
defpred S5[ object ] means ( a <> $1 & [a,$1] in R );
consider RS being set such that
A20: for b being object holds
( b in RS iff ( b in field R & S5[b] ) ) from XBOOLE_0:sch 1();
 A21: RS c= the carrier of S by A18, A20;
assume A22: for b being object st [a,b] in R & a <> b holds
S3[b] ; :: thesis: S3[a]
A23: for b being object st b in RS holds
ex z being object st S4[b,z]
proof
let b be object ; :: thesis: ( b in RS implies ex z being object st S4[b,z] )
assume A24: b in RS ; :: thesis: ex z being object st S4[b,z]
then ( a <> b & [a,b] in R ) by A20;
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 A22, A21, A24;
hence ex z being object st S4[b,z] ; :: thesis: verum
end;
consider f being Function such that
A25: dom f = RS and
A26: for x being object st x in RS holds
S4[x,f . x] from CLASSES1:sch 1(A23);
 assume A27: 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
per cases ( RS <> {} or RS = {} ) ;
suppose A28: 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 object ; :: 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 object such that
A29: l in dom f and
A30: o = f . l by FUNCT_1:def 3;
ex n being Element of NAT st
( 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 A25, A26, A29;
hence o in NAT by A30; :: thesis: verum
end;
then reconsider C = rng f as non empty finite Subset of NAT by A21, A25, A28, FINSET_1:8, RELAT_1:38, RELAT_1:41;
set b = the Element of RS;
( a <> the Element of RS & [a, the Element of RS] in R ) by A20, A28;
then reconsider a1 = a as Gate of S by A1;
reconsider mC = max C as Element of NAT by ORDINAL1:def 12;
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
A31: m = n + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A32: 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 A33: 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 A34: a1 = [(the_arity_of a1),(a1 `2)] by MSUALG_1:def 1;
then the_rank_of x in the_rank_of a1 by A33, CLASSES1:82;
then A35: x <> a ;
( rng (the_arity_of a1) c= the carrier of S & x in proj2 (a `1) ) by A33, A34, FINSEQ_1:def 4;
then A36: [a1,x] in R by A1, A27, A33;
then x in field R by RELAT_1:15;
then A37: x in RS by A20, A35, A36;
then consider l being Element of NAT such that
A38: f . x = l and
A39: 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 A26;
l in rng f by A25, A37, A38, FUNCT_1:3;
then A40: max C >= l by XXREAL_2:def 8;
now :: thesis: for k being Nat holds (Following ((Following (s,mC)),k)) . x = (Following (s,mC)) . x
let k be Nat; :: thesis: (Following ((Following (s,mC)),k)) . x = (Following (s,mC)) . x
A41: mC + k in NAT by ORDINAL1:def 12;
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 A39, A40, A42, XXREAL_0:2, A41
.= (Following (s,mC)) . x by A39, A40 ; :: thesis: verum
end;
hence Following (s,mC) is_stable_at x ; :: thesis: verum
end;
the_result_sort_of a1 = the ResultSort of S . a1 by MSUALG_1:def 2
.= a by CIRCCOMB:44 ;
then Following (Following (s,mC)) is_stable_at a by A32, 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 ;
hence (Following (s,m)) . a = (Following (s,n)) . a by A31, 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 12;
A45: now :: thesis: ( a in InnerVertices S implies (Following (s,m)) . a = (Following (s,n)) . a )
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 ;
for x being set st x in rng (the_arity_of a1) holds
s is_stable_at x then A50: Following s is_stable_at the_result_sort_of a1 by FACIRC_1:19;
the_result_sort_of a1 = the ResultSort of S . a1 by MSUALG_1:def 2
.= a1 by CIRCCOMB:44 ;
then Following (s,n) is_stable_at a1 by A50, FACIRC_1:14;
then (Following ((Following (s,n)),k)) . a = (Following (s,n)) . a ;
hence (Following (s,m)) . a = (Following (s,n)) . a by A44, FACIRC_1:13; :: thesis: verum
end;
A51: now :: thesis: ( a in InputVertices S implies (Following (s,m)) . a = (Following (s,n)) . a )
assume a in InputVertices S ; :: thesis: (Following (s,m)) . a = (Following (s,n)) . a
then A52: s is_stable_at a by FACIRC_1:18;
hence (Following (s,m)) . a = s . a
.= (Following (s,n)) . a by A52 ;
:: thesis: verum
end;
the carrier of S = (InputVertices S) \/ (InnerVertices S) by XBOOLE_1:45;
hence (Following (s,m)) . a = (Following (s,n)) . a by A27, A51, A45, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
A53: for a being object st a in field R holds
S3[a] from REWRITE1:sch 2(A3, A19);
 A54: for a being object st a in field R holds
ex b being object st S2[a,b]
proof
let a be object ; :: thesis: ( a in field R implies ex b being object st S2[a,b] )
assume a in field R ; :: thesis: ex b being object st S2[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 object st S2[a,b] ; :: thesis: verum
end;
consider f being Function such that
A55: dom f = field R and
A56: for x being object st x in field R holds
S2[x,f . x] from CLASSES1:sch 1(A54);
 rng f c= NAT
proof
let o be object ; :: 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 object such that
A57: l in dom f and
A58: o = f . l by FUNCT_1:def 3;
ex n being Element of NAT st
( 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;
hence o in NAT by A58; :: thesis: verum
end;
then reconsider C = rng f as non empty finite Subset of NAT by A18, A55, FINSET_1:8, RELAT_1:38, RELAT_1:41;
reconsider N = max C as Element of NAT by ORDINAL1:def 12;
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: now :: thesis: for x being object st x in the carrier of S holds
(Following (s,N)) . x = (Following (Following (s,N))) . x
let x be object ; :: 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 and
A62: 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 A16, A56;
n in C by A16, A55, A60, A61, FUNCT_1:3;
then A63: N >= n by XXREAL_2:def 8;
then A64: N + 1 >= n by NAT_1:13;
thus (Following (s,N)) . x = (Following (s,n)) . x by A62, A63
.= (Following (s,(N + 1))) . x by A62, A64
.= (Following (Following (s,N))) . x by FACIRC_1:12 ; :: thesis: verum
end;
( dom (Following (s,N)) = the carrier of S & dom (Following (Following (s,N))) = the carrier of S ) by CIRCUIT1:3;
hence Following (s,N) = Following (Following (s,N)) by A59, FUNCT_1:2; :: according to CIRCUIT2:def 6 :: thesis: verum