 Admissible predicate on lazy lists

A predicate on possibly partial lists is admissible when it holds at the limit of every increasing chain of finite approximations on which it holds. Increasing here means replacing a bottom value by more defined information while retaining already defined constructors and values. This closure condition permits a property established for finite approximations to pass to an infinite list. The predicate “the list is finite” lacks this closure: every finite prefix ending in an undefined tail is finite in extent, but their limit may have infinitely many constructors.