let S be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( [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 ; :: thesis: ( 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 ; :: thesis: Following s is_stable_at [p,f]

hence Following s is_stable_at [p,f] by A1, A2, Th19; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( [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 ; :: thesis: ( 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 ; :: thesis: Following s is_stable_at [p,f]

hence Following s is_stable_at [p,f] by A1, A2, Th19; :: thesis: verum