R
↳Dependency Pair Analysis
REV(++(x, y)) -> ++'(rev(y), rev(x))
REV(++(x, y)) -> REV(y)
REV(++(x, y)) -> REV(x)
++'(.(x, y), z) -> ++'(y, z)
++'(x, ++(y, z)) -> ++'(++(x, y), z)
++'(x, ++(y, z)) -> ++'(x, y)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
++'(x, ++(y, z)) -> ++'(x, y)
++'(x, ++(y, z)) -> ++'(++(x, y), z)
++'(.(x, y), z) -> ++'(y, z)
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)
++'(.(x, y), z) -> ++'(y, z)
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
POL(++'(x1, x2)) = 1 + x1 + x2 POL(++(x1, x2)) = x1 + x2 POL(nil) = 0 POL(.(x1, x2)) = 1 + x1 + x2
++'(x1, x2) -> ++'(x1, x2)
.(x1, x2) -> .(x1, x2)
++(x1, x2) -> ++(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
++'(x, ++(y, z)) -> ++'(x, y)
++'(x, ++(y, z)) -> ++'(++(x, y), z)
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)
++'(x, ++(y, z)) -> ++'(x, y)
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
POL(++'(x1, x2)) = 1 + x1 + x2 POL(++(x1, x2)) = 1 + x1 + x2 POL(nil) = 0 POL(.(x1, x2)) = x1 + x2
++'(x1, x2) -> ++'(x1, x2)
++(x1, x2) -> ++(x1, x2)
.(x1, x2) -> .(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳AFS
...
→DP Problem 4
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
++'(x, ++(y, z)) -> ++'(++(x, y), z)
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)
++'(x, ++(y, z)) -> ++'(++(x, y), z)
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
POL(++(x1, x2)) = 1 + x1 + x2 POL(nil) = 0 POL(.(x1, x2)) = x1 + x2
++'(x1, x2) -> x2
++(x1, x2) -> ++(x1, x2)
.(x1, x2) -> .(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳AFS
...
→DP Problem 5
↳Dependency Graph
→DP Problem 2
↳AFS
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
REV(++(x, y)) -> REV(x)
REV(++(x, y)) -> REV(y)
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)
REV(++(x, y)) -> REV(x)
REV(++(x, y)) -> REV(y)
POL(REV(x1)) = x1 POL(++(x1, x2)) = 1 + x1 + x2
REV(x1) -> REV(x1)
++(x1, x2) -> ++(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 6
↳Dependency Graph
rev(nil) -> nil
rev(rev(x)) -> x
rev(++(x, y)) -> ++(rev(y), rev(x))
++(nil, y) -> y
++(x, nil) -> x
++(.(x, y), z) -> .(x, ++(y, z))
++(x, ++(y, z)) -> ++(++(x, y), z)
make(x) -> .(x, nil)