Let $A$ be a set of decision algorithms which are running in polynomial time and which takes natural numbers as inputs.
$x\in A$ if and only if
for $i\in N$
$x(i)=0$ or $x(i)=1$
and running time of $x(i)$ is smaller than $n^k$ ($n$ is digit of $i$)
Now consider a $\mathcal{NP}$ problem for the set $A$.
Problem: "For given $x\in A$, is there any $i\in N$, such that $x(i)=0$?"
For this $\mathcal{NP}$ problem, there is a decider of non-deterministic Turing machine $M$
$$ M(x) = \left\{ \begin{array}{ll} 1\text{ if there exists i∈ N, such that x(i)=0 }\\ 0\text{ otherwise} \end{array} \right. $$
And for this NDTM, there is a verifier of polynomial Deterministic Turing Machine $V$,
$$ V(x,i) = \left\{ \begin{array}{ll} 1\text{ if x(i)=0 }\\ 0\text{ otherwise} \end{array} \right. $$
Question : By the Cook-Levin theorem, I think something can be transformed into a Boolean formula. What is transformed into a Boolean formula?
$M$? $M(x)$? $V$? $V(x)$? $x$? or the NP problem itself?