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 S_{1}[ 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: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A5, A11); :: thesis: verum

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 S

((Computation (s,InpFs)) . $1) . v = IGValue (v,iv);

A4: IIG is with_input_V by A2;

A5: S

proof

A11:
for k being Nat st S
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)) +* (Set-Constants SCS) ;

end;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)) +* (Set-Constants SCS) ;

per cases
( v in InputVertices IIG or v in SortsWithConstants IIG )
by A6, CIRCUIT1:18;

end;

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 A8, XBOOLE_0:3;

then not v in dom (Set-Constants SCS) by PARTFUN1:def 2;

hence ((Computation (s,InpFs)) . 0) . v = (s +* (0 -th_InputValues InpFs)) . v by A7, FUNCT_4:11

.= (0 -th_InputValues InpFs) . v by A8, A9, FUNCT_4:13

.= iv . v by A4, A3, CIRCUIT1:def 2

.= IGValue (v,iv) by A8, Th10 ;

:: thesis: verum

end;InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:4;

then not v in SortsWithConstants IIG by A8, XBOOLE_0:3;

then not v in dom (Set-Constants SCS) by PARTFUN1:def 2;

hence ((Computation (s,InpFs)) . 0) . v = (s +* (0 -th_InputValues InpFs)) . v by A7, FUNCT_4:11

.= (0 -th_InputValues InpFs) . v by A8, A9, FUNCT_4:13

.= iv . v by A4, A3, CIRCUIT1:def 2

.= IGValue (v,iv) by A8, Th10 ;

:: thesis: verum

suppose A10:
v in SortsWithConstants IIG
; :: thesis: ((Computation (s,InpFs)) . 0) . v = IGValue (v,iv)

then
v in dom (Set-Constants SCS)
by PARTFUN1:def 2;

hence ((Computation (s,InpFs)) . 0) . v = (Set-Constants SCS) . v by A7, FUNCT_4:13

.= IGValue (v,iv) by A10, Th11 ;

:: thesis: verum

end;hence ((Computation (s,InpFs)) . 0) . v = (Set-Constants SCS) . v by A7, FUNCT_4:13

.= IGValue (v,iv) by A10, Th11 ;

:: thesis: verum

S

proof

thus
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

reconsider Ck = (Computation (s,InpFs)) . k as State of SCS ;

assume A12: S_{1}[k]
; :: thesis: S_{1}[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 A2, PRE_CIRC:5;

A15: (k + 1) -th_InputValues InpFs = (commute InpFs) . (k + 1) by A4, CIRCUIT1:def 2

.= (commute InpFs) . 0 by A1, A14, FUNCT_1:def 10 ;

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

.= (Following Ck) . v by A3, A15, A16, FUNCT_4:98

.= IGValue (v,iv) by A12, A13, Th13 ; :: thesis: verum

end;reconsider Ck = (Computation (s,InpFs)) . k as State of SCS ;

assume A12: S

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 A2, PRE_CIRC:5;

A15: (k + 1) -th_InputValues InpFs = (commute InpFs) . (k + 1) by A4, CIRCUIT1:def 2

.= (commute InpFs) . 0 by A1, A14, FUNCT_1:def 10 ;

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

.= (Following Ck) . v by A3, A15, A16, FUNCT_4:98

.= IGValue (v,iv) by A12, A13, Th13 ; :: thesis: verum