:: deftheorem defines -th_InputValues CIRCUIT1:def 2 :
for IIG being non empty non void Circuit-like ManySortedSign st IIG is with_input_V holds
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for n being Nat holds n -th_InputValues InpFs = (commute InpFs) . n;