let S be one-gate ManySortedSign ; :: thesis: for A being one-gate Circuit of S
for s being State of A holds stabilization-time s <= 1
let A be one-gate Circuit of S; :: thesis: for s being State of A holds stabilization-time s <= 1
let s be State of A; :: thesis: stabilization-time s <= 1
Following s is stable by Th19;
then A1: Following (s,1) is stable by FACIRC_1:14;
s is stabilizing by Def2;
hence stabilization-time s <= 1 by A1, Def5; :: thesis: verum