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

proof

let v be Vertex of ; :: 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 A6: depth v,SCS = 0 by NAT_1:3;
A7: (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 A6, CIRCUIT1:19;

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

A9: dom (0 -th_InputValues InpFs) = InputVertices IIG by PARTFUN1:def 4;
InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:6;
then not v in SortsWithConstants IIG by A8, XBOOLE_0:3;
then not v in dom (Set-Constants SCS) by PARTFUN1:def 4;
hence ((Computation s,InpFs) . 0 ) . v = (s +* (0 -th_InputValues InpFs)) . v by A7, FUNCT_4:12
.= (0 -th_InputValues InpFs) . v by A8, A9, FUNCT_4:14
.= iv . v by A4, A3, CIRCUIT1:def 2
.= IGValue v,iv by A8, 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 A7, 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 ;
assume A12: S₁[k] ; :: thesis: S₁[k + 1]
let v be Vertex of ; :: thesis: ( depth v,SCS <= k + 1 implies ((Computation s,InpFs) . (k + 1)) . v = IGValue v,iv )
assume A13: depth v,SCS <= k + 1 ; :: thesis: ((Computation s,InpFs) . (k + 1)) . v = IGValue v,iv
A14: dom (commute InpFs) = NAT by A2, PRE_CIRC:8;
A15: (k + 1) -th_InputValues InpFs = (commute InpFs) . (k + 1) by A4, CIRCUIT1:def 2
.= (commute InpFs) . 0 by A1, A14, FUNCT_1:def 16 ;
A16: iv c= Ck by A1, A2, A3, Th14;
thus ((Computation s,InpFs) . (k + 1)) . v = (Following Ck,((k + 1) -th_InputValues InpFs)) . v by Def9
.= (Following Ck) . v by A3, A15, A16, FUNCT_4:79
.= IGValue v,iv by A12, A13, Th13 ; :: thesis: verum

end;

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