Strong normalization of barrecursive terms without using infinite terms. Marc Bezem (1985) Archiv für mathematische Logik und Grundlagenforschung