Bounding Queries Made by a Computation

This file defines a predicate IsQueryBound oa qb to say that a computation with oracles spec never makes a larger number of queries than is given by a bound qb : spec.ι → ℕ. This is useful for showing that some simulated computation is polynomial time, and in things like seeding query values for a computation.

We also define a function minimalQueryBound oa that returns the smallest such count. Calculating this is generally expensive, and so it shouldn't be used in actual algorithms, but it can be useful in some proofs that only care about the existence of a bound.