The proof that $E_{TM}$ is unsatisfiable (Theorem 5.2) from Sipser's Introduction to the Theory of Computation constructs a decider for $A_{TM}$ that simulates an arbitrary Turing machine $M$. To me, it seems like this construction is only a decider if we assume that $M$ is also a decider, which we cannot do.
I'm restating the proof as follows to make my questions more concrete (apologies if the proof is not rigorous enough, but hopefully it suffices to make the question clear)
$\textbf{Theorem:}$ $E_{TM}$ is undecidable where $$E_{TM} = \{\langle M \rangle\ |\ M\text{ is a TM and }L(M) = \phi\}$$
$\textbf{Proof:}$ Given $$A_{TM} = \{\langle M, w\rangle\ |\ \text{$M$ is a TM and $M$ accepts $w$}\}$$ Assume that $R$ decides $E_{TM}$ and construct $S$ that decides $A_{TM}$ as follows.
$S = $"On input $\langle M, w\rangle$,
- Using the encoding of $M$ and $w$ construct $M_1$ that works like $M$ for $w$ and rejects all other strings. $M_1 = $"On input $x$: (a) If $x \neq w$, reject. (b) If $x = w$, run $M$ on input $w$ and accept if $M$ does."
- Run $R$ on input $\langle M_1\rangle$.
- If $R$ accepts, reject. If $R$ rejects, accept. Since $R$ decides $E_{TM}$, $S$ decides $A_{TM}$. Because $A_{TM}$ is undecidable, $E_{TM}$ must be undecidable.
Here's my question in terms of the proof above: $R$ is a decider. We're constructing a decider $S$. $S$ creates $M_1$ that runs $M$ on $w$ and accepts if $M$ does. However, we can't make any assumptions about $M$. So although steps 1(a), 2 and 3 halt, step 1(b) is not guaranteed to halt. So we haven't successfully built a decider for $A_{TM}$. We cannot complete the proof by contradiction.
What am I missing here?
