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 ;
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 ;
set Ck = (Computation (s,InpFs)) . k;
( dom iv = InputVertices IIG & dom () = SortsWithConstants IIG ) by PARTFUN1:def 2;
then A7: dom iv misses dom () by MSAFREE2:4;
per cases ( k = 0 or ex n being Nat st k = n + 1 ) by NAT_1:6;
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)) +* () ;
hence iv c= (Computation (s,InpFs)) . k by ; :: thesis: verum
end;
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
.= Following (Cn +* iv) by A6 ;
hence iv c= (Computation (s,InpFs)) . k by ; :: thesis: verum
end;
end;