(My question is not a duplicate of this question.)
Fix a good coding of non-deterministic random-access machines.
For non-negative integers $m$ that code such a machine, let
$\operatorname{states}(m)$ denote the number of internal states in the coded machine.
("hc" stands for "hard-coded".)
Choose some polynomial function $hcpoly$, and let $L$ be the language
$\{\langle m\hspace{.02 in},\hspace{-0.025 in}t,\hspace{-0.02 in}s\hspace{-0.02 in}\rangle \;\; : \;\; m$ codes such a machine and $\:t\leq 2^{hcpoly(\operatorname{states}(m))}\:$ and
there is a sequence of non-deterministic choices which will make that machine
accept the empty string in at most $t$ time without using more than $s$ space$\}\;$.
Is there a MIP protocol for $L\hspace{.02 in}$ in which the provers use not
much more than $t$ time and/or not much more than $s$ space?
That could just mean $\:poly(\hspace{.02 in}\operatorname{length}(\langle m\hspace{.02 in},\hspace{-0.025 in}t,\hspace{-0.02 in}s\hspace{-0.02 in}\rangle))\:$ time and space, although
ideally it would be $\:poly(\operatorname{states}(m))\hspace{-0.03 in}\cdot \hspace{-0.03 in}t\:$ time and $\:poly(\operatorname{states}(m))\hspace{-0.03 in}+\hspace{-0.03 in}s\:$ space.
