This is a Java implementation of the equivariance sub-algorithm used in the equational anti-unification algorithm for nominal terms described in:

• Alexander Baumgartner and Daniele Nantes-Sobrinho, Nominal Anti-Unification Modulo Equational Theories, Preprint submitted to Journal of Logical and Algebraic Methods in Programming, 2025.

The algorithm solves the following problem:

GIVEN:	Pairs of nominal terms s1 ⊑ t1, …, sn ⊑ tn and a freshness context ∇.
FIND:	A permutation π such that ∇ ⊧ s1 = π·t1, …, sn = π·tn, or ⊥ if no such permutation exists.

Input Syntax

In the input 3 disjoint sets of symbols are used: function symbols, atoms and variables. Symbol names can be of arbitrary length.

• If the first letter of the symbol name is within a - e or A - E, then it is an atom.
• If the first letter of the symbol name is within u - z or U - Z, then it is a variables.
• Otherwise it's a function symbol. Function applications of arity zero f() may be written as just f.
• Associative function applications may be written in flattened form. I.e., f(a,b,c) may be used instead of writing f(f(a,b),c).
• The dot "." is used for abstraction.
• The sharp "#" is used for freshness constrains.

Equivariance problem: (Use the semicolon to separate the equations of the system.) a =< b, c =< a Freshness context ∇: Extra atoms: Commutative symbols ℂ: Associative symbols 𝔸: Use branching heuristics:  Aligns arguments of commutative function applications. Branching limit: -1 = no limit Output format: Simple Verbose Progress Debug all   compact Output lines limit: -1 = no limit Start computation

Output