Term Rewriting System R:
[x, y]
(x, x) -> e
(e, x) -> x
(x, .(x, y)) -> y
(/(x, y), x) -> y
/(x, x) -> e
/(x, e) -> x
/(.(y, x), x) -> y
/(x, (y, x)) -> y
.(e, x) -> x
.(x, e) -> x
.(x, (x, y)) -> y
.(/(y, x), x) -> y

Termination of R to be shown.

Dependency Pair Analysis

R contains no Dependency Pairs and therefore no SCCs.

Termination of R successfully shown.
0:00 minutes