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:

• \(((q_T, q_A), \sigma_1, q_1) \in \delta_B\)

• \((q_1, \sigma_2, q_2) \in \delta_B\)

• ...

• \((q_{n - 1}, \sigma_n, (q_T', q_A')) \in \delta_B\)

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.