A decision procedure for the tape machines would decide $A_TM$: the partial function whose domain is $A_TM$ is partial recursive, so by Turing-completeness one fixed tape machine accepts the unary encoding of $n$ exactly when $n ∈ A_TM$, and the decision procedure applied to that machine and the unary inputs decides $A_TM$ ($Acceptance.tm_acceptance_not_computablyDecidable$). The bridge $computablePred_accepts_iff$ moves between the concept's machines and the source's.

Sipser, Theorem 4.11 for the tape machines of Section 5.2; Lean proof by Aristotle ($RequestProject/Acceptance/Bridge.lean$).