let S be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; for A being non-empty gate`2=den Boolean Circuit of S
for s being State of A
for p being FinSequence
for f being Function st [p,f] in the carrier' of S & ( for x being set st x in rng p holds
s is_stable_at x ) holds
Following s is_stable_at [p,f]
let A be non-empty gate`2=den Boolean Circuit of S; for s being State of A
for p being FinSequence
for f being Function st [p,f] in the carrier' of S & ( for x being set st x in rng p holds
s is_stable_at x ) holds
Following s is_stable_at [p,f]
let s be State of A; for p being FinSequence
for f being Function st [p,f] in the carrier' of S & ( for x being set st x in rng p holds
s is_stable_at x ) holds
Following s is_stable_at [p,f]
let p be FinSequence; for f being Function st [p,f] in the carrier' of S & ( for x being set st x in rng p holds
s is_stable_at x ) holds
Following s is_stable_at [p,f]
let f be Function; ( [p,f] in the carrier' of S & ( for x being set st x in rng p holds
s is_stable_at x ) implies Following s is_stable_at [p,f] )
assume
[p,f] in the carrier' of S
; ( ex x being set st
( x in rng p & not s is_stable_at x ) or Following s is_stable_at [p,f] )
then reconsider g = [p,f] as Gate of S ;
A1: the_arity_of g =
the Arity of S . g
by MSUALG_1:def 1
.=
[( the Arity of S . g),(g `2)] `1
.=
g `1
by CIRCCOMB:def 8
.=
p
;
A2: the_result_sort_of g =
the ResultSort of S . g
by MSUALG_1:def 2
.=
g
by CIRCCOMB:44
;
assume
for x being set st x in rng p holds
s is_stable_at x
; Following s is_stable_at [p,f]
hence
Following s is_stable_at [p,f]
by A1, A2, Th19; verum