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

_{1}[ 0 ]
by NAT_1:3;

thus for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A10, A4); :: thesis: verum

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

A4: now :: thesis: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]

A10:
SS

let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A5: S_{1}[m]
; :: thesis: S_{1}[m + 1]

thus S_{1}[m + 1]
:: thesis: verum

end;assume A5: S

thus S

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)

end;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;

end;

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;.= Following (((Computation (s,InpFs)) . m),((m + 1) -th_InputValues InpFs)) by A8, FUNCT_4:98

.= (Computation (s,InpFs)) . (m + 1) by Def9 ;

:: thesis: verum

thus for m being Nat holds S