Bounded halting predicate ($B(e,x,t)$)

For a fixed effective machine coding, the predicate that program $e$ on input $x$ halts within $t$ steps is primitive recursive. Code finite configurations, iterate a total single-step function by primitive recursion, and test for the halt state. This supplies a bounded simulation even though the unrestricted halting problem is undecidable.