A probabilistic Turing machine has finite control and a finite tape alphabet. At each step an independent fair bit selects one of two transition tables. Each transition moves the tape head one square or writes one symbol. Both tables agree on which configurations are terminal. The input is an ordinary binary word, using the type $Lax434930.PolynomialTime.Word$.

A polynomial-time procedure consists of one such machine, a polynomial $p\in\mathbb N[X]$, and an output attached to each control state. Every computation on $x$ must halt within $p(|x|)$ steps. Halted configurations are left fixed, so we may use exactly $p(|x|)$ random bits, including unused bits after termination. For an output event $E$, its probability is the number of bit strings producing an output in $E$, divided by $2^{p(|x|)}$. All machines and bounds are chosen uniformly, before the input.