 Termination check is very important in dependently typed programming language and theorem proving systems like Coq and Agda.These systems use Curry-Howard isomorphism between programs and proofs.Proofs over inductively defined data types were traditionally described using induction principles.