let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; 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; 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; ( 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
; 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; 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; ( iv = (commute InpFs) . 0 implies for k being Nat holds iv c= (Computation (s,InpFs)) . k )
assume A4:
iv = (commute InpFs) . 0
; for k being Nat holds iv c= (Computation (s,InpFs)) . k
let k be Nat; 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;