Term Rewriting System R:
[y, x, u, v, z]
merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if((x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Termination of R to be shown.

R
Dependency Pair Analysis

R contains the following Dependency Pairs:

MERGE(.(x, y), .(u, v)) -> IF((x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))
MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)
++'(.(x, y), z) -> ++'(y, z)

Furthermore, R contains two SCCs.

R
DPs
→DP Problem 1
Remaining Obligation(s)
→DP Problem 2
Remaining Obligation(s)

The following remains to be proven:
• Dependency Pairs:

MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)
MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if((x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

• Dependency Pair:

++'(.(x, y), z) -> ++'(y, z)

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if((x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

R
DPs
→DP Problem 1
Remaining Obligation(s)
→DP Problem 2
Remaining Obligation(s)

The following remains to be proven:
• Dependency Pairs:

MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)
MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if((x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

• Dependency Pair:

++'(.(x, y), z) -> ++'(y, z)

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if((x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Termination of R could not be shown.
Duration:
0:00 minutes