 Note that this procedure implies finding a normal form for "M".If "M" has a normal form, the Böhm tree is finite and has a simple correspondence to the normal form.If "M" does not have a normal form, the procedure may "grow" some subtrees infinitely, or it may get "stuck in a loop" attempting to produce a result for part of the tree, which is the source of unlabeled leaf nodes.