Consider the following extension of polynomials. The rational exponential expressions (REXes) are given by:

1. The leaves 1 and $x$ for $x$ drawn from a class of variables; and
2. Closed under addition, multiplication, exponentiation, and division. This is a restriction to the positive case of a class of expressions studied in Brown, 1969, "Rational Exponential Expressions and a Conjecture Concerning π and e". Buchberger & Loos, 1982, "Algebraic Simplification", sect. 6, mention the existence of algorithms for finding canonical forms for these expressions, but say their correctness depends on number-theoretic conjectures that have not been settled.

I'm interested in a decision procedure for dominance, where for two monomial REXes, $f$ and $g$, $f \leq g$ if $\exists N.\forall n. N \leq n \implies f(n) \leq g(n)$. Do we have either the existence of canonical forms, or decidability for this problem?

Consider the following extension of polynomials. The rational exponential expressions (REXes) are given by:

1. The leaves 1 and $x$ for $x$ drawn from a class of variables; and
2. Closed under the binary functions of addition, multiplication, exponentiation, and division.

This is a restriction to positive constants of a class of expressions studied in Brown, 1969, "Rational Exponential Expressions and a Conjecture Concerning π and e". Buchberger & Loos, 1982, "Algebraic Simplification", sect. 6, mention the existence of algorithms for finding canonical forms for these expressions, but say their correctness depends on number-theoretic conjectures that have not been settled.

I'm interested in a decision procedure for dominance, where for two REXes in one variable, $f$ and $g$, $f \leq g$ if $\exists N \in {\mathbb N}.\forall n \in {\mathbb N}. N \leq n \implies f(n) \leq g(n)$. Do we have either the existence of canonical forms, or decidability for this problem?