  Brotherston and Simpson [citation] have formalized and investigated cyclic
reasoning, reaching the important conclusion that it is at least as powerful as
inductive reasoning (specifically, they showed that each inductive proof can be
translated into a cyclic proof). We add to their investigation by proving the
converse of this result, namely that each inductive proof can be translated
into an inductive one. This, in effect, establishes the equivalence between
first order cyclic and inductive calculi.
