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
for s being State of SCS
for n being Element of NAT st commute InpFs is constant & not InputVertices IIG is empty & (Computation s,InpFs) . n is stable holds
for m being Element of NAT st n <= m holds
(Computation s,InpFs) . n = (Computation s,InpFs) . m
let SCS be non-empty Circuit of IIG; :: thesis: for InpFs being InputFuncs of SCS
for s being State of SCS
for n being Element of NAT st commute InpFs is constant & not InputVertices IIG is empty & (Computation s,InpFs) . n is stable holds
for m being Element of NAT st n <= m holds
(Computation s,InpFs) . n = (Computation s,InpFs) . m
let InpFs be InputFuncs of SCS; :: thesis: for s being State of SCS
for n being Element of NAT st commute InpFs is constant & not InputVertices IIG is empty & (Computation s,InpFs) . n is stable holds
for m being Element of NAT st n <= m holds
(Computation s,InpFs) . n = (Computation s,InpFs) . m
let s be State of SCS; :: thesis: for n being Element of NAT st commute InpFs is constant & not InputVertices IIG is empty & (Computation s,InpFs) . n is stable holds
for m being Element of NAT st n <= m holds
(Computation s,InpFs) . n = (Computation s,InpFs) . m
let n be Element of NAT ; :: thesis: ( commute InpFs is constant & not InputVertices IIG is empty & (Computation s,InpFs) . n is stable implies for m being Element of NAT st n <= m holds
(Computation s,InpFs) . n = (Computation s,InpFs) . m )
assume that
A1: commute InpFs is constant and
A2: not InputVertices IIG is empty and
A3: (Computation s,InpFs) . n is stable ; :: thesis: for m being Element of NAT st n <= m holds
(Computation s,InpFs) . n = (Computation s,InpFs) . m
defpred S₁[ Element of NAT ] means ( n <= $1 implies (Computation s,InpFs) . n = (Computation s,InpFs) . $1 );

A4: now

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: S₁[m] ; :: thesis: S₁[m + 1]
thus S₁[m + 1] :: thesis: verum

proof

A6: IIG is with_input_V by A2, MSAFREE2:def 4;
then reconsider iv = (commute InpFs) . 0 as InputValues of SCS by CIRCUIT1:2;
reconsider Ckm = (Computation s,InpFs) . m as State of SCS ;
A7: dom (commute InpFs) = NAT by A2, PRE_CIRC:8;
(m + 1) -th_InputValues InpFs = (commute InpFs) . (m + 1) by A6, CIRCUIT1:def 2
.= iv by A1, A7, FUNCT_1:def 16 ;
then A8: (m + 1) -th_InputValues InpFs c= (Computation s,InpFs) . m by A1, A2, Th14;
assume A9: n <= m + 1 ; :: thesis: (Computation s,InpFs) . n = (Computation s,InpFs) . (m + 1)

per cases ( n <= m or n = m + 1 ) by A9, NAT_1:8;

suppose n <= m ; :: thesis: (Computation s,InpFs) . n = (Computation s,InpFs) . (m + 1)

hence (Computation s,InpFs) . n = Following Ckm by A3, A5, Def6
.= Following ((Computation s,InpFs) . m),((m + 1) -th_InputValues InpFs) by A8, FUNCT_4:79
.= (Computation s,InpFs) . (m + 1) by Def9 ;
:: thesis: verum

end;

suppose n = m + 1 ; :: thesis: (Computation s,InpFs) . n = (Computation s,InpFs) . (m + 1)

hence (Computation s,InpFs) . n = (Computation s,InpFs) . (m + 1) ; :: thesis: verum

end;

end;

end;

end;

A10: S₁[ 0 ] by NAT_1:3;
thus for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A10, A4); :: thesis: verum