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: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; :: 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 10 ;
reconsider Cn1 = (Computation (s,InpFs)) . (n + 1) as State of SCS ;

now :: thesis: ( the carrier of IIG = dom Cn & the carrier of IIG = dom Cn1 & ( for x being object st x in the carrier of IIG holds
Cn . x = Cn1 . x ) )

thus the carrier of IIG = dom Cn by CIRCUIT1:3; :: thesis: ( the carrier of IIG = dom Cn1 & ( for x being object st x in the carrier of IIG holds
Cn . x = Cn1 . x ) )
thus the carrier of IIG = dom Cn1 by CIRCUIT1:3; :: thesis: for x being object st x in the carrier of IIG holds
Cn . x = Cn1 . x
let x be object ; :: 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:17;
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)
.= Following (Cn,((n + 1) -th_InputValues InpFs)) by Def9
.= Following ((Computation (s,InpFs)) . n) by A7, A6, FUNCT_4:98 ;
:: according to CIRCUIT2:def 6 :: thesis: verum