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
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains no Dependency Pairs and therefore no SCCs.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes