Aufgaben

• Für E = {aba(x) $\approx$ x} : gilt abbbaa(x) $\approx_{E}^{}$ bba(x) ?
• F = {f (x, f (y, z)) $\approx$ f (f (x, y), z), f (e, x) $\approx$ x, f (i(x), x) $\approx$ e} . Zeige f (x, e) $\approx_{F}^{}$ x .
• G = {f (x, f (y, z)) $\approx$ f (f (x, y), z), f (f (x, y), x) $\approx$ x} . Zeige f (x, x) $\approx_{G}^{}$ x und f (f (x, y), z) $\approx_{G}^{}$ f (x, z)
• H = {f (x, f (y, z)) $\approx$ f (f (x, y), z), f (e, x) $\approx$ x, f (x, i(x)) $\approx$ e} . Zeige f (x, e) $\not\approx$_Hx .

Quellen: http://www.cs.vu.nl/~tcs/trs/,
Franz Baader und Tobias Nipkow: Term Rewriting and All That, http://www21.in.tum.de/~nipkow/TRaAT/

Autotoolisierung dieser Aufgaben? (zwei Fälle)