YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 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 UsableRulesReductionPairsProof (⇔, 0 ms)
↳12 QDP
↳13 QDPOrderProof (⇔, 16 ms)
↳14 QDP
↳15 QDPOrderProof (⇔, 0 ms)
↳16 QDP
↳17 PisEmptyProof (⇔, 0 ms)
↳18 YES
f(s(x)) → f(id_inc(c(x, x)))
f(c(s(x), y)) → g(c(x, y))
g(c(s(x), y)) → g(c(y, x))
g(c(x, s(y))) → g(c(y, x))
g(c(x, x)) → f(x)
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
id_inc(s(x)) → s(id_inc(x))
id_inc(0) → 0
id_inc(0) → s(0)
F(s(x)) → F(id_inc(c(x, x)))
F(s(x)) → ID_INC(c(x, x))
F(c(s(x), y)) → G(c(x, y))
G(c(s(x), y)) → G(c(y, x))
G(c(x, s(y))) → G(c(y, x))
G(c(x, x)) → F(x)
ID_INC(c(x, y)) → ID_INC(x)
ID_INC(c(x, y)) → ID_INC(y)
ID_INC(s(x)) → ID_INC(x)
f(s(x)) → f(id_inc(c(x, x)))
f(c(s(x), y)) → g(c(x, y))
g(c(s(x), y)) → g(c(y, x))
g(c(x, s(y))) → g(c(y, x))
g(c(x, x)) → f(x)
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
id_inc(s(x)) → s(id_inc(x))
id_inc(0) → 0
id_inc(0) → s(0)
ID_INC(c(x, y)) → ID_INC(y)
ID_INC(c(x, y)) → ID_INC(x)
ID_INC(s(x)) → ID_INC(x)
f(s(x)) → f(id_inc(c(x, x)))
f(c(s(x), y)) → g(c(x, y))
g(c(s(x), y)) → g(c(y, x))
g(c(x, s(y))) → g(c(y, x))
g(c(x, x)) → f(x)
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
id_inc(s(x)) → s(id_inc(x))
id_inc(0) → 0
id_inc(0) → s(0)
ID_INC(c(x, y)) → ID_INC(y)
ID_INC(c(x, y)) → ID_INC(x)
ID_INC(s(x)) → ID_INC(x)
From the DPs we obtained the following set of size-change graphs:
F(c(s(x), y)) → G(c(x, y))
G(c(s(x), y)) → G(c(y, x))
G(c(x, s(y))) → G(c(y, x))
G(c(x, x)) → F(x)
F(s(x)) → F(id_inc(c(x, x)))
f(s(x)) → f(id_inc(c(x, x)))
f(c(s(x), y)) → g(c(x, y))
g(c(s(x), y)) → g(c(y, x))
g(c(x, s(y))) → g(c(y, x))
g(c(x, x)) → f(x)
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
id_inc(s(x)) → s(id_inc(x))
id_inc(0) → 0
id_inc(0) → s(0)
Used ordering: POLO with Polynomial interpretation [POLO]:
f(s(x)) → f(id_inc(c(x, x)))
f(c(s(x), y)) → g(c(x, y))
g(c(s(x), y)) → g(c(y, x))
g(c(x, s(y))) → g(c(y, x))
g(c(x, x)) → f(x)
POL(0) = 0
POL(F(x1)) = 2 + x1
POL(G(x1)) = 2 + x1
POL(c(x1, x2)) = x1 + x2
POL(id_inc(x1)) = x1
POL(s(x1)) = 2·x1
F(c(s(x), y)) → G(c(x, y))
G(c(s(x), y)) → G(c(y, x))
G(c(x, s(y))) → G(c(y, x))
G(c(x, x)) → F(x)
F(s(x)) → F(id_inc(c(x, x)))
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
id_inc(s(x)) → s(id_inc(x))
id_inc(0) → 0
id_inc(0) → s(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(c(s(x), y)) → G(c(x, y))
G(c(s(x), y)) → G(c(y, x))
G(c(x, s(y))) → G(c(y, x))
G(c(x, x)) → F(x)
The value of delta used in the strict ordering is 4.
POL(0) = [4]
POL(F(x1)) = [4]x1
POL(G(x1)) = [4] + [4]x1
POL(c(x1, x2)) = [1/2]x1 + [1/2]x2
POL(id_inc(x1)) = [4] + [4]x1
POL(s(x1)) = [4] + [4]x1
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
id_inc(s(x)) → s(id_inc(x))
id_inc(0) → 0
id_inc(0) → s(0)
F(s(x)) → F(id_inc(c(x, x)))
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
id_inc(s(x)) → s(id_inc(x))
id_inc(0) → 0
id_inc(0) → s(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(s(x)) → F(id_inc(c(x, x)))
s > idinc > c
s=1
id_inc=1
c=1
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
id_inc(s(x)) → s(id_inc(x))
id_inc(0) → 0
id_inc(0) → s(0)