YES
0 QTRS
↳1 DependencyPairsProof (⇔, 8 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔, 0 ms)
↳7 QDP
↳8 QDPSizeChangeProof (⇔, 0 ms)
↳9 YES
↳10 QDP
↳11 UsableRulesProof (⇔, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
↳15 QDP
↳16 QDPOrderProof (⇔, 30 ms)
↳17 QDP
↳18 PisEmptyProof (⇔, 0 ms)
↳19 YES
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(s(x), y) → plus(x, s(y))
plus(s(x), y) → s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) → s(plus(plus(x, y), z))
MINUS(s(x), s(y)) → MINUS(x, y)
DOUBLE(s(x)) → DOUBLE(x)
PLUS(s(x), y) → PLUS(x, y)
PLUS(s(x), y) → PLUS(x, s(y))
PLUS(s(x), y) → PLUS(minus(x, y), double(y))
PLUS(s(x), y) → MINUS(x, y)
PLUS(s(x), y) → DOUBLE(y)
PLUS(s(plus(x, y)), z) → PLUS(plus(x, y), z)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(s(x), y) → plus(x, s(y))
plus(s(x), y) → s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) → s(plus(plus(x, y), z))
DOUBLE(s(x)) → DOUBLE(x)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(s(x), y) → plus(x, s(y))
plus(s(x), y) → s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) → s(plus(plus(x, y), z))
DOUBLE(s(x)) → DOUBLE(x)
From the DPs we obtained the following set of size-change graphs:
MINUS(s(x), s(y)) → MINUS(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(s(x), y) → plus(x, s(y))
plus(s(x), y) → s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) → s(plus(plus(x, y), z))
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
PLUS(s(x), y) → PLUS(x, s(y))
PLUS(s(x), y) → PLUS(x, y)
PLUS(s(x), y) → PLUS(minus(x, y), double(y))
PLUS(s(plus(x, y)), z) → PLUS(plus(x, y), z)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(s(x), y) → plus(x, s(y))
plus(s(x), y) → s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) → s(plus(plus(x, y), z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(s(x), y) → PLUS(x, s(y))
PLUS(s(x), y) → PLUS(x, y)
PLUS(s(x), y) → PLUS(minus(x, y), double(y))
PLUS(s(plus(x, y)), z) → PLUS(plus(x, y), z)
[PLUS2, plus2] > double1 > s1
[PLUS2, plus2] > double1 > 0
PLUS2: [1,2]
s1: multiset
double1: multiset
plus2: [1,2]
0: multiset
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(s(x), y) → plus(x, s(y))
plus(s(x), y) → s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) → s(plus(plus(x, y), z))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(s(x), y) → plus(x, s(y))
plus(s(x), y) → s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) → s(plus(plus(x, y), z))