Term Rewriting System R:
[x, y, f, xs]
app(id, x) -> x
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, x), xs)) -> app(app(cons, app(f, x)), app(app(map, f), xs))

Innermost Termination of R to be shown.

`   R`
`     ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

APP(app(map, f), app(app(cons, x), xs)) -> APP(app(cons, app(f, x)), app(app(map, f), xs))
APP(app(map, f), app(app(cons, x), xs)) -> APP(cons, app(f, x))
APP(app(map, f), app(app(cons, x), xs)) -> APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) -> APP(app(map, f), xs)

Furthermore, R contains two SCCs.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Usable Rules (Innermost)`
`       →DP Problem 2`
`         ↳UsableRules`

Dependency Pairs:

APP(app(map, f), app(app(cons, x), xs)) -> APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) -> APP(f, x)

Rules:

app(id, x) -> x
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, x), xs)) -> app(app(cons, app(f, x)), app(app(map, f), xs))

Strategy:

innermost

As we are in the innermost case, we can delete all 5 non-usable-rules.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`           →DP Problem 3`
`             ↳Size-Change Principle`
`       →DP Problem 2`
`         ↳UsableRules`

Dependency Pairs:

APP(app(map, f), app(app(cons, x), xs)) -> APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) -> APP(f, x)

Rule:

none

Strategy:

innermost

We number the DPs as follows:
1. APP(app(map, f), app(app(cons, x), xs)) -> APP(app(map, f), xs)
2. APP(app(map, f), app(app(cons, x), xs)) -> APP(f, x)
and get the following Size-Change Graph(s):
{1, 2} , {1, 2}
1=1
2>2
{1, 2} , {1, 2}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1, 2} , {1, 2}
1>1
2>2
{1, 2} , {1, 2}
1=1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
app(x1, x2) -> app(x1, x2)

We obtain no new DP problems.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳Usable Rules (Innermost)`

Dependency Pair:

Rules:

app(id, x) -> x
app(app(map, f), nil) -> nil
app(app(map, f), app(app(cons, x), xs)) -> app(app(cons, app(f, x)), app(app(map, f), xs))

Strategy:

innermost

As we are in the innermost case, we can delete all 4 non-usable-rules.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`           →DP Problem 4`
`             ↳Modular Removal of Rules`

Dependency Pair:

Rule:

Strategy:

innermost

We have the following set of usable rules:

To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
 POL(0) =  0 POL(s) =  0 POL(APP(x1, x2)) =  1 + x1 + x2 POL(app(x1, x2)) =  x1 + x2 POL(id) =  0 POL(add) =  0

We have the following set D of usable symbols: {APP, app, id, add}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D: