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 A1: ( commute InpFs is constant & 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
then A2: IIG is with_input_V by MSAFREE2:def 4;
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 A3: n = depth SCS ; :: thesis: (Computation s,InpFs) . n is stable
A4: dom (commute InpFs) = NAT by A1, PRE_CIRC:8;
A5: (n + 1) -th_InputValues InpFs = (commute InpFs) . (n + 1) by A2, CIRCUIT1:def 2
.= (commute InpFs) . 0 by A1, A4, FUNCT_1:def 16 ;
reconsider Cn = (Computation s,InpFs) . n as State of SCS ;
reconsider iv = (commute InpFs) . 0 as InputValues of SCS by A2, CIRCUIT1:2;
A6: iv c= Cn by A1, Th14;
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 x' = x as Vertex of IIG ;
A7: depth x',SCS <= n by A3, CIRCUIT1:18;
then Cn . x' = IGValue x',iv by A1, Th16;
hence Cn . x = Cn1 . x by A1, A7, 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 A5, A6, FUNCT_4:79 ;
:: according to CIRCUIT2:def 6 :: thesis: verum