let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s1, s2 being State of SCS holds (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
let SCS be non-empty Circuit of IIG; for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s1, s2 being State of SCS holds (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
let InpFs be InputFuncs of SCS; ( commute InpFs is constant & not InputVertices IIG is empty implies for s1, s2 being State of SCS holds (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS) )
assume that
A1:
commute InpFs is constant
and
A2:
not InputVertices IIG is empty
; for s1, s2 being State of SCS holds (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
IIG is with_input_V
by A2;
then reconsider iv = (commute InpFs) . 0 as InputValues of SCS by CIRCUIT1:2;
reconsider dSCS = depth SCS as Element of NAT by ORDINAL1:def 12;
let s1, s2 be State of SCS; (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
reconsider Cs1 = (Computation (s1,InpFs)) . dSCS as State of SCS ;
reconsider Cs2 = (Computation (s2,InpFs)) . dSCS as State of SCS ;
hence
(Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
; verum