R
↳Dependency Pair Analysis
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)
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)
MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))
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
++'(.(x, y), z) -> ++'(y, 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
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)
MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))
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
++'(.(x, y), z) -> ++'(y, 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