Proposition 21 ([Completion of the interface argument]). If the interface can be implemented at every strongly connected component, then every legal expression of the PTS is strongly normalizing.

Process the finitely many components and apply Proposition 20 ([Advancing one component]). At the end, G_T=_T for every actual type with nonempty profile. Empty-profile actual types are literal sorts, for which this equality already holds by Lemma 16 ([Elementary properties of the tests]). Suppose a typable expression is not strongly normalizing and choose one of least syntax size, among all valid contexts and typings. Its proper syntactic children are typable in the corresponding contexts, including under binders, and so are strongly normalizing. A variable or sort is normal; a product or lambda with strongly normalizing children is strongly normalizing. The expression must therefore be an application f n , with f,n strongly normalizing. Generation types f at a product and n at its domain. Normalize that product, convert these typings, and embed the finite context into Ω . The resulting normal product is an actual type with nonempty profile: it is sorted by correctness of types and cannot be a literal sort. The equality G_T=_T and its one-frame test now give strong normalization of f n , a contradiction. This also handles an empty feasible-profile graph, since the hypothetical application would itself produce a feasible product profile. Finally, every legal expression is typable by validity and correctness of types, or is a literal sort. Literal sorts are normal. Hence the conclusion holds with the full legal-expression and open-context scope.