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 iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth v,SCS <= k holds
((Computation s,InpFs) . k) . v = IGValue v,iv
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 iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth v,SCS <= k holds
((Computation s,InpFs) . k) . v = IGValue v,iv
let InpFs be InputFuncs of SCS; :: thesis: ( commute InpFs is constant & not InputVertices IIG is empty implies for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth v,SCS <= k holds
((Computation s,InpFs) . k) . v = IGValue v,iv )
assume A1: ( commute InpFs is constant & not InputVertices IIG is empty ) ; :: thesis: for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth v,SCS <= k holds
((Computation s,InpFs) . k) . v = IGValue v,iv
then A2: IIG is with_input_V by MSAFREE2:def 4;
let s be State of SCS; :: thesis: for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth v,SCS <= k holds
((Computation s,InpFs) . k) . v = IGValue v,iv
let iv be InputValues of SCS; :: thesis: ( iv = (commute InpFs) . 0 implies for k being Element of NAT
for v being Vertex of IIG st depth v,SCS <= k holds
((Computation s,InpFs) . k) . v = IGValue v,iv )
assume A3: iv = (commute InpFs) . 0 ; :: thesis: for k being Element of NAT
for v being Vertex of IIG st depth v,SCS <= k holds
((Computation s,InpFs) . k) . v = IGValue v,iv
defpred S₁[ Element of NAT ] means for v being Vertex of IIG st depth v,SCS <= $1 holds
((Computation s,InpFs) . $1) . v = IGValue v,iv;
A4: S₁[ 0 ]

proof

let v be Vertex of IIG; :: thesis: ( depth v,SCS <= 0 implies ((Computation s,InpFs) . 0 ) . v = IGValue v,iv )
assume depth v,SCS <= 0 ; :: thesis: ((Computation s,InpFs) . 0 ) . v = IGValue v,iv
then A5: depth v,SCS = 0 by NAT_1:3;
A6: (Computation s,InpFs) . 0 = InitialComp s,InpFs by Def9
.= (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) ;

per cases ( v in InputVertices IIG or v in SortsWithConstants IIG ) by A5, CIRCUIT1:19;

suppose A7: v in InputVertices IIG ; :: thesis: ((Computation s,InpFs) . 0 ) . v = IGValue v,iv

InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:6;
then not v in SortsWithConstants IIG by A7, XBOOLE_0:3;
then A8: not v in dom (Set-Constants SCS) by PARTFUN1:def 4;
A9: dom (0 -th_InputValues InpFs) = InputVertices IIG by PARTFUN1:def 4;
thus ((Computation s,InpFs) . 0 ) . v = (s +* (0 -th_InputValues InpFs)) . v by A6, A8, FUNCT_4:12
.= (0 -th_InputValues InpFs) . v by A7, A9, FUNCT_4:14
.= iv . v by A2, A3, CIRCUIT1:def 2
.= IGValue v,iv by A7, Th10 ; :: thesis: verum

end;

suppose A10: v in SortsWithConstants IIG ; :: thesis: ((Computation s,InpFs) . 0 ) . v = IGValue v,iv

then v in dom (Set-Constants SCS) by PARTFUN1:def 4;
hence ((Computation s,InpFs) . 0 ) . v = (Set-Constants SCS) . v by A6, FUNCT_4:14
.= IGValue v,iv by A10, Th11 ;
:: thesis: verum

end;

end;

end;

A11: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider Ck = (Computation s,InpFs) . k as State of SCS ;
assume A12: S₁[k] ; :: thesis: S₁[k + 1]
A13: dom (commute InpFs) = NAT by A1, PRE_CIRC:8;
A14: (k + 1) -th_InputValues InpFs = (commute InpFs) . (k + 1) by A2, CIRCUIT1:def 2
.= (commute InpFs) . 0 by A1, A13, FUNCT_1:def 16 ;
A15: iv c= Ck by A1, A3, Th14;
let v be Vertex of IIG; :: thesis: ( depth v,SCS <= k + 1 implies ((Computation s,InpFs) . (k + 1)) . v = IGValue v,iv )
assume A16: depth v,SCS <= k + 1 ; :: thesis: ((Computation s,InpFs) . (k + 1)) . v = IGValue v,iv
thus ((Computation s,InpFs) . (k + 1)) . v = (Following Ck,((k + 1) -th_InputValues InpFs)) . v by Def9
.= (Following Ck) . v by A3, A14, A15, FUNCT_4:79
.= IGValue v,iv by A12, A16, Th13 ; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A11); :: thesis: verum