  Automata operating on infinite objects feature prominently in the theory of
the modal $\mu$-calculus. One such application concerns the tableau games
introduced by Niwi\'{n}ski & Walukiewicz, of which the winning condition for
infinite plays can be naturally checked by a nondeterministic parity stream
automaton. Inspired by work of Jungteerapanich and Stirling we show how
determinization constructions of this automaton may be used to directly obtain
proof systems for the $\mu$-calculus. More concretely, we introduce a binary
tree construction for determinizing nondeterministic parity stream automata.
Using this construction we define the annotated cyclic proof system
$\mathsf{BT}$, where formulas are annotated by tuples of binary strings.
Soundness and Completeness of this system follow almost immediately from the
correctness of the determinization method.
