= Solution
For $a\in\{0,1\}$ define a typed transition term $D_a:\sigma\to\sigma$ by a nested Boolean choice:
$$
D_a=\lambda x:\sigma.
eq_\sigma,x,q_0,q_{\delta(q_0,a)}
\bigl(eq_\sigma,x,q_1,q_{\delta(q_1,a)}
\bigl(\cdots(eq_\sigma,x,q_{n-2},q_{\delta(q_{n-2},a)},q_{\delta(q_{n-1},a)})\cdots\bigr)\bigr).
$$
Here a Church Boolean acts as an if-then-else operator. The assumed behavior of $eq_\sigma$ gives $D_aq_i\equiv_\beta q_{\delta(q_i,a)}$.
For $w=a_1\cdots a_k$, put
$$
\mathbf w=\lambda x:\sigma.D_{a_k}(D_{a_{k-1}}(\cdots D_{a_1}x\cdots)),
$$
and use $\mathbf\epsilon=\lambda x.x$. Induction on the word length gives
$$
\mathbf wq_0\equiv_\beta q_{\delta^*(q_0,w)}.
$$
Back to article page
