0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔)
↳7 QDP
↳8 QDPSizeChangeProof (⇔)
↳9 TRUE
↳10 QDP
↳11 UsableRulesReductionPairsProof (⇔)
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 DependencyGraphProof (⇔)
↳16 QDP
↳17 QDPOrderProof (⇔)
↳18 QDP
↳19 PisEmptyProof (⇔)
↳20 TRUE
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)
POL(0) = 0
POL(F(x1)) = 1 + 2·x1
POL(G(x1)) = 1 + 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.
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 1.
POL(F(x1)) = (2)x1
POL(c(x1, x2)) = (1/2)x1 + (1/2)x2
POL(s(x1)) = 1 + (4)x1
POL(G(x1)) = 1 + (2)x1
POL(id_inc(x1)) = 1 + (4)x1
POL(0) = 0
id_inc(0) → s(0)
id_inc(0) → 0
id_inc(s(x)) → s(id_inc(x))
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
F(c(s(x), y)) → G(c(x, y))
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)
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)))
POL(0) = 0
POL(F(x1)) = x1
POL(c(x1, x2)) = 0
POL(id_inc(x1)) = x1
POL(s(x1)) = 1
id_inc(s(x)) → s(id_inc(x))
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)