 However, it was found later that describing a program via a recursively defined function with pattern matching is a more natural way of proving than using induction principles directly.Unfortunately, allowing non-terminating definitions leads to logical inconsistency in type theories.That's why Agda and Coq have termination checkers built-in.