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 (A +* (1GateCircuit (p,f)))
for s9 being State of A st s9 = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s9)
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 (A +* (1GateCircuit (p,f)))
for s9 being State of A st s9 = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s9)
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 (A +* (1GateCircuit (p,f)))
for s9 being State of A st s9 = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s9)
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 (A +* (1GateCircuit (p,f)))
for s9 being State of A st s9 = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s9)
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 (A +* (1GateCircuit (p,f)))
for s9 being State of A st s9 = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s9)
let p be FinSeqLen of n; :: thesis: ( not Output (1GateCircStr (p,f)) in InputVertices S implies for s being State of (A +* (1GateCircuit (p,f)))
for s9 being State of A st s9 = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s9) )
assume A1: not Output (1GateCircStr (p,f)) in InputVertices S ; :: thesis: for s being State of (A +* (1GateCircuit (p,f)))
for s9 being State of A st s9 = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s9)
InnerVertices (1GateCircStr (p,f)) = {(Output (1GateCircStr (p,f)))} by Th16;
then A2: InputVertices S misses InnerVertices (1GateCircStr (p,f)) by A1, ZFMISC_1:50;
let s be State of (A +* (1GateCircuit (p,f))); :: thesis: for s9 being State of A st s9 = s | the carrier of S holds
stabilization-time s <= 1 + (stabilization-time s9)
let s9 be State of A; :: thesis: ( s9 = s | the carrier of S implies stabilization-time s <= 1 + (stabilization-time s9) )
assume A3: s9 = s | the carrier of S ; :: thesis: stabilization-time s <= 1 + (stabilization-time s9)
A tolerates 1GateCircuit (p,f) by Th27;
then the Sorts of A tolerates the Sorts of (1GateCircuit (p,f)) ;
then reconsider s1 = (Following (s,(stabilization-time s9))) | the carrier of (1GateCircStr (p,f)) as State of (1GateCircuit (p,f)) by CIRCCOMB:26;
A4: stabilization-time s1 <= 1 by Th21;
( s9 is stabilizing & s1 is stabilizing ) by Def2;
then stabilization-time s = (stabilization-time s9) + (stabilization-time s1) by A3, A2, Th10, Th27;
hence stabilization-time s <= 1 + (stabilization-time s9) by A4, XREAL_1:6; :: thesis: verum