let S be one-gate ManySortedSign ; :: thesis: for A being one-gate Circuit of S
for s being State of A holds Following s is stable
let A be one-gate Circuit of S; :: thesis: for s being State of A holds Following s is stable
let s be State of A; :: thesis: Following s is stable
ex X being non empty finite set ex n being Element of NAT ex p being FinSeqLen of n ex f being Function of (n -tuples_on X),X st
( S = 1GateCircStr (p,f) & A = 1GateCircuit (p,f) ) by Def7;
hence Following s is stable by CIRCCMB2:2; :: thesis: verum