Review of need for termination analysis for recursive functions on inductive datatypes.\xa0 Discussion of a serious problem with syntactic termination checks, namely noncompositionality.\xa0 A function may pass the syntactic termination check, but abstracting part of it out into a helper function may result in code which no longer passes the check.\xa0 So we need a compositional termination check, which will be discussed in subsequent episodes.