A Variant of HigherOrder AntiUnification
This is a Java implementation of the higherorder antiunification
algorithm described in:

Alexander Baumgartner,
Temur Kutsia,
Jordi Levy,
Mateu Villaret.
A Variant of HigherOrder AntiUnification.
In: F. van Raamsdonk, editor, Proceedings of the 24th International Conference on Rewriting Techniques and Applications, RTA 2013. June 2426, 2013, Eindhoven, The Netherlands. Vol. 21 of the Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl, 2013, 113127.
The algorithm solves the following problem:
GIVEN: 
Higherorder terms t and s. 
FIND: 
A higherorder pattern least general generalization of t and s. 
The antiunification algorithm relies on
a subalgorithm that constructively decides about the existence of a variable renaming such that two lambda terms become alphaequivalent. This subalgorithm can also be
accessed separately.
The algorithm works both for untyped and simplytyped λterms. For
untyped terms, the input should not contain βredexes. For simply typed
terms, the input should be in the ηlong βnormal form.
Input Syntax:

The symbols AZ, az, 19 are allowed for variable names and
function names. Names can be of any length.
 If the first letter of the name is within [u,z] or [U,Z], then it
is a variable.
 The backslash "\" is used for the lambda symbol.
 The colon ":" is used to declare the type.
 The dash "" is used as type constructor.
 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):
 \x.f(x,x) =^= \x.f(a,x)
 \x.f(b,x) =^= \x.f(a,x)
 \x,y.f(f(g(x),y),f(g(y),x)) =^= \x,y.f(h(y,g(x)),h(x,g(y)))
 \x,y.f(x,y) =^= \x,y.f(y,x)
 \y:i2.\z:i3. f:i2i3i1(y,z) =^= \y:i2.\z:i3. x:i3i2i1(z,y)
 \x,y,z.g(f(x,z),f(y,z),f(y,x)) =^= \x,y,z.g(h(y,x),h(x,y),h(z,y))
 \x,y.f(\z.g(z,y),g(x,y)) =^= \x,y.f(\z.h(y,z),h(y,x))
 \x.f(\y.g(x,y),\y.g(y,x)) =^= \x.f(\y.h(x,y,x),\y.h(y,x,y))

