The provably terminating operations of the subsystem of explicit mathematics

In Spescha and Strahm (2009) [15], a system PET of explicit mathematics in the style of Feferman (1975, 1978) [6,7] is introduced, and in Spescha and Strahm (in press) [16] the addition of the join principle to PET is studied. Changing to intuitionistic logic, it could be shown that the provably terminating operations of PETJ i are the polytime functions on binary words. However, although strongly conjectured, it remained open whether the same holds true for the corresponding theory PETJ with classical logic. This note supplements a proof of this conjecture.