Term Rewriting System R:
[x]
app(app(f, x), app(g, x)) -> app(app(f, 1), app(g, x))
app(g, 1) -> app(g, 0)
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
APP(app(f, x), app(g, x)) -> APP(app(f, 1), app(g, x))
APP(app(f, x), app(g, x)) -> APP(f, 1)
APP(g, 1) -> APP(g, 0)
R contains no SCCs.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes