R
↳Dependency Pair Analysis
EQ(s(X), s(Y)) -> EQ(X, Y)
RM(N, add(M, X)) -> IFRM(eq(N, M), N, add(M, X))
RM(N, add(M, X)) -> EQ(N, M)
IFRM(true, N, add(M, X)) -> RM(N, X)
IFRM(false, N, add(M, X)) -> RM(N, X)
PURGE(add(N, X)) -> PURGE(rm(N, X))
PURGE(add(N, X)) -> RM(N, X)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
EQ(s(X), s(Y)) -> EQ(X, Y)
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
one new Dependency Pair is created:
EQ(s(X), s(Y)) -> EQ(X, Y)
EQ(s(s(X'')), s(s(Y''))) -> EQ(s(X''), s(Y''))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳Forward Instantiation Transformation
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
EQ(s(s(X'')), s(s(Y''))) -> EQ(s(X''), s(Y''))
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
one new Dependency Pair is created:
EQ(s(s(X'')), s(s(Y''))) -> EQ(s(X''), s(Y''))
EQ(s(s(s(X''''))), s(s(s(Y'''')))) -> EQ(s(s(X'''')), s(s(Y'''')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳FwdInst
...
→DP Problem 5
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
EQ(s(s(s(X''''))), s(s(s(Y'''')))) -> EQ(s(s(X'''')), s(s(Y'''')))
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
EQ(s(s(s(X''''))), s(s(s(Y'''')))) -> EQ(s(s(X'''')), s(s(Y'''')))
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
{nil, purge}
{eq, true}
{rm, ifrm}
{s, false}
EQ(x1, x2) -> EQ(x1, x2)
s(x1) -> s(x1)
eq(x1, x2) -> eq(x1, x2)
rm(x1, x2) -> rm(x1, x2)
add(x1, x2) -> x2
ifrm(x1, x2, x3) -> ifrm(x2, x3)
purge(x1) -> purge
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳FwdInst
...
→DP Problem 6
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳Nar
IFRM(false, N, add(M, X)) -> RM(N, X)
IFRM(true, N, add(M, X)) -> RM(N, X)
RM(N, add(M, X)) -> IFRM(eq(N, M), N, add(M, X))
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
IFRM(false, N, add(M, X)) -> RM(N, X)
IFRM(true, N, add(M, X)) -> RM(N, X)
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
purge > add
{eq, true} > false
IFRM(x1, x2, x3) -> x3
add(x1, x2) -> add(x1, x2)
RM(x1, x2) -> x2
eq(x1, x2) -> eq(x1, x2)
s(x1) -> s(x1)
rm(x1, x2) -> x2
ifrm(x1, x2, x3) -> x3
purge(x1) -> purge(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳AFS
→DP Problem 7
↳Dependency Graph
→DP Problem 3
↳Nar
RM(N, add(M, X)) -> IFRM(eq(N, M), N, add(M, X))
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳AFS
→DP Problem 3
↳Narrowing Transformation
PURGE(add(N, X)) -> PURGE(rm(N, X))
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
two new Dependency Pairs are created:
PURGE(add(N, X)) -> PURGE(rm(N, X))
PURGE(add(N'', nil)) -> PURGE(nil)
PURGE(add(N'', add(M', X''))) -> PURGE(ifrm(eq(N'', M'), N'', add(M', X'')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 8
↳Argument Filtering and Ordering
PURGE(add(N'', add(M', X''))) -> PURGE(ifrm(eq(N'', M'), N'', add(M', X'')))
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
PURGE(add(N'', add(M', X''))) -> PURGE(ifrm(eq(N'', M'), N'', add(M', X'')))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))
{purge, add}
{eq, true}
{0, false}
PURGE(x1) -> PURGE(x1)
add(x1, x2) -> add(x1, x2)
ifrm(x1, x2, x3) -> x3
rm(x1, x2) -> x2
eq(x1, x2) -> eq(x1, x2)
s(x1) -> s(x1)
purge(x1) -> purge(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 8
↳AFS
...
→DP Problem 9
↳Dependency Graph
eq(0, 0) -> true
eq(0, s(X)) -> false
eq(s(X), 0) -> false
eq(s(X), s(Y)) -> eq(X, Y)
rm(N, nil) -> nil
rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
ifrm(true, N, add(M, X)) -> rm(N, X)
ifrm(false, N, add(M, X)) -> add(M, rm(N, X))
purge(nil) -> nil
purge(add(N, X)) -> add(N, purge(rm(N, X)))