In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean.\xa0 I warmly invite ITTC listeners to experiment with the tool themselves.\xa0 The repo is here.\xa0