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 st not Output (1GateCircStr p,f) in InputVertices S holds
for s being State of (A +* (1GateCircuit p,f))
for s' being State of A 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 st not Output (1GateCircStr p,f) in InputVertices S holds
for s being State of (A +* (1GateCircuit p,f))
for s' being State of A 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 st not Output (1GateCircStr p,f) in InputVertices S holds
for s being State of (A +* (1GateCircuit p,f))
for s' being State of A 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 st not Output (1GateCircStr p,f) in InputVertices S holds
for s being State of (A +* (1GateCircuit p,f))
for s' being State of A 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 st not Output (1GateCircStr p,f) in InputVertices S holds
for s being State of (A +* (1GateCircuit p,f))
for s' being State of A st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s')
let p be FinSeqLen of ; :: thesis: ( not Output (1GateCircStr p,f) in InputVertices S implies for s being State of (A +* (1GateCircuit p,f))
for s' being State of A 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 (A +* (1GateCircuit p,f))
for s' being State of A st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s')
let s be State of (A +* (1GateCircuit p,f)); :: thesis: for s' being State of A st s' = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s')
let s' be State of A; :: thesis: ( s' = s | the carrier of S implies stabilization-time s <= 1 + (stabilization-time s') )
assume A2: 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 (1GateCircuit p,f) by CIRCCOMB:33;
A3: stabilization-time s1 <= 1 by Th22;
A4: ( s' is stabilizing & s1 is stabilizing ) by Def2;
InnerVertices (1GateCircStr p,f) = {(Output (1GateCircStr p,f))} by Th17;
then InputVertices S misses InnerVertices (1GateCircStr p,f) by A1, ZFMISC_1:56;
then stabilization-time s = (stabilization-time s') + (stabilization-time s1) by A2, A4, Th11, Th30;
hence stabilization-time s <= 1 + (stabilization-time s') by A3, XREAL_1:8; :: thesis: verum