Bounded halting predicate (source code)

= Bounded halting predicate
{title2=$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.