YES
0 QTRS
↳1 QTRSRRRProof (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 17 ms)
↳4 QTRS
↳5 AAECC Innermost (⇔, 0 ms)
↳6 QTRS
↳7 DependencyPairsProof (⇔, 0 ms)
↳8 QDP
↳9 DependencyGraphProof (⇔, 0 ms)
↳10 AND
↳11 QDP
↳12 UsableRulesProof (⇔, 0 ms)
↳13 QDP
↳14 QReductionProof (⇔, 0 ms)
↳15 QDP
↳16 QDPSizeChangeProof (⇔, 0 ms)
↳17 YES
↳18 QDP
↳19 UsableRulesProof (⇔, 0 ms)
↳20 QDP
↳21 QReductionProof (⇔, 0 ms)
↳22 QDP
↳23 QDPSizeChangeProof (⇔, 0 ms)
↳24 YES
↳25 QDP
↳26 UsableRulesProof (⇔, 0 ms)
↳27 QDP
↳28 QReductionProof (⇔, 0 ms)
↳29 QDP
↳30 QDPOrderProof (⇔, 38 ms)
↳31 QDP
↳32 PisEmptyProof (⇔, 0 ms)
↳33 YES
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(d) = 0
POL(double(x1)) = x1
POL(f(x1, x2)) = x1 + x2
POL(g(x1, x2)) = x1 + x2
POL(h) = 0
POL(half(x1)) = x1
POL(id(x1)) = 2 + 2·x1
POL(s(x1)) = x1
id(x) → f(x, s(0))
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(d) = 0
POL(double(x1)) = x1
POL(f(x1, x2)) = 2 + 2·x1 + x2
POL(g(x1, x2)) = 2·x1 + x2
POL(h) = 0
POL(half(x1)) = x1
POL(s(x1)) = x1
f(s(0), y) → y
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
f(s(x), y) → f(half(s(x)), double(y))
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
f(s(x0), x1)
G(d, s(x)) → G(d, x)
G(h, s(s(x))) → G(h, x)
DOUBLE(x) → G(d, x)
HALF(x) → G(h, x)
F(s(x), y) → F(half(s(x)), double(y))
F(s(x), y) → HALF(s(x))
F(s(x), y) → DOUBLE(y)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
f(s(x0), x1)
G(h, s(s(x))) → G(h, x)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
f(s(x0), x1)
G(h, s(s(x))) → G(h, x)
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
f(s(x0), x1)
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
f(s(x0), x1)
G(h, s(s(x))) → G(h, x)
From the DPs we obtained the following set of size-change graphs:
G(d, s(x)) → G(d, x)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
f(s(x0), x1)
G(d, s(x)) → G(d, x)
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
f(s(x0), x1)
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
f(s(x0), x1)
G(d, s(x)) → G(d, x)
From the DPs we obtained the following set of size-change graphs:
F(s(x), y) → F(half(s(x)), double(y))
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
f(s(x0), x1)
F(s(x), y) → F(half(s(x)), double(y))
half(x) → g(h, x)
double(x) → g(d, x)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
f(s(x0), x1)
f(s(x0), x1)
F(s(x), y) → F(half(s(x)), double(y))
half(x) → g(h, x)
double(x) → g(d, x)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(s(x), y) → F(half(s(x)), double(y))
The value of delta used in the strict ordering is 1/2.
POL(0) = 0
POL(F(x1, x2)) = x1
POL(d) = 0
POL(double(x1)) = [2] + [4]x1
POL(g(x1, x2)) = [1/2]x2
POL(h) = [1]
POL(half(x1)) = [1/2]x1
POL(s(x1)) = [1] + [2]x1
half(x) → g(h, x)
g(x, 0) → 0
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
half(x) → g(h, x)
double(x) → g(d, x)
g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
g(x0, 0)
g(d, s(x0))
g(h, s(0))
g(h, s(s(x0)))
double(x0)
half(x0)