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 S1[ 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: S1[ 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)) +* () ;
per cases ( v in InputVertices IIG or v in SortsWithConstants IIG ) by ;
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 ;
then not v in dom () by PARTFUN1:def 2;
hence ((Computation (s,InpFs)) . 0) . v = (s +* (0 -th_InputValues InpFs)) . v by
.= (0 -th_InputValues InpFs) . v by
.= iv . v by
.= IGValue (v,iv) by ;
:: thesis: verum
end;
suppose A10: v in SortsWithConstants IIG ; :: thesis: ((Computation (s,InpFs)) . 0) . v = IGValue (v,iv)
then v in dom () by PARTFUN1:def 2;
hence ((Computation (s,InpFs)) . 0) . v = () . v by
.= IGValue (v,iv) by ;
:: thesis: verum
end;
end;
end;
A11: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
reconsider Ck = (Computation (s,InpFs)) . k as State of SCS ;
assume A12: S1[k] ; :: thesis: S1[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 ;
A15: (k + 1) -th_InputValues InpFs = (commute InpFs) . (k + 1) by
.= (commute InpFs) . 0 by ;
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
.= () . v by
.= IGValue (v,iv) by ; :: thesis: verum
end;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A5, A11); :: thesis: verum