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:18;
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