# A proof theoretic study of abstract termination principles

## TL;DR

This paper provides a proof theoretic analysis of termination principles for recursive path orders, deriving bounds on derivation tree sizes and complexity, applicable to term rewrite systems.

## Contribution

It introduces a general termination principle and extracts subrecursive bounds using G"odel's system T plus bar recursion, linking proof theory with complexity analysis.

## Key findings

- Derived subrecursive bounds on derivation tree sizes
- Analyzed the complexity of these bounds within G"odel's system T plus bar recursion
- Applied the results to bound derivational complexity of term rewrite systems

## Abstract

We carry out a proof theoretic analysis of the wellfoundedness of recursive path orders in an abstract setting. We outline a very general termination principle and extract from its wellfoundedness proof subrecursive bounds on the size of derivation trees which can be defined in G\"{o}del's system T plus bar recursion. We then carry out a complexity analysis of these terms, and demonstrate how this can be applied to bound the derivational complexity of term rewrite systems.