  We address a problem connected to the unfolding semantics of functional
programming languages: give a useful characterization of those infinite
lambda-terms that are lambda_{letrec}-expressible in the sense that they arise
as infinite unfoldings of terms in lambda_{letrec}, the lambda-calculus with
letrec. We provide two characterizations, using concepts we introduce for
infinite lambda-terms: regularity, strong regularity, and binding-capturing
chains. It turns out that lambda_{letrec}-expressible infinite lambda-terms
form a proper subclass of the regular infinite lambda-terms. In this paper we
establish these characterizations only for expressibility in lambda_{mu}, the
lambda-calculus with explicit mu-recursion. We show that for all infinite
lambda-terms T the following are equivalent: (i): T is lambda_{mu}-expressible;
(ii): T is strongly regular; (iii): T is regular, and it only has finite
binding-capturing chains.
  We define regularity and strong regularity for infinite lambda-terms as two
different generalizations of regularity for infinite first-order terms: as the
existence of only finitely many subterms that are defined as the reducts of two
rewrite relations for decomposing lambda-terms. These rewrite relations act on
infinite lambda-terms furnished with a marked prefix of abstractions for
collecting decomposed lambda-abstractions and keeping the terms closed under
decomposition. They differ in how vacuous abstractions in the prefix are
removed.
  This report accompanies the article with the same title for the proceedings
of the conference RTA 2013, and mainly differs from that by providing the proof
of the characterization of lambda_{mu}-expressibility with binding-capturing
chains.
