let S be non empty finite non void unsplit gate`1=arity gate`2=den ManySortedSign ; 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; ( A is gate`2=den implies A is with_stabilization-limit )
assume A2:
A is gate`2=den
; 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 ;
REWRITE1:def 16 ( 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 <> {}
;
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
;
( 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;
for b1 being object holds
( not b1 in Y or y = b1 or not [y,b1] in R )
let b be
object ;
( 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 )
;
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;
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
A16:
the carrier of S c= field R
dom R c= the carrier of S
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 ;
( ( 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]
;
S3[a]
A23:
for
b being
object st
b in RS holds
ex
z being
object st
S4[
b,
z]
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
;
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 <> {}
;
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
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;
for s being State of A
for m being Element of NAT st m >= n holds
(Following (s,m)) . a = (Following (s,n)) . alet s be
State of
A;
for m being Element of NAT st m >= n holds
(Following (s,m)) . a = (Following (s,n)) . alet m be
Element of
NAT ;
( m >= n implies (Following (s,m)) . a = (Following (s,n)) . a )assume
m >= n
;
(Following (s,m)) . a = (Following (s,n)) . athen 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 ;
( x in rng (the_arity_of a1) implies Following (s,mC) is_stable_at x )
assume A33:
x in rng (the_arity_of a1)
;
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 for k being Nat holds (Following ((Following (s,mC)),k)) . x = (Following (s,mC)) . xlet k be
Nat;
(Following ((Following (s,mC)),k)) . x = (Following (s,mC)) . xA41:
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
;
verum end;
hence
Following (
s,
mC)
is_stable_at x
;
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;
verum end; suppose A43:
RS = {}
;
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)) . atake n = 1;
for s being State of A
for m being Element of NAT st m >= n holds
(Following (s,m)) . a = (Following (s,n)) . alet s be
State of
A;
for m being Element of NAT st m >= n holds
(Following (s,m)) . a = (Following (s,n)) . alet m be
Element of
NAT ;
( m >= n implies (Following (s,m)) . a = (Following (s,n)) . a )assume
m >= n
;
(Following (s,m)) . a = (Following (s,n)) . athen 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 ( a in InnerVertices S implies (Following (s,m)) . a = (Following (s,n)) . a )assume
a in InnerVertices S
;
(Following (s,m)) . a = (Following (s,n)) . athen
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
proof
let x be
set ;
( x in rng (the_arity_of a1) implies s is_stable_at x )
assume A46:
x in rng (the_arity_of a1)
;
s is_stable_at x
a1 = [( the Arity of S . a1),(a1 `2)]
by CIRCCOMB:def 8;
then A47:
a1 = [(the_arity_of a1),(a1 `2)]
by MSUALG_1:def 1;
then
the_rank_of x in the_rank_of a1
by A46, CLASSES1:82;
then A48:
x <> a
;
(
rng (the_arity_of a1) c= the
carrier of
S &
x in proj2 (a `1) )
by A46, A47, FINSEQ_1:def 4;
then A49:
[a1,x] in R
by A1, A27, A46;
then
x in field R
by RELAT_1:15;
hence
s is_stable_at x
by A20, A43, A48, A49;
verum
end; 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;
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;
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]
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
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
; CIRCCMB3:def 3 for s being State of A holds Following (s,N) is stable
let s be State of A; Following (s,N) is stable
A59:
now for x being object st x in the carrier of S holds
(Following (s,N)) . x = (Following (Following (s,N))) . xlet x be
object ;
( x in the carrier of S implies (Following (s,N)) . x = (Following (Following (s,N))) . x )assume A60:
x in the
carrier of
S
;
(Following (s,N)) . x = (Following (Following (s,N))) . xthen 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
;
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; CIRCUIT2:def 6 verum