let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for iv being InputValues of SCS st commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 holds
for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
let SCS be non-empty Circuit of IIG; for InpFs being InputFuncs of SCS
for iv being InputValues of SCS st commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 holds
for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
let InpFs be InputFuncs of SCS; for iv being InputValues of SCS st commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 holds
for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
let iv be InputValues of SCS; ( commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 implies for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv) )
assume A1:
( commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 )
; for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
let s be State of SCS; for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
let v be Vertex of IIG; for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
A2:
depth (v,SCS) <= depth SCS
by CIRCUIT1:17;
let n be Element of NAT ; ( n = depth SCS implies ((Computation (s,InpFs)) . n) . v = IGValue (v,iv) )
assume
n = depth SCS
; ((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
hence
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
by A1, A2, Th16; verum