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 S₁[ Nat] means ( n <= $1 implies (Computation (s,InpFs)) . n = (Computation (s,InpFs)) . $1 );

A4: now :: thesis: for m being Nat st S₁[m] holds
S₁[m + 1]

let m be 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;
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:5;
(m + 1) -th_InputValues InpFs = (commute InpFs) . (m + 1) by A6, CIRCUIT1:def 2
.= iv by A1, A7, FUNCT_1:def 10 ;
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
.= Following (((Computation (s,InpFs)) . m),((m + 1) -th_InputValues InpFs)) by A8, FUNCT_4:98
.= (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 Nat holds S₁[m] from NAT_1:sch 2(A10, A4); :: thesis: verum