YES
0 QTRS
↳1 QTRSRRRProof (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 0 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 4 ms)
↳6 QTRS
↳7 QTRSRRRProof (⇔, 0 ms)
↳8 QTRS
↳9 RisEmptyProof (⇔, 0 ms)
↳10 YES
double(0) → 0
double(s(x)) → s(s(double(x)))
+(x, 0) → x
+(x, s(y)) → s(+(x, y))
+(s(x), y) → s(+(x, y))
double(x) → +(x, x)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(+(x1, x2)) = 2 + x1 + x2
POL(0) = 1
POL(double(x1)) = 2 + 2·x1
POL(s(x1)) = 2 + x1
double(0) → 0
+(x, 0) → x
double(s(x)) → s(s(double(x)))
+(x, s(y)) → s(+(x, y))
+(s(x), y) → s(+(x, y))
double(x) → +(x, x)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(+(x1, x2)) = 1 + x1 + x2
POL(double(x1)) = 2 + 2·x1
POL(s(x1)) = 1 + x1
double(x) → +(x, x)
double(s(x)) → s(s(double(x)))
+(x, s(y)) → s(+(x, y))
+(s(x), y) → s(+(x, y))
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(+(x1, x2)) = 2 + 2·x1 + 2·x2
POL(double(x1)) = 2 + 2·x1
POL(s(x1)) = 1 + x1
+(x, s(y)) → s(+(x, y))
+(s(x), y) → s(+(x, y))
double(s(x)) → s(s(double(x)))
double1 > s1
double1: multiset
s1: multiset
double(s(x)) → s(s(double(x)))