Nominal Equivariance
This is a Java implementation of the equivariance
algorithm for nominal terms described in:

Alexander Baumgartner,
Temur Kutsia,
Jordi Levy,
Mateu Villaret.
Nominal AntiUnification.
In: M. Fernández, editor, Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA 2015. June 29–July 3, 2015, Warsaw, Poland. Vol. 36 of the Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl, 2015, 57–73.
Part of the Library of Unification and AntiUnification Algorithms.
The algorithm solves the following problem:
GIVEN: 
A set of of atoms A, nominal equivariance equations of the form t ≈ s and a freshness context ∇, all based on A. 
FIND: 
An Abased permutation π, such that π(t) is alpha equivalent to s under ∇ for all equations. 
The equivariance algorithm is a part of an algorithm which solves the nominal antiunification problem.
This
antiunification algorithm has also been implemented and is available online.
Input Syntax:

The symbols AZ, az, 19 are allowed for atom names,
function names, variable names and sort names. Names can be of any length.
 If the first letter of the name is within [a,e] or [A,E], then it
is an atom.
 If the first letter of the name is within [u,z] or [U,Z], then it
is a variable.
 Otherwise it is a function symbol. The application of a function with arity zero f() may be written as just f.
 The dot "." is used for abstraction.
 The colon ":" is used to declare the sorts.
 If a sort name starts with a capital letter, then it is of sort data.
 The dash "" is used as type constructor.
 The sharp "#" is used for freshness constrains.
 Mixed mode of typed and untyped calculus is allowed.
This software is released under the GNU Lesser General Public License ("LGPL").
For presentation purpose, the Java source code has been translated into JavaScript by the GWT compiler.
Some examples (click on them to prepared the input form):
 c = a; g(c, b, a) = g(a, c, b)
 a = b; b = c)
 g(a, b, a) = g(a, c, b); c = a
 a.f(a,b) = b.f(b,a)
 a.f(a,c) = b.f(b,c); a = d
 a.f(a,a) = a.f(a,b); a = b
 a.b.f(a,b) = b.a.f(b,a)
 a.a.b.f(a,b) = a.b.b.f(a,b)
 a.a.b.f(a,b) = b.a.b.f(a,b)
 a.a.b.f(a,b) = c.b.a.f(b,a)
 a.X = b.X with nabla {a#X}
 a.(a b)X = b.X
 a.(a b)X = b.X with nabla {a#X}
 a.(a b)X = b.X; a = b with nabla {a#X}
 (a b)X = X with nabla {a#X, b#X}
 (a b)X = X
 a.(a b)(c d)X = b.X with nabla {a#X}
 a.f(b, X) = b.f(a, X) with nabla {a#X}
 a.f(b, (a b)X) = b.f(a, X) with nabla {a#X}
 (a b)X = (a b)X; b = c with nabla {a#X, c#X}

