Unifikation--Algorithmus

mgu(s, t) mathend000# nach Fallunterscheidung

• s mathend000# ist Variable: ...
• t mathend000# ist Variable: symmetrisch
• s = (s₁→s₂) mathend000# und t = (t₁→t₂) mathend000#: ...

mgu :: Term -> Term -> Maybe Substitution