For the definition of a propositional proof system we have:
An abstract proof system is a polynomial time function f whose range is equal to the set of tautologies. If τ is a tautology, then an f-proof of τ is any value π such that f(π)=τ.
In regards to a polynomially-bounded propositional proof system, we have:
If τ is a tautology, then an f-proof of τ is any value π such that f(π)=τ and |π| $ \leq $ f(τ).
My question is in regards to a regular propositional proof system, does the function need to run in polynomial-time relative to any particular value? What is the polynomial in terms of?
Am I understanding it right, that the polynomial can in fact be in terms of any number, whereas a polynomial-bounded proof system would have the polynomial be in terms of the value of the size of the given tautology?