FSM transducer sequential composition decidability this is a followup/ sequel to this recent question which was answered, this one presumably significantly harder. consider a deterministic FSM transducer $F$ and its mapping $F(x)$ of an input word $x$. define a sequence/ composition of such mappings $x_n = F(\ldots F(x_1))$ where $F^n(x)$ is $n$ sequential mappings of $x$. the sequence terminates if/ "at the point" that $F(x_n)$ is unaccepted (by the FSM transducer). 

now consider/ define a property of such sequences "descending". a FSM sequence $x_i$ is "descending" iff $|x_i| \geq |x_{i + 1}|$ where $|x|$ denotes word length, and for all $i,j$, $x_i \neq x_j$. (by defn all such sequences must be finite/ terminating.)


  question: given an input regular language $L$ and a FSM transducer $F$. is it decidable if all sequences $x_n = F^n(x) = F(\ldots F(x))$ for all $x \in L$ are descending?


a complete answer would be ideal but prefer partial answer(s) to none at all. looking for nontrivial analysis, reduction(s) to known problems, refs to related literature etc.

motivation/ background: a long story, but inspired/ related to investigation of a highly studied open number theory problem. the basic idea is to look for/ formulate a generalized loop invariant function applicable to automated theorem proving.
The problem seems undecidable: consider a transducer $F$ that parses and "executes" a single step of a Turing machine $M$ with the head $H$ on symbol $a$, in state $S$ and with tape content $x[a]by$ where $a,b \in \Sigma; x,y \in \Sigma^*$:

$$\# x \, a \, H\, S \, b \, y \, \# \, w $$

where $w \in \{0,1\}^+$ and it outputs 

$$\# x \, H \, S' \, a'\, b \, y \, \# \, w' $$ 

if the head moves left, i.e. $\sigma(a,S)\to (a',S',L)$ or it outputs

$$\# x \, a' \, b \, H \, S' \, y \, \# \, w' $$ 

if the head moves right, i.e. $\sigma(a,S)\to (a',S',R)$.

$w'$ is simply $w +1$ (binary addition with the LSB on the left) and its "role" is to make $x_{i+1} \neq x_j \forall j \leq i$ as required.

If $M$ halts (when $S'$ is a final state), then $F$ adds an extra $\#$ at the end (i.e. it makes the output ascending) and rejects to stop the sequence; otherwise it accepts and the length is unaltered.

If there is not enough space for a right move of the head then $F$ rejects to stop the sequence.

If there is not enough space for writing $w+1$ (carry overflow on the right), it simply replaces the last digit with $\#$ (to make $x_{i+1} \neq x_i$) and rejects to stop the sequence.

Note that:


$F$ needs only a limited look-ahead buffer (4 symbols) to make the rewrite and also to perform the $w+1$ operation;
the internal states of $F$ embeds the internal states of $M$ so it can simulate the transition function $\sigma$;


Now, consider $M$ on an empty tape; we can use an (infinite) regular language: 

$L = \{ \# \, H \, S_0\, \, 0^+ \# \, 0^+ \}$ 

$M$ halts if and only if $F^n(x)$ is not descending for all $n$, for all $x \in L$

Indeed the only length increase occurs when $F$ runs on $\# \, H \, S_0\, 0^s \, \# \, 0^t$ and $s,t$ are such that $M$ halts in less than  $2^t$ steps using at most $s$ space.