 Pointwise running-time domination problem

Give a nonhalting Turing machine computation halting time infinity. The formal language of pairs satisfying the displayed inequality is a co-recursively enumerable language but is not a recursively enumerable language. A violation has a finite witness: $N_1$ has halted on some input after $t$ moves while $N_2$ has not halted by that time. For the other direction, reduce non-halting by making $N_1$ simulate a fixed computation on every input and making $N_2$ run forever. The pair satisfies domination exactly when the fixed computation never halts. The convention $\infty \ge \infty$ is essential to this many-one reduction.