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 holds iv c= (Computation (s,InpFs)) . k

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 holds iv c= (Computation (s,InpFs)) . k

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 holds iv c= (Computation (s,InpFs)) . k )

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 holds iv c= (Computation (s,InpFs)) . k

A3: dom (commute InpFs) = NAT by A2, PRE_CIRC:5;

let s be State of SCS; :: thesis: for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds

for k being Nat holds iv c= (Computation (s,InpFs)) . k

let iv be InputValues of SCS; :: thesis: ( iv = (commute InpFs) . 0 implies for k being Nat holds iv c= (Computation (s,InpFs)) . k )

assume A4: iv = (commute InpFs) . 0 ; :: thesis: for k being Nat holds iv c= (Computation (s,InpFs)) . k

let k be Nat; :: thesis: iv c= (Computation (s,InpFs)) . k

A5: k in NAT by ORDINAL1:def 12;

IIG is with_input_V by A2;

then A6: k -th_InputValues InpFs = (commute InpFs) . k by CIRCUIT1:def 2

.= iv by A1, A4, A3, FUNCT_1:def 10, A5 ;

set Ck = (Computation (s,InpFs)) . k;

( dom iv = InputVertices IIG & dom (Set-Constants SCS) = SortsWithConstants IIG ) by PARTFUN1:def 2;

then A7: dom iv misses dom (Set-Constants SCS) by MSAFREE2:4;

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 holds iv c= (Computation (s,InpFs)) . k

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 holds iv c= (Computation (s,InpFs)) . k

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 holds iv c= (Computation (s,InpFs)) . k )

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 holds iv c= (Computation (s,InpFs)) . k

A3: dom (commute InpFs) = NAT by A2, PRE_CIRC:5;

let s be State of SCS; :: thesis: for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds

for k being Nat holds iv c= (Computation (s,InpFs)) . k

let iv be InputValues of SCS; :: thesis: ( iv = (commute InpFs) . 0 implies for k being Nat holds iv c= (Computation (s,InpFs)) . k )

assume A4: iv = (commute InpFs) . 0 ; :: thesis: for k being Nat holds iv c= (Computation (s,InpFs)) . k

let k be Nat; :: thesis: iv c= (Computation (s,InpFs)) . k

A5: k in NAT by ORDINAL1:def 12;

IIG is with_input_V by A2;

then A6: k -th_InputValues InpFs = (commute InpFs) . k by CIRCUIT1:def 2

.= iv by A1, A4, A3, FUNCT_1:def 10, A5 ;

set Ck = (Computation (s,InpFs)) . k;

( dom iv = InputVertices IIG & dom (Set-Constants SCS) = SortsWithConstants IIG ) by PARTFUN1:def 2;

then A7: dom iv misses dom (Set-Constants SCS) by MSAFREE2:4;

per cases
( k = 0 or ex n being Nat st k = n + 1 )
by NAT_1:6;

end;

suppose A8:
k = 0
; :: thesis: iv c= (Computation (s,InpFs)) . k

then (Computation (s,InpFs)) . k =
InitialComp (s,InpFs)
by Def9

.= (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) ;

hence iv c= (Computation (s,InpFs)) . k by A6, A7, A8, FUNCT_4:25, FUNCT_4:124; :: thesis: verum

end;.= (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) ;

hence iv c= (Computation (s,InpFs)) . k by A6, A7, A8, FUNCT_4:25, FUNCT_4:124; :: thesis: verum

suppose
ex n being Nat st k = n + 1
; :: thesis: iv c= (Computation (s,InpFs)) . k

then consider n being Nat such that

A9: k = n + 1 ;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

reconsider Cn = (Computation (s,InpFs)) . n as State of SCS ;

(Computation (s,InpFs)) . k = Following (Cn,(k -th_InputValues InpFs)) by A9, Def9

.= Following (Cn +* iv) by A6 ;

hence iv c= (Computation (s,InpFs)) . k by Th12, FUNCT_4:25; :: thesis: verum

end;A9: k = n + 1 ;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

reconsider Cn = (Computation (s,InpFs)) . n as State of SCS ;

(Computation (s,InpFs)) . k = Following (Cn,(k -th_InputValues InpFs)) by A9, Def9

.= Following (Cn +* iv) by A6 ;

hence iv c= (Computation (s,InpFs)) . k by Th12, FUNCT_4:25; :: thesis: verum