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