For any transducer \(T = (Q_T, \Sigma, \delta_T, q_{0, T}, F_T)\) and FA \(A = (Q_A, \Sigma, \delta_A, q_{0, A}, F_A)\), we can construct a FA \(B = (Q_B, \Sigma, \delta_B, q_{0, B}, F_B)\) which satisfies \(L (B) =\operatorname{Post}_T (A)\) as follows:

\(Q_B = (Q_T \times Q_A) \cup S\), where S contains all the fresh intermediate states which are introduced below.

The initial state \(q_{0, B}\) is \((q_{0, T}, q_{0, A})\), and \(F_B\) contains states of the form \((q_T, q_A)\) which satisfies \(q_T \in F_T \wedge q_A \in F_A\).

For any tuple \((q_T, a, w, q_T') \in \delta_T\), and any \((q_A, a, q_A') \in \delta_A\):

Suppose \(w = \sigma_1 \ldots \sigma_n\), then we add \(n - 1\) fresh states to \(Q_B\), which we label by \(q_1, \ldots, q_{n - 1}\). Then we have:

Note that the input 'a' is not used in the construction, but it is crucial that the transitions in T and A have the same input character.