The provably terminating operations of the subsystem PETJ of explicit mathematics
Keywords: ریاضیات صریح; 03D15; 03D75; 03H15; Explicit mathematics; Polytime functions; Non-standard models;