Term Rewriting System R:
[x, y, z]
.(1, x) -> x
.(x, 1) -> x
.(i(x), x) -> 1
.(x, i(x)) -> 1
.(i(y), .(y, z)) -> z
.(y, .(i(y), z)) -> z
i(1) -> 1
i(i(x)) -> x
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