The provably terminating operations of the subsystem PETJ of explicit mathematics (Q639690)

The paper is devoted to the study of a system PET of explicit mathematics introduced by \textit{D. Spescha} and \textit{T. Strahm} in [Math. Log. Q. 55, No. 3, 245--258 (2009; Zbl 1171.03036)] and of a system PETJ obtained by adding the join principle. In particular the author discusses the problem whether the provably terminating operations of PETJ with classical logic are the polytime functions on binary words (what is the case if the logic is intuitionistic). In the paper a proof of this is supplemented.