  A sound and complete algorithm for nominal unification of higher-order
expressions with a recursive let is described, and shown to run in
nondeterministic polynomial time. We also explore specializations like nominal
letrec-matching for expressions, for DAGs, and for garbage-free expressions and
determine their complexity. Finally, we also provide a nominal unification
algorithm for higher-order expressions with recursive let and atom-variables,
where we show that it also runs in nondeterministic polynomial time.
