let S be one-gate ManySortedSign ; :: thesis: for A being one-gate Circuit of strict non-empty one-gate
for s being State of holds Following s is stable
let A be one-gate Circuit of strict non-empty one-gate ; :: thesis: for s being State of holds Following s is stable
let s be State of ; :: 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