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
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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( n = depth SCS implies ((Computation (s,InpFs)) . n) . v = IGValue (v,iv) )
assume n = depth SCS ; :: thesis: ((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
hence ((Computation (s,InpFs)) . n) . v = IGValue (v,iv) by A1, A2, Th16; :: thesis: verum