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.

Dependency Pair Analysis

R contains no Dependency Pairs and therefore no SCCs.

Innermost Termination of R successfully shown.
0:00 minutes