The transducers considered here are those Wikipedia calls finite state transducers. The behavior of a transducer $T$, that is, the relation it computes, is written $[T]$: a word $y$ is an output for $x$ iff $x[T]y$.
Question: Is the following problem decidable:
Given: A transducer $T$ and a regular language $L$
Decide: Does it hold that $\forall x \in L$, $\forall y$ a word, $x[T]y$ implies that $|y| \leq |x|$?
I'm looking for nontrivial analysis/solvable subcases, reduction to known problems and/or related refs. (right now not even sure it is decidable in general...?)
Motivation: this problem was inspired by analysis/inquiry into automated theorem proving of number theoretic problems in general and a highly-studied one, Collatz conjecture, in particular.