As already mentioned above, however, online proof techniques will in general produce different outputs at different times. Is this worrisome when it comes to ensuring the property of bias-optimality? Not really: since proof techniques are general programs, some of them may compensate `just in the right way' for online Gödel machine state changes that are caused by time-varying inputs and various processes running on the Gödel machine. In particular, some proof techniques may produce appropriate target theorems no matter what's the precise time at which they are started, e.g., by appropriately computing useful values for switchprog and in formula (2) in response to the current , or by waiting for a certain type of repetitive, informative input until it reappears, etc. No matter how proof techniques compute proofs, Method 2.1 has the optimal order of computational complexity in the following sense.
So the method is asymptotically as fast as the fastest (unknown) such proof technique, assuming that the Gödel machine's lifetime is sufficient to absorb the constant factor. In general, however, no method can generate more than a small fraction of the possible proofs, not even Method 2.1, despite its limited optimality properties. For example, each single cycle in principle could already give rise to a whole variety of distinct theorems producible through instruction state2theorem (Item 4 in Section 2.2.1). Most of them will never be generated though, since the instruction itself will typically already consume several cycles.
We observe that BIOPS searches for a provably good switchprog in a near-bias-optimal and asymptotically optimal way, exploiting the fact that proof verification is a simple and fast business. But here the expression `provably good' refers to a typically different and more powerful sense of optimality depending on the Gödel machine's utility function! Compare Section 3.5.2 and note that the total utility of a Gödel machine may be hard to verify--the evaluation may consume its entire lifetime.