Termination Proof using AProVE

Term Rewriting System R:
[x, y]
app(app(, x), x) -> e
app(app(, e), x) -> x
app(app(, x), app(app(., x), y)) -> y
app(app(, app(app(/, x), y)), x) -> y
app(app(/, x), x) -> e
app(app(/, x), e) -> x
app(app(/, app(app(., y), x)), x) -> y
app(app(/, x), app(app(, y), x)) -> y
app(app(., e), x) -> x
app(app(., x), e) -> x
app(app(., x), app(app(, x), y)) -> y
app(app(., app(app(/, 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.
Duration:
0:00 minutes