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