While studying Termination of term rewriting systems I came across the folowing problem from Baader's book Term Rewriting and All That
$\textbf{My idea:}$
Let $s\rightarrow_R t$, then there exists $p\in Pos(s)$, $l=r \in R$ and a substitution $\sigma$ such that $$s|_p=\sigma(l)$$ $$t=s[\sigma(r)]_p$$ From $s|_p=\sigma(l)$ we have that $|s|_p|_f=|\sigma(l)|_f$.
From $t=s[\sigma(r)]_p$ we have that $|t|_f=|s|_f-|s|_p|_f+|\sigma(r)|_f$.
Thus, $|t|_f=|s|_f+(|\sigma(r)|_f-|\sigma(l)|_f)$. But I can't conclude that $|\sigma(r)|_f-|\sigma(l)|_f\geq0$.
I'm not sure if this is the right aproach for this problem, can someone help me?
At first glance, your approach lacks the consideration of how TRS $R$ is like. The key of this proposition seems that a constant $k$ depends on TRS $R$ and function symbol $f$, and doesn’t depend on terms $s$ and $t$.
If I approach this problem, I would try to determine $k$ for given TRS $R$ and $f$. A constant $k$ probably depends on the maximum number of occurrence of $f$ on lhs minus occurrence of $f$ on rhs of rules (I haven’t tried yet, so this might be wrong).