Mechanically certifying formula-based Noetherian induction reasoning

In practice, the methodology has been implemented to automatically certify implicit induction proofs generated by the SPIKE theorem prover as well as reductive-free cyclic proofs built by the same system but in a less automatic way.