An analysis of the Podelski–Rybalchenko termination theorem via bar recursion

We present an effective proof (with explicit bounds) of the Podelski and Rybalchenko Termination Theorem. The sub-recursive bounds we obtain make use of bar recursion, in the form of the product of selection functions, as this is used to interpret the Weak Ramsey Theorem for pairs. The construction can be seen as calculating a modulus of well-foundedness for a given program given moduli of well-foundedness for the disjunctively well-founded finite set of covering relations. When the input moduli are in system T, this modulus is also definable in system T by a result of Schwichtenberg on bar recursion.