let X be non empty finite set ; :: thesis: for S being finite Signature of X
for A being Circuit of X,S
for n being Element of NAT
for f being Function of n -tuples_on X,X
for p being FinSeqLen of n st not Output (1GateCircStr p,f) in InputVertices S holds
for s being State of
for s' being State of st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s')
let S be finite Signature of X; :: thesis: for A being Circuit of X,S
for n being Element of NAT
for f being Function of n -tuples_on X,X
for p being FinSeqLen of n st not Output (1GateCircStr p,f) in InputVertices S holds
for s being State of
for s' being State of st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s')
let A be Circuit of X,S; :: thesis: for n being Element of NAT
for f being Function of n -tuples_on X,X
for p being FinSeqLen of n st not Output (1GateCircStr p,f) in InputVertices S holds
for s being State of
for s' being State of st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s')
let n be Element of NAT ; :: thesis: for f being Function of n -tuples_on X,X
for p being FinSeqLen of n st not Output (1GateCircStr p,f) in InputVertices S holds
for s being State of
for s' being State of st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s')
let f be Function of n -tuples_on X,X; :: thesis: for p being FinSeqLen of n st not Output (1GateCircStr p,f) in InputVertices S holds
for s being State of
for s' being State of st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s')
let p be FinSeqLen of n; :: thesis: ( not Output (1GateCircStr p,f) in InputVertices S implies for s being State of
for s' being State of st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s') )
assume A1: not Output (1GateCircStr p,f) in InputVertices S ; :: thesis: for s being State of
for s' being State of st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s')
InnerVertices (1GateCircStr p,f) = {(Output (1GateCircStr p,f))} by Th17;
then A2: InputVertices S misses InnerVertices (1GateCircStr p,f) by A1, ZFMISC_1:56;
let s be State of ; :: thesis: for s' being State of st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s')
let s' be State of ; :: thesis: ( s' = s | the carrier of S implies stabilization-time s <= 1 + (stabilization-time s') )
assume A3: s' = s | the carrier of S ; :: thesis: stabilization-time s <= 1 + (stabilization-time s')
A tolerates 1GateCircuit p,f by Th30;
then the Sorts of A tolerates the Sorts of (1GateCircuit p,f) by CIRCCOMB:def 3;
then reconsider s1 = (Following s,(stabilization-time s')) | the carrier of (1GateCircStr p,f) as State of by CIRCCOMB:33;
A4: stabilization-time s1 <= 1 by Th22;
( s' is stabilizing & s1 is stabilizing ) by Def2;
then stabilization-time s = (stabilization-time s') + (stabilization-time s1) by A3, A2, Th11, Th30;
hence stabilization-time s <= 1 + (stabilization-time s') by A4, XREAL_1:8; :: thesis: verum