let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: (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 ;

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: (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 ;

now :: thesis: ( the carrier of IIG = dom Cs1 & the carrier of IIG = dom Cs2 & ( for x being object st x in the carrier of IIG holds

Cs1 . x = Cs2 . x ) )

hence
(Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
; :: thesis: verumCs1 . x = Cs2 . x ) )

thus
the carrier of IIG = dom Cs1
by CIRCUIT1:3; :: thesis: ( the carrier of IIG = dom Cs2 & ( for x being object st x in the carrier of IIG holds

Cs1 . x = Cs2 . x ) )

thus the carrier of IIG = dom Cs2 by CIRCUIT1:3; :: thesis: for x being object st x in the carrier of IIG holds

Cs1 . x = Cs2 . x

let x be object ; :: thesis: ( x in the carrier of IIG implies Cs1 . x = Cs2 . x )

assume x in the carrier of IIG ; :: thesis: Cs1 . x = Cs2 . x

then reconsider x9 = x as Vertex of IIG ;

Cs1 . x9 = IGValue (x9,iv) by A1, A2, Th17;

hence Cs1 . x = Cs2 . x by A1, A2, Th17; :: thesis: verum

end;Cs1 . x = Cs2 . x ) )

thus the carrier of IIG = dom Cs2 by CIRCUIT1:3; :: thesis: for x being object st x in the carrier of IIG holds

Cs1 . x = Cs2 . x

let x be object ; :: thesis: ( x in the carrier of IIG implies Cs1 . x = Cs2 . x )

assume x in the carrier of IIG ; :: thesis: Cs1 . x = Cs2 . x

then reconsider x9 = x as Vertex of IIG ;

Cs1 . x9 = IGValue (x9,iv) by A1, A2, Th17;

hence Cs1 . x = Cs2 . x by A1, A2, Th17; :: thesis: verum