  One of the elegant achievements in the history of proof theory is the
characterization of the provably total recursive functions of an arithmetical
theory by its proof-theoretic ordinal as a way to measure the time complexity
of the functions. Unfortunately, the machinery is not sufficiently fine-grained
to be applicable on the weak theories on the one hand and to capture the
bounded functions with bounded definitions of strong theories, on the other. In
this paper, we develop such a machinery to address the bounded theorems of both
strong and weak theories of arithmetic. In the first part, we provide a refined
version of ordinal analysis to capture the feasibly definable and bounded
functions that are provably total in $\mathrm{PA}+\bigcup_{\beta \prec \alpha}
\mathrm{TI}(\prec_{\beta})$, the extension of Peano arithmetic by transfinite
induction up to the ordinals below $\alpha$. Roughly speaking, we identify the
functions as the ones that are computable by a sequence of
$\mathrm{PV}$-provable polynomial time modifications on an initial polynomial
time value, where the computational steps are indexed by the ordinals below
$\alpha$, decreasing by the modifications. In the second part, and choosing $l
\leq k$, we use similar technique to capture the functions with bounded
definitions in the theory $T^k_2$ (resp. $S^k_2$) as the functions computable
by exponentially (resp. polynomially) long sequence of
$\mathrm{PV}_{k-l+1}$-provable reductions between $l$-turn games starting with
an explicit $\mathrm{PV}_{k-l+1}$-provable winning strategy for the first game.
