Bounded simulation of a computation
= Bounded simulation of a computation
A bounded simulation records whether a specified deterministic program has halted, with a specified output, within a given finite number of steps. This is a primitive recursive predicate of the program code, input and time bound. <Peano arithmetic> can verify genuine finite computation certificates and prove that two different outputs cannot both be the first halting output.