@@ -691,21 +691,12 @@ of types with complexity less than or equal to _c(T<sub>ps</sub>)_ is finite and
691
691
exhausted. This time, however, the sequence cannot be extended, because there are no more distinct
692
692
covering sets available to be introduced to avoid dominating an earlier element of the sequence ∎.
693
693
694
- To show that all paths in the tree of implicit expansions are finite we must decompose them into
695
- definitional subpaths as in the previous proof. All nodes are either byname or strict, and so each of
696
- these definitional subpaths consist of zero or more byname nodes each separated by zero or more strict
697
- nodes.
698
-
699
- Call the sequence consisting of only the byname nodes of a definitional subpath, in path order, its
700
- _ byname subpath_ . And call the set of (possibly empty) sequences of strict nodes separating each
701
- byname node its _ strict subpaths_ . By construction, the byname subpath is non-dominating and so by
702
- the lemma above must be finite. Each of the strict subpaths is also non-dominating by construction and
703
- hence also finite. Consequently each of the definitional subpaths are the concatenation of a finite
704
- number of finite byname nodes separated by a finite sequence of strict nodes, which must in turn be
705
- finite.
706
-
707
- Finally, as in the previous proof we rely on ** P3** to show that there are only a finite number of
708
- these finite definitional subpaths and hence that their interleaving must also be finite ∎.
694
+ Finally, as in the previous proof each path in the tree consists of nodes labelled with some element
695
+ of _ D_ and so can be decomposed into an interleaving of definitional subpaths with respect to each of
696
+ those definitions. These definitional subpaths are non-dominating and hence, by the earlier lemma,
697
+ finite. ** P3** asserts that there are only a finite number of these finite paths, so we know that
698
+ their interleaving must also be finite ∎.
699
+
709
700
710
701
#### Motivating example for the covering set based divergence critera
711
702
0 commit comments