# Proof that $A_{DFA}$ is decidable in Sipser

It seems like the proof that $$A_{DFA}$$ is decidable in Sipser (2nd ed.) assumes the computation will halt... and hence only really proves that $$A_{DFA}$$ is recognizable.

The language $$A_{DFA}$$ is defined by $$A_{DFA} = \{\langle B, w \rangle \mid B \text{ is a } \mathsf{DFA} \text{ that accepts input string } w \}$$.

Here is the passage (I've bolded the most relevant sentence):

First, let's examine the input $$\langle B, w \rangle$$. It is a representation of a $$\mathsf{DFA}$$ $$B$$ together with a string $$w$$. One reasonable representation of $$B$$ is simply a list of its five components, $$Q$$, $$\Sigma$$, $$\delta$$, $$q_0$$, and $$F$$. When $$M$$ receives its input, $$M$$ first determines whether it properly represents a $$\mathsf{DFA}$$ $$B$$ and a string $$w$$. If not, $$M$$ rejects.

Then $$M$$ carries out the simulation directly. It keeps track of $$B$$'s current state and $$B$$'s current position in the input $$w$$ by writing this information down on its tape. Initially, $$B$$'s current state is $$q_0$$ and $$B$$'s current input position is the leftmost symbol of $$w$$. The states and position are updated according to the specified transition function $$\delta$$. When $$M$$ finishes processing the last symbol of $$w$$, $$M$$ accepts the input if $$B$$ is in an accepting state; $$M$$ rejects the input if $$B$$ is in a nonaccepting state.

Am I missing something or is this proof bogus?

EDIT: Never mind, I think I see my problem. A Turing machine may move back and forth, never halting, but an automaton like $$B$$ given finite input $$w$$ finishes after $$|w|$$ steps, correct? So $$M$$ does halt. Feel free to post an answer explaining this yourself - I don't want anyone to miss out on a chance to answer by me deleting the question. If no one responds within a day, I'll post an answer myself.

The computation will always halt. If $M$ doesn't reject right away, then $B$ is an encoding of a DFA. DFA always halt on any finite input, so the simulation must halt too.