Nominal terms are a term-language used to accurately and expressively represent systems with binding. We present Nominal Algebra (NA), a theory of algebraic equality on nominal terms. Built-in support for binding in the presence of meta-variables allows NA to closely mirror informal mathematical usage and notation, where expressions such as ()or () are common, in which meta-variables () and () explicitly occur in the scope of a variable a. We describe the syntax and semantics of NA, and provide a sound and complete proof system for it. We also give some examples of axioms; other work has considered sets of axioms of particular interest in some detail.
