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 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 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 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 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 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 Nat st n <= m holds
(Computation (s,InpFs)) . n = (Computation (s,InpFs)) . m

defpred S1[ Nat] means ( n <= \$1 implies (Computation (s,InpFs)) . n = (Computation (s,InpFs)) . \$1 );
A4: now :: thesis: for m being Nat st S1[m] holds
S1[m + 1]
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A5: S1[m] ; :: thesis: S1[m + 1]
thus S1[m + 1] :: thesis: verum
proof
A6: IIG is with_input_V by A2;
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 ;
(m + 1) -th_InputValues InpFs = (commute InpFs) . (m + 1) by
.= iv by ;
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 ;
suppose n <= m ; :: thesis: (Computation (s,InpFs)) . n = (Computation (s,InpFs)) . (m + 1)
hence (Computation (s,InpFs)) . n = Following Ckm by A3, A5
.= Following (((Computation (s,InpFs)) . m),((m + 1) -th_InputValues InpFs)) by
.= (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: S1[ 0 ] by NAT_1:3;
thus for m being Nat holds S1[m] from NAT_1:sch 2(A10, A4); :: thesis: verum