# On Quasi Ordinal Diagram Systems

## TL;DR

This paper generalizes ordinal diagram systems using recent tree embedding theorems and explores their application in proving termination of complex term rewriting systems, including second-order systems.

## Contribution

It extends Okada-Takeuti's ordinal diagram theory with modern embedding results and discusses their potential for termination proofs in advanced rewriting systems.

## Key findings

- Generalization of ordinal diagram systems using Dershowitz-Tzameret's theorem
- Application of ordinal notation to termination proofs for second-order rewriting
- Potential for ordinal systems to improve termination analysis methods

## Abstract

The purposes of this note are the following two; we first generalize Okada-Takeuti's well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret's version of tree embedding theorem with gap conditions. Second, we discuss possible use of such strong ordinal notation systems for the purpose of a typical traditional termination proof method for term rewriting systems, especially for second-order (pattern-matching-based) rewriting systems including a rewrite-theoretic version of Buchholz's hydra game.