Let’s have expressions that are composed of elements of $ \mathbb N$ and a limited set of binary operations {$ +,\times,,/$ } and functions {$ \exp, \ln$ }. The expressions are always wellformed and form finite trees, with numbers as leaf nodes and operators as internal nodes, binary operations having two child subexpressions and the functions one. A value of such an expression is interpreted to mean some number in $ \mathbb R$ .
There are two limitations on the structure of the expressions: the divisor (the righthand subexpression) of $ /$ can’t be 0 and the argument of $ \ln$ must be positive.
I have two questions about these kind of expressions:

Is it possible to ensure “soundness” of such an expression, in the sense that the two limitations can be checked in limited time?

is an equality check between two such expressions decidable?
These questions seem to be connected in the sense that if you’re able to check equality of the relevant subexpression to zero, you can decide whether a division parent expression is sound, and it doesn’t seem hard to check whether a subexpression of $ \ln$ is positive or negative if it’s known not to be zero.
I know that equality in $ \mathbb R$ is generally not decidable, whereas equality in algebraic numbers is. However, I wonder how inclusion of {$ \exp, \ln$ } changes the result.
(A side note: I posted an earlier version of a question with similar intent here, but it turned out to have too little thought behind it, and had unnecessary (= not related to the meat of the question) complications with negative logarithms.)