We investigate a Gentzen-style proof system for the first-order μ-calculusbased on cyclic proofs, produced by unfolding fixed point formulasand detecting repeated proof goals. Our system uses explicit ordinalvariables and approximations to support a simple semantic inductiondischarge condition which ensures the well-foundedness of inductivereasoning. As the main result of this paper we propose a new syntacticdischarge condition based on traces and establish its equivalencewith the semantic condition. We give an automata-theoretic reformulationof this condition which is more suitable for practical proofs. Fora detailed comparison with previous work we consider two simpler syntacticconditions and show that they are more restrictive than our new condition.
