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 s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable
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 s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable
let InpFs be InputFuncs of SCS; ( commute InpFs is constant & not InputVertices IIG is empty implies for s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable )
assume that
A1:
commute InpFs is constant
and
A2:
not InputVertices IIG is empty
; for s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable
A3:
dom (commute InpFs) = NAT
by A2, PRE_CIRC:5;
A4:
IIG is with_input_V
by A2;
then reconsider iv = (commute InpFs) . 0 as InputValues of SCS by CIRCUIT1:2;
let s be State of SCS; for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable
let n be Element of NAT ; ( n = depth SCS implies (Computation (s,InpFs)) . n is stable )
assume A5:
n = depth SCS
; (Computation (s,InpFs)) . n is stable
reconsider Cn = (Computation (s,InpFs)) . n as State of SCS ;
A6:
iv c= Cn
by A1, A2, Th14;
A7: (n + 1) -th_InputValues InpFs =
(commute InpFs) . (n + 1)
by A4, CIRCUIT1:def 2
.=
(commute InpFs) . 0
by A1, A3, FUNCT_1:def 10
;
reconsider Cn1 = (Computation (s,InpFs)) . (n + 1) as State of SCS ;
hence (Computation (s,InpFs)) . n =
(Computation (s,InpFs)) . (n + 1)
.=
Following (Cn,((n + 1) -th_InputValues InpFs))
by Def9
.=
Following ((Computation (s,InpFs)) . n)
by A7, A6, FUNCT_4:98
;
CIRCUIT2:def 6 verum