Non-terminal symbol Unification

Defining rules for nonterminal symbol Unification:

Unification LhsTerm  INF  RhsTerm

Occurrences of symbol Unification in body of other rules:

Clause Unification  ';'