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 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 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 Nat
for v being Vertex of IIG 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 SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Nat
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv)
let s be State of SCS; :: thesis: for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being 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 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 Nat
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv)
defpred S₁[ Nat] means for v being Vertex of IIG st depth (v,SCS) <= $1 holds
((Computation (s,InpFs)) . $1) . v = IGValue (v,iv);
A4: IIG is with_input_V by A2;
A5: 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 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:18;

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 2;
InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:4;
then not v in SortsWithConstants IIG by A8, XBOOLE_0:3;
then not v in dom (Set-Constants SCS) by PARTFUN1:def 2;
hence ((Computation (s,InpFs)) . 0) . v = (s +* (0 -th_InputValues InpFs)) . v by A7, FUNCT_4:11
.= (0 -th_InputValues InpFs) . v by A8, A9, FUNCT_4:13
.= 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 2;
hence ((Computation (s,InpFs)) . 0) . v = (Set-Constants SCS) . v by A7, FUNCT_4:13
.= IGValue (v,iv) by A10, Th11 ;
:: thesis: verum

end;

end;

end;

A11: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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]
let v be Vertex of IIG; :: 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:5;
A15: (k + 1) -th_InputValues InpFs = (commute InpFs) . (k + 1) by A4, CIRCUIT1:def 2
.= (commute InpFs) . 0 by A1, A14, FUNCT_1:def 10 ;
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:98
.= IGValue (v,iv) by A12, A13, Th13 ; :: thesis: verum

end;

thus for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A11); :: thesis: verum