[colanderman]

See my sibling comment. Decidability by definition does not apply to infinite inputs (i.e., it is a nonsensical question to ask, like "what is the square root of potato?"). Some proof languages like Coq implicitly extend decidability to extend to infinite streams with finite representations (think generative regular expressions or state machines).