YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 QDPOrderProof (⇔, 15 ms)
↳27 QDP
↳28 PisEmptyProof (⇔, 0 ms)
↳29 YES
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(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(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
purge(nil)
purge(add(x0, x1))
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)
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(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
purge(nil)
purge(add(x0, x1))
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)))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
purge(nil)
purge(add(x0, x1))
EQ(s(X), s(Y)) → EQ(X, Y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
purge(nil)
purge(add(x0, x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
purge(nil)
purge(add(x0, x1))
EQ(s(X), s(Y)) → EQ(X, Y)
From the DPs we obtained the following set of size-change graphs:
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)) → 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)))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
purge(nil)
purge(add(x0, x1))
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)) → 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)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
purge(nil)
purge(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
purge(nil)
purge(add(x0, x1))
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)) → 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)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
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)))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
purge(nil)
purge(add(x0, x1))
PURGE(add(N, X)) → PURGE(rm(N, X))
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)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
purge(nil)
purge(add(x0, x1))
purge(nil)
purge(add(x0, x1))
PURGE(add(N, X)) → PURGE(rm(N, X))
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)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PURGE(add(N, X)) → PURGE(rm(N, X))
trivial
add_1=1
nil=1
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))
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)
eq(0, 0) → true
eq(0, s(X)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
ifrm(false, N, add(M, X)) → add(M, rm(N, X))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
rm(x0, nil)
rm(x0, add(x1, x2))
ifrm(true, x0, add(x1, x2))
ifrm(false, x0, add(x1, x2))