let S be one-gate ManySortedSign ; :: thesis: for A being one-gate Circuit of strict non-empty stabilizing with_stabilization-limit one-gate
for s being State of holds stabilization-time s <= 1
let A be one-gate Circuit of strict non-empty stabilizing with_stabilization-limit one-gate ; :: thesis: for s being State of holds stabilization-time s <= 1
let s be State of ; :: thesis: stabilization-time s <= 1
Following s is stable by Th20;
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