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

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