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 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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:8;
A4: IIG is with_input_V by A2, MSAFREE2:def 4;
then reconsider iv = (commute InpFs) . 0 as InputValues of SCS by CIRCUIT1:2;
let s be State of SCS; :: thesis: for n being Element of NAT st n = depth SCS holds
(Computation s,InpFs) . n is stable
let n be Element of NAT ; :: thesis: ( n = depth SCS implies (Computation s,InpFs) . n is stable )
assume A5: n = depth SCS ; :: thesis: (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 16 ;
reconsider Cn1 = (Computation s,InpFs) . (n + 1) as State of SCS ;

now

thus the carrier of IIG = dom Cn by CIRCUIT1:4; :: thesis: ( the carrier of IIG = dom Cn1 & ( for x being set st x in the carrier of IIG holds
Cn . x = Cn1 . x ) )
thus the carrier of IIG = dom Cn1 by CIRCUIT1:4; :: thesis: for x being set st x in the carrier of IIG holds
Cn . x = Cn1 . x
let x be set ; :: thesis: ( x in the carrier of IIG implies Cn . x = Cn1 . x )
assume x in the carrier of IIG ; :: thesis: Cn . x = Cn1 . x
then reconsider x9 = x as Vertex of IIG ;
A8: depth x9,SCS <= n by A5, CIRCUIT1:18;
then Cn . x9 = IGValue x9,iv by A1, A2, Th16;
hence Cn . x = Cn1 . x by A1, A2, A8, Th16, NAT_1:12; :: thesis: verum

end;

hence (Computation s,InpFs) . n = (Computation s,InpFs) . (n + 1) by FUNCT_1:9
.= Following Cn,((n + 1) -th_InputValues InpFs) by Def9
.= Following ((Computation s,InpFs) . n) by A7, A6, FUNCT_4:79 ;
:: according to CIRCUIT2:def 6 :: thesis: verum