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
↳Remaining
→DP Problem 3
↳Remaining
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
↳Remaining
→DP Problem 3
↳Remaining
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
↳Forward Instantiation Transformation
→DP Problem 2
↳Remaining
→DP Problem 3
↳Remaining
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)))
one new Dependency Pair is created:
EQ(s(s(s(X''''))), s(s(s(Y'''')))) -> EQ(s(s(X'''')), s(s(Y'''')))
EQ(s(s(s(s(X'''''')))), s(s(s(s(Y''''''))))) -> EQ(s(s(s(X''''''))), s(s(s(Y''''''))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳FwdInst
...
→DP Problem 6
↳Forward Instantiation Transformation
→DP Problem 2
↳Remaining
→DP Problem 3
↳Remaining
EQ(s(s(s(s(X'''''')))), s(s(s(s(Y''''''))))) -> EQ(s(s(s(X''''''))), s(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)))
one new Dependency Pair is created:
EQ(s(s(s(s(X'''''')))), s(s(s(s(Y''''''))))) -> EQ(s(s(s(X''''''))), s(s(s(Y''''''))))
EQ(s(s(s(s(s(X''''''''))))), s(s(s(s(s(Y'''''''')))))) -> EQ(s(s(s(s(X'''''''')))), s(s(s(s(Y'''''''')))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳FwdInst
...
→DP Problem 7
↳Forward Instantiation Transformation
→DP Problem 2
↳Remaining
→DP Problem 3
↳Remaining
EQ(s(s(s(s(s(X''''''''))))), s(s(s(s(s(Y'''''''')))))) -> EQ(s(s(s(s(X'''''''')))), s(s(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)))
one new Dependency Pair is created:
EQ(s(s(s(s(s(X''''''''))))), s(s(s(s(s(Y'''''''')))))) -> EQ(s(s(s(s(X'''''''')))), s(s(s(s(Y'''''''')))))
EQ(s(s(s(s(s(s(X'''''''''')))))), s(s(s(s(s(s(Y''''''''''))))))) -> EQ(s(s(s(s(s(X''''''''''))))), s(s(s(s(s(Y''''''''''))))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
EQ(s(s(s(s(s(s(X'''''''''')))))), s(s(s(s(s(s(Y''''''''''))))))) -> EQ(s(s(s(s(s(X''''''''''))))), s(s(s(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)))
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)))
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)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
EQ(s(s(s(s(s(s(X'''''''''')))))), s(s(s(s(s(s(Y''''''''''))))))) -> EQ(s(s(s(s(s(X''''''''''))))), s(s(s(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)))
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)))
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)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
EQ(s(s(s(s(s(s(X'''''''''')))))), s(s(s(s(s(s(Y''''''''''))))))) -> EQ(s(s(s(s(s(X''''''''''))))), s(s(s(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)))
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)))
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)))