(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
d2(0) → 2
d3(0) → 3
d4(0) → 4
d5(0) → 5
d6(0) → 6
d7(0) → 7
d8(0) → 8
d9(0) → 9
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
times(x, 0) → 0
times(x, 1) → plus(times(x, 0), x)
times(x, 2) → plus(times(x, 1), x)
times(x, 3) → plus(times(x, 2), x)
times(x, 4) → plus(times(x, 3), x)
times(x, 5) → plus(times(x, 4), x)
times(x, 6) → plus(times(x, 5), x)
times(x, 7) → plus(times(x, 6), x)
times(x, 8) → plus(times(x, 7), x)
times(x, 9) → plus(times(x, 8), x)
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, d2(y)) → plus(d0(times(x, y)), times(x, 2))
times(x, d3(y)) → plus(d0(times(x, y)), times(x, 3))
times(x, d4(y)) → plus(d0(times(x, y)), times(x, 4))
times(x, d5(y)) → plus(d0(times(x, y)), times(x, 5))
times(x, d6(y)) → plus(d0(times(x, y)), times(x, 6))
times(x, d7(y)) → plus(d0(times(x, y)), times(x, 7))
times(x, d8(y)) → plus(d0(times(x, y)), times(x, 8))
times(x, d9(y)) → plus(d0(times(x, y)), times(x, 9))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
p(m(x)) → m(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d9(p(x)))
d2(m(x)) → m(d8(p(x)))
d3(m(x)) → m(d7(p(x)))
d4(m(x)) → m(d6(p(x)))
d5(m(x)) → m(d5(p(x)))
d6(m(x)) → m(d4(p(x)))
d7(m(x)) → m(d3(p(x)))
d8(m(x)) → m(d2(p(x)))
d9(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(9) → D0(1)
S(d0(x)) → D1(x)
S(d1(x)) → D2(x)
S(d2(x)) → D3(x)
S(d3(x)) → D4(x)
S(d4(x)) → D5(x)
S(d5(x)) → D6(x)
S(d6(x)) → D7(x)
S(d7(x)) → D8(x)
S(d8(x)) → D9(x)
S(d9(x)) → D0(s(x))
S(d9(x)) → S(x)
PLUS(x, 1) → S(x)
PLUS(x, 2) → S(s(x))
PLUS(x, 2) → S(x)
PLUS(x, 3) → S(s(s(x)))
PLUS(x, 3) → S(s(x))
PLUS(x, 3) → S(x)
PLUS(x, 4) → S(s(s(s(x))))
PLUS(x, 4) → S(s(s(x)))
PLUS(x, 4) → S(s(x))
PLUS(x, 4) → S(x)
PLUS(x, 5) → S(s(s(s(s(x)))))
PLUS(x, 5) → S(s(s(s(x))))
PLUS(x, 5) → S(s(s(x)))
PLUS(x, 5) → S(s(x))
PLUS(x, 5) → S(x)
PLUS(x, 6) → S(s(s(s(s(s(x))))))
PLUS(x, 6) → S(s(s(s(s(x)))))
PLUS(x, 6) → S(s(s(s(x))))
PLUS(x, 6) → S(s(s(x)))
PLUS(x, 6) → S(s(x))
PLUS(x, 6) → S(x)
PLUS(x, 7) → S(s(s(s(s(s(s(x)))))))
PLUS(x, 7) → S(s(s(s(s(s(x))))))
PLUS(x, 7) → S(s(s(s(s(x)))))
PLUS(x, 7) → S(s(s(s(x))))
PLUS(x, 7) → S(s(s(x)))
PLUS(x, 7) → S(s(x))
PLUS(x, 7) → S(x)
PLUS(x, 8) → S(s(s(s(s(s(s(s(x))))))))
PLUS(x, 8) → S(s(s(s(s(s(s(x)))))))
PLUS(x, 8) → S(s(s(s(s(s(x))))))
PLUS(x, 8) → S(s(s(s(s(x)))))
PLUS(x, 8) → S(s(s(s(x))))
PLUS(x, 8) → S(s(s(x)))
PLUS(x, 8) → S(s(x))
PLUS(x, 8) → S(x)
PLUS(x, 9) → S(s(s(s(s(s(s(s(s(x)))))))))
PLUS(x, 9) → S(s(s(s(s(s(s(s(x))))))))
PLUS(x, 9) → S(s(s(s(s(s(s(x)))))))
PLUS(x, 9) → S(s(s(s(s(s(x))))))
PLUS(x, 9) → S(s(s(s(s(x)))))
PLUS(x, 9) → S(s(s(s(x))))
PLUS(x, 9) → S(s(s(x)))
PLUS(x, 9) → S(s(x))
PLUS(x, 9) → S(x)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → S(plus(x, d0(y)))
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d1(y)) → D0(y)
PLUS(x, d2(y)) → S(s(plus(x, d0(y))))
PLUS(x, d2(y)) → S(plus(x, d0(y)))
PLUS(x, d2(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → D0(y)
PLUS(x, d3(y)) → S(s(s(plus(x, d0(y)))))
PLUS(x, d3(y)) → S(s(plus(x, d0(y))))
PLUS(x, d3(y)) → S(plus(x, d0(y)))
PLUS(x, d3(y)) → PLUS(x, d0(y))
PLUS(x, d3(y)) → D0(y)
PLUS(x, d4(y)) → S(s(s(s(plus(x, d0(y))))))
PLUS(x, d4(y)) → S(s(s(plus(x, d0(y)))))
PLUS(x, d4(y)) → S(s(plus(x, d0(y))))
PLUS(x, d4(y)) → S(plus(x, d0(y)))
PLUS(x, d4(y)) → PLUS(x, d0(y))
PLUS(x, d4(y)) → D0(y)
PLUS(x, d5(y)) → S(s(s(s(s(plus(x, d0(y)))))))
PLUS(x, d5(y)) → S(s(s(s(plus(x, d0(y))))))
PLUS(x, d5(y)) → S(s(s(plus(x, d0(y)))))
PLUS(x, d5(y)) → S(s(plus(x, d0(y))))
PLUS(x, d5(y)) → S(plus(x, d0(y)))
PLUS(x, d5(y)) → PLUS(x, d0(y))
PLUS(x, d5(y)) → D0(y)
PLUS(x, d6(y)) → S(s(s(s(s(s(plus(x, d0(y))))))))
PLUS(x, d6(y)) → S(s(s(s(s(plus(x, d0(y)))))))
PLUS(x, d6(y)) → S(s(s(s(plus(x, d0(y))))))
PLUS(x, d6(y)) → S(s(s(plus(x, d0(y)))))
PLUS(x, d6(y)) → S(s(plus(x, d0(y))))
PLUS(x, d6(y)) → S(plus(x, d0(y)))
PLUS(x, d6(y)) → PLUS(x, d0(y))
PLUS(x, d6(y)) → D0(y)
PLUS(x, d7(y)) → S(s(s(s(s(s(s(plus(x, d0(y)))))))))
PLUS(x, d7(y)) → S(s(s(s(s(s(plus(x, d0(y))))))))
PLUS(x, d7(y)) → S(s(s(s(s(plus(x, d0(y)))))))
PLUS(x, d7(y)) → S(s(s(s(plus(x, d0(y))))))
PLUS(x, d7(y)) → S(s(s(plus(x, d0(y)))))
PLUS(x, d7(y)) → S(s(plus(x, d0(y))))
PLUS(x, d7(y)) → S(plus(x, d0(y)))
PLUS(x, d7(y)) → PLUS(x, d0(y))
PLUS(x, d7(y)) → D0(y)
PLUS(x, d8(y)) → S(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
PLUS(x, d8(y)) → S(s(s(s(s(s(s(plus(x, d0(y)))))))))
PLUS(x, d8(y)) → S(s(s(s(s(s(plus(x, d0(y))))))))
PLUS(x, d8(y)) → S(s(s(s(s(plus(x, d0(y)))))))
PLUS(x, d8(y)) → S(s(s(s(plus(x, d0(y))))))
PLUS(x, d8(y)) → S(s(s(plus(x, d0(y)))))
PLUS(x, d8(y)) → S(s(plus(x, d0(y))))
PLUS(x, d8(y)) → S(plus(x, d0(y)))
PLUS(x, d8(y)) → PLUS(x, d0(y))
PLUS(x, d8(y)) → D0(y)
PLUS(x, d9(y)) → S(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
PLUS(x, d9(y)) → S(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
PLUS(x, d9(y)) → S(s(s(s(s(s(s(plus(x, d0(y)))))))))
PLUS(x, d9(y)) → S(s(s(s(s(s(plus(x, d0(y))))))))
PLUS(x, d9(y)) → S(s(s(s(s(plus(x, d0(y)))))))
PLUS(x, d9(y)) → S(s(s(s(plus(x, d0(y))))))
PLUS(x, d9(y)) → S(s(s(plus(x, d0(y)))))
PLUS(x, d9(y)) → S(s(plus(x, d0(y))))
PLUS(x, d9(y)) → S(plus(x, d0(y)))
PLUS(x, d9(y)) → PLUS(x, d0(y))
PLUS(x, d9(y)) → D0(y)
TIMES(x, 1) → PLUS(times(x, 0), x)
TIMES(x, 1) → TIMES(x, 0)
TIMES(x, 2) → PLUS(times(x, 1), x)
TIMES(x, 2) → TIMES(x, 1)
TIMES(x, 3) → PLUS(times(x, 2), x)
TIMES(x, 3) → TIMES(x, 2)
TIMES(x, 4) → PLUS(times(x, 3), x)
TIMES(x, 4) → TIMES(x, 3)
TIMES(x, 5) → PLUS(times(x, 4), x)
TIMES(x, 5) → TIMES(x, 4)
TIMES(x, 6) → PLUS(times(x, 5), x)
TIMES(x, 6) → TIMES(x, 5)
TIMES(x, 7) → PLUS(times(x, 6), x)
TIMES(x, 7) → TIMES(x, 6)
TIMES(x, 8) → PLUS(times(x, 7), x)
TIMES(x, 8) → TIMES(x, 7)
TIMES(x, 9) → PLUS(times(x, 8), x)
TIMES(x, 9) → TIMES(x, 8)
TIMES(x, d0(y)) → PLUS(d0(times(x, y)), times(x, 0))
TIMES(x, d0(y)) → D0(times(x, y))
TIMES(x, d0(y)) → TIMES(x, y)
TIMES(x, d0(y)) → TIMES(x, 0)
TIMES(x, d1(y)) → PLUS(d0(times(x, y)), times(x, 1))
TIMES(x, d1(y)) → D0(times(x, y))
TIMES(x, d1(y)) → TIMES(x, y)
TIMES(x, d1(y)) → TIMES(x, 1)
TIMES(x, d2(y)) → PLUS(d0(times(x, y)), times(x, 2))
TIMES(x, d2(y)) → D0(times(x, y))
TIMES(x, d2(y)) → TIMES(x, y)
TIMES(x, d2(y)) → TIMES(x, 2)
TIMES(x, d3(y)) → PLUS(d0(times(x, y)), times(x, 3))
TIMES(x, d3(y)) → D0(times(x, y))
TIMES(x, d3(y)) → TIMES(x, y)
TIMES(x, d3(y)) → TIMES(x, 3)
TIMES(x, d4(y)) → PLUS(d0(times(x, y)), times(x, 4))
TIMES(x, d4(y)) → D0(times(x, y))
TIMES(x, d4(y)) → TIMES(x, y)
TIMES(x, d4(y)) → TIMES(x, 4)
TIMES(x, d5(y)) → PLUS(d0(times(x, y)), times(x, 5))
TIMES(x, d5(y)) → D0(times(x, y))
TIMES(x, d5(y)) → TIMES(x, y)
TIMES(x, d5(y)) → TIMES(x, 5)
TIMES(x, d6(y)) → PLUS(d0(times(x, y)), times(x, 6))
TIMES(x, d6(y)) → D0(times(x, y))
TIMES(x, d6(y)) → TIMES(x, y)
TIMES(x, d6(y)) → TIMES(x, 6)
TIMES(x, d7(y)) → PLUS(d0(times(x, y)), times(x, 7))
TIMES(x, d7(y)) → D0(times(x, y))
TIMES(x, d7(y)) → TIMES(x, y)
TIMES(x, d7(y)) → TIMES(x, 7)
TIMES(x, d8(y)) → PLUS(d0(times(x, y)), times(x, 8))
TIMES(x, d8(y)) → D0(times(x, y))
TIMES(x, d8(y)) → TIMES(x, y)
TIMES(x, d8(y)) → TIMES(x, 8)
TIMES(x, d9(y)) → PLUS(d0(times(x, y)), times(x, 9))
TIMES(x, d9(y)) → D0(times(x, y))
TIMES(x, d9(y)) → TIMES(x, y)
TIMES(x, d9(y)) → TIMES(x, 9)
P(0) → M(1)
P(d0(x)) → D9(p(x))
P(d0(x)) → P(x)
P(d1(x)) → D0(x)
P(d2(x)) → D1(x)
P(d3(x)) → D2(x)
P(d4(x)) → D3(x)
P(d5(x)) → D4(x)
P(d6(x)) → D5(x)
P(d7(x)) → D6(x)
P(d8(x)) → D7(x)
P(d9(x)) → D8(x)
P(m(x)) → M(s(x))
P(m(x)) → S(x)
S(m(1)) → M(0)
S(m(2)) → M(1)
S(m(3)) → M(2)
S(m(4)) → M(3)
S(m(5)) → M(4)
S(m(6)) → M(5)
S(m(7)) → M(6)
S(m(8)) → M(7)
S(m(9)) → M(8)
S(m(d0(x))) → M(d9(p(x)))
S(m(d0(x))) → D9(p(x))
S(m(d0(x))) → P(x)
S(m(d1(x))) → M(d0(x))
S(m(d1(x))) → D0(x)
S(m(d2(x))) → M(d1(x))
S(m(d2(x))) → D1(x)
S(m(d3(x))) → M(d2(x))
S(m(d3(x))) → D2(x)
S(m(d4(x))) → M(d3(x))
S(m(d4(x))) → D3(x)
S(m(d5(x))) → M(d4(x))
S(m(d5(x))) → D4(x)
S(m(d6(x))) → M(d5(x))
S(m(d6(x))) → D5(x)
S(m(d7(x))) → M(d6(x))
S(m(d7(x))) → D6(x)
S(m(d8(x))) → M(d7(x))
S(m(d8(x))) → D7(x)
S(m(d9(x))) → M(d8(x))
S(m(d9(x))) → D8(x)
D0(m(x)) → M(d0(x))
D0(m(x)) → D0(x)
D1(m(x)) → M(d9(p(x)))
D1(m(x)) → D9(p(x))
D1(m(x)) → P(x)
D2(m(x)) → M(d8(p(x)))
D2(m(x)) → D8(p(x))
D2(m(x)) → P(x)
D3(m(x)) → M(d7(p(x)))
D3(m(x)) → D7(p(x))
D3(m(x)) → P(x)
D4(m(x)) → M(d6(p(x)))
D4(m(x)) → D6(p(x))
D4(m(x)) → P(x)
D5(m(x)) → M(d5(p(x)))
D5(m(x)) → D5(p(x))
D5(m(x)) → P(x)
D6(m(x)) → M(d4(p(x)))
D6(m(x)) → D4(p(x))
D6(m(x)) → P(x)
D7(m(x)) → M(d3(p(x)))
D7(m(x)) → D3(p(x))
D7(m(x)) → P(x)
D8(m(x)) → M(d2(p(x)))
D8(m(x)) → D2(p(x))
D8(m(x)) → P(x)
D9(m(x)) → M(d1(p(x)))
D9(m(x)) → D1(p(x))
D9(m(x)) → P(x)
PLUS(x, m(y)) → M(plus(m(x), y))
PLUS(x, m(y)) → PLUS(m(x), y)
PLUS(x, m(y)) → M(x)
TIMES(x, m(y)) → M(times(x, y))
TIMES(x, m(y)) → TIMES(x, y)

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
d2(0) → 2
d3(0) → 3
d4(0) → 4
d5(0) → 5
d6(0) → 6
d7(0) → 7
d8(0) → 8
d9(0) → 9
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
times(x, 0) → 0
times(x, 1) → plus(times(x, 0), x)
times(x, 2) → plus(times(x, 1), x)
times(x, 3) → plus(times(x, 2), x)
times(x, 4) → plus(times(x, 3), x)
times(x, 5) → plus(times(x, 4), x)
times(x, 6) → plus(times(x, 5), x)
times(x, 7) → plus(times(x, 6), x)
times(x, 8) → plus(times(x, 7), x)
times(x, 9) → plus(times(x, 8), x)
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, d2(y)) → plus(d0(times(x, y)), times(x, 2))
times(x, d3(y)) → plus(d0(times(x, y)), times(x, 3))
times(x, d4(y)) → plus(d0(times(x, y)), times(x, 4))
times(x, d5(y)) → plus(d0(times(x, y)), times(x, 5))
times(x, d6(y)) → plus(d0(times(x, y)), times(x, 6))
times(x, d7(y)) → plus(d0(times(x, y)), times(x, 7))
times(x, d8(y)) → plus(d0(times(x, y)), times(x, 8))
times(x, d9(y)) → plus(d0(times(x, y)), times(x, 9))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
p(m(x)) → m(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d9(p(x)))
d2(m(x)) → m(d8(p(x)))
d3(m(x)) → m(d7(p(x)))
d4(m(x)) → m(d6(p(x)))
d5(m(x)) → m(d5(p(x)))
d6(m(x)) → m(d4(p(x)))
d7(m(x)) → m(d3(p(x)))
d8(m(x)) → m(d2(p(x)))
d9(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 8 SCCs with 223 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(d0(x)) → D9(p(x))
D9(m(x)) → D1(p(x))
D1(m(x)) → D9(p(x))
D9(m(x)) → P(x)
P(d0(x)) → P(x)
D1(m(x)) → P(x)

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
d2(0) → 2
d3(0) → 3
d4(0) → 4
d5(0) → 5
d6(0) → 6
d7(0) → 7
d8(0) → 8
d9(0) → 9
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
times(x, 0) → 0
times(x, 1) → plus(times(x, 0), x)
times(x, 2) → plus(times(x, 1), x)
times(x, 3) → plus(times(x, 2), x)
times(x, 4) → plus(times(x, 3), x)
times(x, 5) → plus(times(x, 4), x)
times(x, 6) → plus(times(x, 5), x)
times(x, 7) → plus(times(x, 6), x)
times(x, 8) → plus(times(x, 7), x)
times(x, 9) → plus(times(x, 8), x)
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, d2(y)) → plus(d0(times(x, y)), times(x, 2))
times(x, d3(y)) → plus(d0(times(x, y)), times(x, 3))
times(x, d4(y)) → plus(d0(times(x, y)), times(x, 4))
times(x, d5(y)) → plus(d0(times(x, y)), times(x, 5))
times(x, d6(y)) → plus(d0(times(x, y)), times(x, 6))
times(x, d7(y)) → plus(d0(times(x, y)), times(x, 7))
times(x, d8(y)) → plus(d0(times(x, y)), times(x, 8))
times(x, d9(y)) → plus(d0(times(x, y)), times(x, 9))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
p(m(x)) → m(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d9(p(x)))
d2(m(x)) → m(d8(p(x)))
d3(m(x)) → m(d7(p(x)))
d4(m(x)) → m(d6(p(x)))
d5(m(x)) → m(d5(p(x)))
d6(m(x)) → m(d4(p(x)))
d7(m(x)) → m(d3(p(x)))
d8(m(x)) → m(d2(p(x)))
d9(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(6) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(d0(x)) → D9(p(x))
D9(m(x)) → D1(p(x))
D1(m(x)) → D9(p(x))
D9(m(x)) → P(x)
P(d0(x)) → P(x)
D1(m(x)) → P(x)

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(8) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
plus(x0, m(x1))
times(x0, m(x1))

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(d0(x)) → D9(p(x))
D9(m(x)) → D1(p(x))
D1(m(x)) → D9(p(x))
D9(m(x)) → P(x)
P(d0(x)) → P(x)
D1(m(x)) → P(x)

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(10) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

D9(m(x)) → D1(p(x))
D1(m(x)) → D9(p(x))
D9(m(x)) → P(x)
P(d0(x)) → P(x)
D1(m(x)) → P(x)

Strictly oriented rules of the TRS R:

d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 2   
POL(1) = 2   
POL(2) = 2   
POL(3) = 2   
POL(4) = 2   
POL(5) = 2   
POL(6) = 2   
POL(7) = 2   
POL(8) = 2   
POL(9) = 2   
POL(D1(x1)) = 2 + 2·x1   
POL(D9(x1)) = 2 + 2·x1   
POL(P(x1)) = 1 + x1   
POL(d0(x1)) = 1 + 2·x1   
POL(d1(x1)) = 1 + 2·x1   
POL(d2(x1)) = 1 + 2·x1   
POL(d3(x1)) = 1 + 2·x1   
POL(d4(x1)) = 1 + 2·x1   
POL(d5(x1)) = 1 + 2·x1   
POL(d6(x1)) = 1 + 2·x1   
POL(d7(x1)) = 1 + 2·x1   
POL(d8(x1)) = 1 + 2·x1   
POL(d9(x1)) = 1 + 2·x1   
POL(m(x1)) = 2 + 2·x1   
POL(p(x1)) = x1   

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(d0(x)) → D9(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(12) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(13) TRUE

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D5(m(x)) → D5(p(x))

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
d2(0) → 2
d3(0) → 3
d4(0) → 4
d5(0) → 5
d6(0) → 6
d7(0) → 7
d8(0) → 8
d9(0) → 9
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
times(x, 0) → 0
times(x, 1) → plus(times(x, 0), x)
times(x, 2) → plus(times(x, 1), x)
times(x, 3) → plus(times(x, 2), x)
times(x, 4) → plus(times(x, 3), x)
times(x, 5) → plus(times(x, 4), x)
times(x, 6) → plus(times(x, 5), x)
times(x, 7) → plus(times(x, 6), x)
times(x, 8) → plus(times(x, 7), x)
times(x, 9) → plus(times(x, 8), x)
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, d2(y)) → plus(d0(times(x, y)), times(x, 2))
times(x, d3(y)) → plus(d0(times(x, y)), times(x, 3))
times(x, d4(y)) → plus(d0(times(x, y)), times(x, 4))
times(x, d5(y)) → plus(d0(times(x, y)), times(x, 5))
times(x, d6(y)) → plus(d0(times(x, y)), times(x, 6))
times(x, d7(y)) → plus(d0(times(x, y)), times(x, 7))
times(x, d8(y)) → plus(d0(times(x, y)), times(x, 8))
times(x, d9(y)) → plus(d0(times(x, y)), times(x, 9))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
p(m(x)) → m(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d9(p(x)))
d2(m(x)) → m(d8(p(x)))
d3(m(x)) → m(d7(p(x)))
d4(m(x)) → m(d6(p(x)))
d5(m(x)) → m(d5(p(x)))
d6(m(x)) → m(d4(p(x)))
d7(m(x)) → m(d3(p(x)))
d8(m(x)) → m(d2(p(x)))
d9(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(15) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D5(m(x)) → D5(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(17) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
plus(x0, m(x1))
times(x0, m(x1))

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D5(m(x)) → D5(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(19) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

D5(m(x)) → D5(p(x))

Strictly oriented rules of the TRS R:

p(3) → 2
p(4) → 3
p(5) → 4
p(7) → 6
p(9) → 8
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d1(0) → 1
m(0) → 0
m(m(x)) → x

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 2   
POL(1) = 1   
POL(2) = 0   
POL(3) = 0   
POL(4) = 0   
POL(5) = 2   
POL(6) = 1   
POL(7) = 2   
POL(8) = 1   
POL(9) = 1   
POL(D5(x1)) = x1   
POL(d0(x1)) = 1 + 2·x1   
POL(d1(x1)) = 2·x1   
POL(d2(x1)) = 2·x1   
POL(d3(x1)) = 2·x1   
POL(d4(x1)) = 2·x1   
POL(d5(x1)) = 2·x1   
POL(d6(x1)) = 2·x1   
POL(d7(x1)) = 2·x1   
POL(d8(x1)) = 2·x1   
POL(d9(x1)) = 2·x1   
POL(m(x1)) = 2 + x1   
POL(p(x1)) = 1 + x1   

(20) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(6) → 5
p(8) → 7
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
d9(m(x)) → m(d1(p(x)))
d1(m(x)) → m(d9(p(x)))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(21) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(22) YES

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D4(m(x)) → D6(p(x))
D6(m(x)) → D4(p(x))

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
d2(0) → 2
d3(0) → 3
d4(0) → 4
d5(0) → 5
d6(0) → 6
d7(0) → 7
d8(0) → 8
d9(0) → 9
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
times(x, 0) → 0
times(x, 1) → plus(times(x, 0), x)
times(x, 2) → plus(times(x, 1), x)
times(x, 3) → plus(times(x, 2), x)
times(x, 4) → plus(times(x, 3), x)
times(x, 5) → plus(times(x, 4), x)
times(x, 6) → plus(times(x, 5), x)
times(x, 7) → plus(times(x, 6), x)
times(x, 8) → plus(times(x, 7), x)
times(x, 9) → plus(times(x, 8), x)
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, d2(y)) → plus(d0(times(x, y)), times(x, 2))
times(x, d3(y)) → plus(d0(times(x, y)), times(x, 3))
times(x, d4(y)) → plus(d0(times(x, y)), times(x, 4))
times(x, d5(y)) → plus(d0(times(x, y)), times(x, 5))
times(x, d6(y)) → plus(d0(times(x, y)), times(x, 6))
times(x, d7(y)) → plus(d0(times(x, y)), times(x, 7))
times(x, d8(y)) → plus(d0(times(x, y)), times(x, 8))
times(x, d9(y)) → plus(d0(times(x, y)), times(x, 9))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
p(m(x)) → m(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d9(p(x)))
d2(m(x)) → m(d8(p(x)))
d3(m(x)) → m(d7(p(x)))
d4(m(x)) → m(d6(p(x)))
d5(m(x)) → m(d5(p(x)))
d6(m(x)) → m(d4(p(x)))
d7(m(x)) → m(d3(p(x)))
d8(m(x)) → m(d2(p(x)))
d9(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(24) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D4(m(x)) → D6(p(x))
D6(m(x)) → D4(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(26) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
plus(x0, m(x1))
times(x0, m(x1))

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D4(m(x)) → D6(p(x))
D6(m(x)) → D4(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(28) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

D4(m(x)) → D6(p(x))
D6(m(x)) → D4(p(x))

Strictly oriented rules of the TRS R:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

Used ordering: Knuth-Bendix order [KBO] with precedence:
p1 > d91 > 3 > d11 > d71 > 6 > m1 > 5 > 1 > 4 > D61 > 2 > 8 > d21 > d41 > D41 > 0 > d01 > 7 > 9 > d61 > d31 > d81 > d51

and weight map:

1=9
0=8
2=10
3=11
4=12
5=13
6=14
7=15
8=16
9=17
p_1=0
d0_1=10
d9_1=10
d1_1=10
d2_1=10
d3_1=10
d4_1=10
d5_1=10
d6_1=10
d7_1=10
d8_1=10
m_1=1
D4_1=2
D6_1=1

The variable weight is 1

(29) Obligation:

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(30) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(31) YES

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D3(m(x)) → D7(p(x))
D7(m(x)) → D3(p(x))

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
d2(0) → 2
d3(0) → 3
d4(0) → 4
d5(0) → 5
d6(0) → 6
d7(0) → 7
d8(0) → 8
d9(0) → 9
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
times(x, 0) → 0
times(x, 1) → plus(times(x, 0), x)
times(x, 2) → plus(times(x, 1), x)
times(x, 3) → plus(times(x, 2), x)
times(x, 4) → plus(times(x, 3), x)
times(x, 5) → plus(times(x, 4), x)
times(x, 6) → plus(times(x, 5), x)
times(x, 7) → plus(times(x, 6), x)
times(x, 8) → plus(times(x, 7), x)
times(x, 9) → plus(times(x, 8), x)
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, d2(y)) → plus(d0(times(x, y)), times(x, 2))
times(x, d3(y)) → plus(d0(times(x, y)), times(x, 3))
times(x, d4(y)) → plus(d0(times(x, y)), times(x, 4))
times(x, d5(y)) → plus(d0(times(x, y)), times(x, 5))
times(x, d6(y)) → plus(d0(times(x, y)), times(x, 6))
times(x, d7(y)) → plus(d0(times(x, y)), times(x, 7))
times(x, d8(y)) → plus(d0(times(x, y)), times(x, 8))
times(x, d9(y)) → plus(d0(times(x, y)), times(x, 9))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
p(m(x)) → m(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d9(p(x)))
d2(m(x)) → m(d8(p(x)))
d3(m(x)) → m(d7(p(x)))
d4(m(x)) → m(d6(p(x)))
d5(m(x)) → m(d5(p(x)))
d6(m(x)) → m(d4(p(x)))
d7(m(x)) → m(d3(p(x)))
d8(m(x)) → m(d2(p(x)))
d9(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(33) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D3(m(x)) → D7(p(x))
D7(m(x)) → D3(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(35) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
plus(x0, m(x1))
times(x0, m(x1))

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D3(m(x)) → D7(p(x))
D7(m(x)) → D3(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(37) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

D7(m(x)) → D3(p(x))

Strictly oriented rules of the TRS R:

d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 2   
POL(1) = 2   
POL(2) = 2   
POL(3) = 2   
POL(4) = 2   
POL(5) = 2   
POL(6) = 2   
POL(7) = 2   
POL(8) = 2   
POL(9) = 2   
POL(D3(x1)) = 2·x1   
POL(D7(x1)) = 2 + x1   
POL(d0(x1)) = 2·x1   
POL(d1(x1)) = 2·x1   
POL(d2(x1)) = 2·x1   
POL(d3(x1)) = 2·x1   
POL(d4(x1)) = 2·x1   
POL(d5(x1)) = 2·x1   
POL(d6(x1)) = 2·x1   
POL(d7(x1)) = 2·x1   
POL(d8(x1)) = 2·x1   
POL(d9(x1)) = 2·x1   
POL(m(x1)) = 1 + 2·x1   
POL(p(x1)) = x1   

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D3(m(x)) → D7(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(39) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(40) TRUE

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D2(m(x)) → D8(p(x))
D8(m(x)) → D2(p(x))

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
d2(0) → 2
d3(0) → 3
d4(0) → 4
d5(0) → 5
d6(0) → 6
d7(0) → 7
d8(0) → 8
d9(0) → 9
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
times(x, 0) → 0
times(x, 1) → plus(times(x, 0), x)
times(x, 2) → plus(times(x, 1), x)
times(x, 3) → plus(times(x, 2), x)
times(x, 4) → plus(times(x, 3), x)
times(x, 5) → plus(times(x, 4), x)
times(x, 6) → plus(times(x, 5), x)
times(x, 7) → plus(times(x, 6), x)
times(x, 8) → plus(times(x, 7), x)
times(x, 9) → plus(times(x, 8), x)
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, d2(y)) → plus(d0(times(x, y)), times(x, 2))
times(x, d3(y)) → plus(d0(times(x, y)), times(x, 3))
times(x, d4(y)) → plus(d0(times(x, y)), times(x, 4))
times(x, d5(y)) → plus(d0(times(x, y)), times(x, 5))
times(x, d6(y)) → plus(d0(times(x, y)), times(x, 6))
times(x, d7(y)) → plus(d0(times(x, y)), times(x, 7))
times(x, d8(y)) → plus(d0(times(x, y)), times(x, 8))
times(x, d9(y)) → plus(d0(times(x, y)), times(x, 9))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
p(m(x)) → m(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d9(p(x)))
d2(m(x)) → m(d8(p(x)))
d3(m(x)) → m(d7(p(x)))
d4(m(x)) → m(d6(p(x)))
d5(m(x)) → m(d5(p(x)))
d6(m(x)) → m(d4(p(x)))
d7(m(x)) → m(d3(p(x)))
d8(m(x)) → m(d2(p(x)))
d9(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(42) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D2(m(x)) → D8(p(x))
D8(m(x)) → D2(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(44) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
plus(x0, m(x1))
times(x0, m(x1))

(45) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D2(m(x)) → D8(p(x))
D8(m(x)) → D2(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(46) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

D8(m(x)) → D2(p(x))

Strictly oriented rules of the TRS R:

d9(0) → 9
d9(m(x)) → m(d1(p(x)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 2   
POL(1) = 2   
POL(2) = 2   
POL(3) = 2   
POL(4) = 2   
POL(5) = 2   
POL(6) = 2   
POL(7) = 2   
POL(8) = 2   
POL(9) = 2   
POL(D2(x1)) = 2·x1   
POL(D8(x1)) = 2 + x1   
POL(d0(x1)) = 2·x1   
POL(d1(x1)) = 2·x1   
POL(d2(x1)) = 2·x1   
POL(d3(x1)) = 2·x1   
POL(d4(x1)) = 2·x1   
POL(d5(x1)) = 2·x1   
POL(d6(x1)) = 2·x1   
POL(d7(x1)) = 2·x1   
POL(d8(x1)) = 2·x1   
POL(d9(x1)) = 2·x1   
POL(m(x1)) = 1 + 2·x1   
POL(p(x1)) = x1   

(47) Obligation:

Q DP problem:
The TRS P consists of the following rules:

D2(m(x)) → D8(p(x))

The TRS R consists of the following rules:

p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(48) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(49) TRUE

(50) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(d9(x)) → S(x)

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
d2(0) → 2
d3(0) → 3
d4(0) → 4
d5(0) → 5
d6(0) → 6
d7(0) → 7
d8(0) → 8
d9(0) → 9
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
times(x, 0) → 0
times(x, 1) → plus(times(x, 0), x)
times(x, 2) → plus(times(x, 1), x)
times(x, 3) → plus(times(x, 2), x)
times(x, 4) → plus(times(x, 3), x)
times(x, 5) → plus(times(x, 4), x)
times(x, 6) → plus(times(x, 5), x)
times(x, 7) → plus(times(x, 6), x)
times(x, 8) → plus(times(x, 7), x)
times(x, 9) → plus(times(x, 8), x)
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, d2(y)) → plus(d0(times(x, y)), times(x, 2))
times(x, d3(y)) → plus(d0(times(x, y)), times(x, 3))
times(x, d4(y)) → plus(d0(times(x, y)), times(x, 4))
times(x, d5(y)) → plus(d0(times(x, y)), times(x, 5))
times(x, d6(y)) → plus(d0(times(x, y)), times(x, 6))
times(x, d7(y)) → plus(d0(times(x, y)), times(x, 7))
times(x, d8(y)) → plus(d0(times(x, y)), times(x, 8))
times(x, d9(y)) → plus(d0(times(x, y)), times(x, 9))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
p(m(x)) → m(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d9(p(x)))
d2(m(x)) → m(d8(p(x)))
d3(m(x)) → m(d7(p(x)))
d4(m(x)) → m(d6(p(x)))
d5(m(x)) → m(d5(p(x)))
d6(m(x)) → m(d4(p(x)))
d7(m(x)) → m(d3(p(x)))
d8(m(x)) → m(d2(p(x)))
d9(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(51) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(52) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(d9(x)) → S(x)

R is empty.
The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(53) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(d9(x)) → S(x)

R is empty.
The set Q consists of the following terms:

d9(0)
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(55) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • S(d9(x)) → S(x)
    The graph contains the following edges 1 > 1

(56) YES

(57) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → PLUS(x, d0(y))
PLUS(x, d3(y)) → PLUS(x, d0(y))
PLUS(x, d4(y)) → PLUS(x, d0(y))
PLUS(x, d5(y)) → PLUS(x, d0(y))
PLUS(x, d6(y)) → PLUS(x, d0(y))
PLUS(x, d7(y)) → PLUS(x, d0(y))
PLUS(x, d8(y)) → PLUS(x, d0(y))
PLUS(x, d9(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
d2(0) → 2
d3(0) → 3
d4(0) → 4
d5(0) → 5
d6(0) → 6
d7(0) → 7
d8(0) → 8
d9(0) → 9
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
times(x, 0) → 0
times(x, 1) → plus(times(x, 0), x)
times(x, 2) → plus(times(x, 1), x)
times(x, 3) → plus(times(x, 2), x)
times(x, 4) → plus(times(x, 3), x)
times(x, 5) → plus(times(x, 4), x)
times(x, 6) → plus(times(x, 5), x)
times(x, 7) → plus(times(x, 6), x)
times(x, 8) → plus(times(x, 7), x)
times(x, 9) → plus(times(x, 8), x)
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, d2(y)) → plus(d0(times(x, y)), times(x, 2))
times(x, d3(y)) → plus(d0(times(x, y)), times(x, 3))
times(x, d4(y)) → plus(d0(times(x, y)), times(x, 4))
times(x, d5(y)) → plus(d0(times(x, y)), times(x, 5))
times(x, d6(y)) → plus(d0(times(x, y)), times(x, 6))
times(x, d7(y)) → plus(d0(times(x, y)), times(x, 7))
times(x, d8(y)) → plus(d0(times(x, y)), times(x, 8))
times(x, d9(y)) → plus(d0(times(x, y)), times(x, 9))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
p(m(x)) → m(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d9(p(x)))
d2(m(x)) → m(d8(p(x)))
d3(m(x)) → m(d7(p(x)))
d4(m(x)) → m(d6(p(x)))
d5(m(x)) → m(d5(p(x)))
d6(m(x)) → m(d4(p(x)))
d7(m(x)) → m(d3(p(x)))
d8(m(x)) → m(d2(p(x)))
d9(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(58) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(59) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → PLUS(x, d0(y))
PLUS(x, d3(y)) → PLUS(x, d0(y))
PLUS(x, d4(y)) → PLUS(x, d0(y))
PLUS(x, d5(y)) → PLUS(x, d0(y))
PLUS(x, d6(y)) → PLUS(x, d0(y))
PLUS(x, d7(y)) → PLUS(x, d0(y))
PLUS(x, d8(y)) → PLUS(x, d0(y))
PLUS(x, d9(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(60) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
times(x0, m(x1))

(61) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → PLUS(x, d0(y))
PLUS(x, d3(y)) → PLUS(x, d0(y))
PLUS(x, d4(y)) → PLUS(x, d0(y))
PLUS(x, d5(y)) → PLUS(x, d0(y))
PLUS(x, d6(y)) → PLUS(x, d0(y))
PLUS(x, d7(y)) → PLUS(x, d0(y))
PLUS(x, d8(y)) → PLUS(x, d0(y))
PLUS(x, d9(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(62) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PLUS(x, d9(y)) → PLUS(x, d0(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x2
d0(x1)  =  x1
d1(x1)  =  x1
d2(x1)  =  x1
d3(x1)  =  x1
d4(x1)  =  x1
d5(x1)  =  x1
d6(x1)  =  x1
d7(x1)  =  x1
d8(x1)  =  x1
d9(x1)  =  d9(x1)
0  =  0
m(x1)  =  x1

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

dummyConstant=1
d9_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(63) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → PLUS(x, d0(y))
PLUS(x, d3(y)) → PLUS(x, d0(y))
PLUS(x, d4(y)) → PLUS(x, d0(y))
PLUS(x, d5(y)) → PLUS(x, d0(y))
PLUS(x, d6(y)) → PLUS(x, d0(y))
PLUS(x, d7(y)) → PLUS(x, d0(y))
PLUS(x, d8(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(64) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PLUS(x, d8(y)) → PLUS(x, d0(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x2
d0(x1)  =  x1
d1(x1)  =  x1
d2(x1)  =  x1
d3(x1)  =  x1
d4(x1)  =  x1
d5(x1)  =  x1
d6(x1)  =  x1
d7(x1)  =  x1
d8(x1)  =  d8(x1)
0  =  0
m(x1)  =  x1

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

dummyConstant=1
d8_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(65) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → PLUS(x, d0(y))
PLUS(x, d3(y)) → PLUS(x, d0(y))
PLUS(x, d4(y)) → PLUS(x, d0(y))
PLUS(x, d5(y)) → PLUS(x, d0(y))
PLUS(x, d6(y)) → PLUS(x, d0(y))
PLUS(x, d7(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(66) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PLUS(x, d7(y)) → PLUS(x, d0(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x2
d0(x1)  =  x1
d1(x1)  =  x1
d2(x1)  =  x1
d3(x1)  =  x1
d4(x1)  =  x1
d5(x1)  =  x1
d6(x1)  =  x1
d7(x1)  =  d7(x1)
0  =  0
m(x1)  =  x1

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

dummyConstant=1
d7_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(67) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → PLUS(x, d0(y))
PLUS(x, d3(y)) → PLUS(x, d0(y))
PLUS(x, d4(y)) → PLUS(x, d0(y))
PLUS(x, d5(y)) → PLUS(x, d0(y))
PLUS(x, d6(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(68) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PLUS(x, d6(y)) → PLUS(x, d0(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x2
d0(x1)  =  x1
d1(x1)  =  x1
d2(x1)  =  x1
d3(x1)  =  x1
d4(x1)  =  x1
d5(x1)  =  x1
d6(x1)  =  d6(x1)
0  =  0
m(x1)  =  x1

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

dummyConstant=1
d6_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(69) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → PLUS(x, d0(y))
PLUS(x, d3(y)) → PLUS(x, d0(y))
PLUS(x, d4(y)) → PLUS(x, d0(y))
PLUS(x, d5(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(70) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PLUS(x, d5(y)) → PLUS(x, d0(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x2
d0(x1)  =  x1
d1(x1)  =  x1
d2(x1)  =  x1
d3(x1)  =  x1
d4(x1)  =  x1
d5(x1)  =  d5(x1)
0  =  0
m(x1)  =  x1

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

dummyConstant=1
d5_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(71) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → PLUS(x, d0(y))
PLUS(x, d3(y)) → PLUS(x, d0(y))
PLUS(x, d4(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(72) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PLUS(x, d4(y)) → PLUS(x, d0(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x2
d0(x1)  =  x1
d1(x1)  =  x1
d2(x1)  =  x1
d3(x1)  =  x1
d4(x1)  =  d4(x1)
0  =  0
m(x1)  =  x1

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

dummyConstant=1
d4_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(73) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → PLUS(x, d0(y))
PLUS(x, d3(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(74) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PLUS(x, d3(y)) → PLUS(x, d0(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x2
d0(x1)  =  x1
d1(x1)  =  x1
d2(x1)  =  x1
d3(x1)  =  d3(x1)
0  =  0
m(x1)  =  x1

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

d3_1=1
dummyConstant=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(75) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))
PLUS(x, d2(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(76) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PLUS(x, d2(y)) → PLUS(x, d0(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x2
d0(x1)  =  x1
d1(x1)  =  x1
d2(x1)  =  d2(x1)
0  =  0
m(x1)  =  x1

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

dummyConstant=1
d2_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(77) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)
PLUS(x, d1(y)) → PLUS(x, d0(y))

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(78) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


PLUS(x, d1(y)) → PLUS(x, d0(y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x2
d0(x1)  =  x1
d1(x1)  =  d1(x1)
0  =  0
m(x1)  =  x1

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

dummyConstant=1
d1_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(79) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
PLUS(x, d0(y)) → PLUS(plus(x, y), y)
PLUS(x, d0(y)) → PLUS(x, y)

The TRS R consists of the following rules:

plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
d9(0) → 9
d9(m(x)) → m(d1(p(x)))
m(0) → 0
m(m(x)) → x
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
d0(0) → 0
d0(m(x)) → m(d0(x))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(80) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y)
    The graph contains the following edges 2 > 2

  • PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
    The graph contains the following edges 2 > 2

  • PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y)
    The graph contains the following edges 2 > 2

  • PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y)
    The graph contains the following edges 2 > 2

  • PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(plus(x, y), y), y), y), y), y)
    The graph contains the following edges 2 > 2

  • PLUS(x, d0(y)) → PLUS(plus(plus(plus(plus(x, y), y), y), y), y)
    The graph contains the following edges 2 > 2

  • PLUS(x, d0(y)) → PLUS(plus(plus(plus(x, y), y), y), y)
    The graph contains the following edges 2 > 2

  • PLUS(x, d0(y)) → PLUS(plus(plus(x, y), y), y)
    The graph contains the following edges 2 > 2

  • PLUS(x, d0(y)) → PLUS(plus(x, y), y)
    The graph contains the following edges 2 > 2

  • PLUS(x, d0(y)) → PLUS(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

(81) YES

(82) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(x, d1(y)) → TIMES(x, y)
TIMES(x, d0(y)) → TIMES(x, y)
TIMES(x, d2(y)) → TIMES(x, y)
TIMES(x, d3(y)) → TIMES(x, y)
TIMES(x, d4(y)) → TIMES(x, y)
TIMES(x, d5(y)) → TIMES(x, y)
TIMES(x, d6(y)) → TIMES(x, y)
TIMES(x, d7(y)) → TIMES(x, y)
TIMES(x, d8(y)) → TIMES(x, y)
TIMES(x, d9(y)) → TIMES(x, y)

The TRS R consists of the following rules:

d0(0) → 0
d1(0) → 1
d2(0) → 2
d3(0) → 3
d4(0) → 4
d5(0) → 5
d6(0) → 6
d7(0) → 7
d8(0) → 8
d9(0) → 9
s(0) → 1
s(1) → 2
s(2) → 3
s(3) → 4
s(4) → 5
s(5) → 6
s(6) → 7
s(7) → 8
s(8) → 9
s(9) → d0(1)
s(d0(x)) → d1(x)
s(d1(x)) → d2(x)
s(d2(x)) → d3(x)
s(d3(x)) → d4(x)
s(d4(x)) → d5(x)
s(d5(x)) → d6(x)
s(d6(x)) → d7(x)
s(d7(x)) → d8(x)
s(d8(x)) → d9(x)
s(d9(x)) → d0(s(x))
plus(x, 0) → x
plus(x, 1) → s(x)
plus(x, 2) → s(s(x))
plus(x, 3) → s(s(s(x)))
plus(x, 4) → s(s(s(s(x))))
plus(x, 5) → s(s(s(s(s(x)))))
plus(x, 6) → s(s(s(s(s(s(x))))))
plus(x, 7) → s(s(s(s(s(s(s(x)))))))
plus(x, 8) → s(s(s(s(s(s(s(s(x))))))))
plus(x, 9) → s(s(s(s(s(s(s(s(s(x)))))))))
plus(x, d0(y)) → plus(plus(plus(plus(plus(plus(plus(plus(plus(plus(x, y), y), y), y), y), y), y), y), y), y)
plus(x, d1(y)) → s(plus(x, d0(y)))
plus(x, d2(y)) → s(s(plus(x, d0(y))))
plus(x, d3(y)) → s(s(s(plus(x, d0(y)))))
plus(x, d4(y)) → s(s(s(s(plus(x, d0(y))))))
plus(x, d5(y)) → s(s(s(s(s(plus(x, d0(y)))))))
plus(x, d6(y)) → s(s(s(s(s(s(plus(x, d0(y))))))))
plus(x, d7(y)) → s(s(s(s(s(s(s(plus(x, d0(y)))))))))
plus(x, d8(y)) → s(s(s(s(s(s(s(s(plus(x, d0(y))))))))))
plus(x, d9(y)) → s(s(s(s(s(s(s(s(s(plus(x, d0(y)))))))))))
times(x, 0) → 0
times(x, 1) → plus(times(x, 0), x)
times(x, 2) → plus(times(x, 1), x)
times(x, 3) → plus(times(x, 2), x)
times(x, 4) → plus(times(x, 3), x)
times(x, 5) → plus(times(x, 4), x)
times(x, 6) → plus(times(x, 5), x)
times(x, 7) → plus(times(x, 6), x)
times(x, 8) → plus(times(x, 7), x)
times(x, 9) → plus(times(x, 8), x)
times(x, d0(y)) → plus(d0(times(x, y)), times(x, 0))
times(x, d1(y)) → plus(d0(times(x, y)), times(x, 1))
times(x, d2(y)) → plus(d0(times(x, y)), times(x, 2))
times(x, d3(y)) → plus(d0(times(x, y)), times(x, 3))
times(x, d4(y)) → plus(d0(times(x, y)), times(x, 4))
times(x, d5(y)) → plus(d0(times(x, y)), times(x, 5))
times(x, d6(y)) → plus(d0(times(x, y)), times(x, 6))
times(x, d7(y)) → plus(d0(times(x, y)), times(x, 7))
times(x, d8(y)) → plus(d0(times(x, y)), times(x, 8))
times(x, d9(y)) → plus(d0(times(x, y)), times(x, 9))
m(0) → 0
m(m(x)) → x
p(0) → m(1)
p(1) → 0
p(2) → 1
p(3) → 2
p(4) → 3
p(5) → 4
p(6) → 5
p(7) → 6
p(8) → 7
p(9) → 8
p(d0(x)) → d9(p(x))
p(d1(x)) → d0(x)
p(d2(x)) → d1(x)
p(d3(x)) → d2(x)
p(d4(x)) → d3(x)
p(d5(x)) → d4(x)
p(d6(x)) → d5(x)
p(d7(x)) → d6(x)
p(d8(x)) → d7(x)
p(d9(x)) → d8(x)
p(m(x)) → m(s(x))
s(m(1)) → m(0)
s(m(2)) → m(1)
s(m(3)) → m(2)
s(m(4)) → m(3)
s(m(5)) → m(4)
s(m(6)) → m(5)
s(m(7)) → m(6)
s(m(8)) → m(7)
s(m(9)) → m(8)
s(m(d0(x))) → m(d9(p(x)))
s(m(d1(x))) → m(d0(x))
s(m(d2(x))) → m(d1(x))
s(m(d3(x))) → m(d2(x))
s(m(d4(x))) → m(d3(x))
s(m(d5(x))) → m(d4(x))
s(m(d6(x))) → m(d5(x))
s(m(d7(x))) → m(d6(x))
s(m(d8(x))) → m(d7(x))
s(m(d9(x))) → m(d8(x))
d0(m(x)) → m(d0(x))
d1(m(x)) → m(d9(p(x)))
d2(m(x)) → m(d8(p(x)))
d3(m(x)) → m(d7(p(x)))
d4(m(x)) → m(d6(p(x)))
d5(m(x)) → m(d5(p(x)))
d6(m(x)) → m(d4(p(x)))
d7(m(x)) → m(d3(p(x)))
d8(m(x)) → m(d2(p(x)))
d9(m(x)) → m(d1(p(x)))
plus(x, m(y)) → m(plus(m(x), y))
times(x, m(y)) → m(times(x, y))

The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(83) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(84) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(x, d1(y)) → TIMES(x, y)
TIMES(x, d0(y)) → TIMES(x, y)
TIMES(x, d2(y)) → TIMES(x, y)
TIMES(x, d3(y)) → TIMES(x, y)
TIMES(x, d4(y)) → TIMES(x, y)
TIMES(x, d5(y)) → TIMES(x, y)
TIMES(x, d6(y)) → TIMES(x, y)
TIMES(x, d7(y)) → TIMES(x, y)
TIMES(x, d8(y)) → TIMES(x, y)
TIMES(x, d9(y)) → TIMES(x, y)

R is empty.
The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))
plus(x0, m(x1))
times(x0, m(x1))

We have to consider all minimal (P,Q,R)-chains.

(85) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

s(0)
s(1)
s(2)
s(3)
s(4)
s(5)
s(6)
s(7)
s(8)
s(9)
s(d0(x0))
s(d1(x0))
s(d2(x0))
s(d3(x0))
s(d4(x0))
s(d5(x0))
s(d6(x0))
s(d7(x0))
s(d8(x0))
s(d9(x0))
plus(x0, 0)
plus(x0, 1)
plus(x0, 2)
plus(x0, 3)
plus(x0, 4)
plus(x0, 5)
plus(x0, 6)
plus(x0, 7)
plus(x0, 8)
plus(x0, 9)
plus(x0, d0(x1))
plus(x0, d1(x1))
plus(x0, d2(x1))
plus(x0, d3(x1))
plus(x0, d4(x1))
plus(x0, d5(x1))
plus(x0, d6(x1))
plus(x0, d7(x1))
plus(x0, d8(x1))
plus(x0, d9(x1))
times(x0, 0)
times(x0, 1)
times(x0, 2)
times(x0, 3)
times(x0, 4)
times(x0, 5)
times(x0, 6)
times(x0, 7)
times(x0, 8)
times(x0, 9)
times(x0, d0(x1))
times(x0, d1(x1))
times(x0, d2(x1))
times(x0, d3(x1))
times(x0, d4(x1))
times(x0, d5(x1))
times(x0, d6(x1))
times(x0, d7(x1))
times(x0, d8(x1))
times(x0, d9(x1))
m(0)
m(m(x0))
p(0)
p(1)
p(2)
p(3)
p(4)
p(5)
p(6)
p(7)
p(8)
p(9)
p(d0(x0))
p(d1(x0))
p(d2(x0))
p(d3(x0))
p(d4(x0))
p(d5(x0))
p(d6(x0))
p(d7(x0))
p(d8(x0))
p(d9(x0))
p(m(x0))
s(m(1))
s(m(2))
s(m(3))
s(m(4))
s(m(5))
s(m(6))
s(m(7))
s(m(8))
s(m(9))
s(m(d0(x0)))
s(m(d1(x0)))
s(m(d2(x0)))
s(m(d3(x0)))
s(m(d4(x0)))
s(m(d5(x0)))
s(m(d6(x0)))
s(m(d7(x0)))
s(m(d8(x0)))
s(m(d9(x0)))
plus(x0, m(x1))
times(x0, m(x1))

(86) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(x, d1(y)) → TIMES(x, y)
TIMES(x, d0(y)) → TIMES(x, y)
TIMES(x, d2(y)) → TIMES(x, y)
TIMES(x, d3(y)) → TIMES(x, y)
TIMES(x, d4(y)) → TIMES(x, y)
TIMES(x, d5(y)) → TIMES(x, y)
TIMES(x, d6(y)) → TIMES(x, y)
TIMES(x, d7(y)) → TIMES(x, y)
TIMES(x, d8(y)) → TIMES(x, y)
TIMES(x, d9(y)) → TIMES(x, y)

R is empty.
The set Q consists of the following terms:

d0(0)
d1(0)
d2(0)
d3(0)
d4(0)
d5(0)
d6(0)
d7(0)
d8(0)
d9(0)
d0(m(x0))
d1(m(x0))
d2(m(x0))
d3(m(x0))
d4(m(x0))
d5(m(x0))
d6(m(x0))
d7(m(x0))
d8(m(x0))
d9(m(x0))

We have to consider all minimal (P,Q,R)-chains.

(87) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • TIMES(x, d1(y)) → TIMES(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • TIMES(x, d0(y)) → TIMES(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • TIMES(x, d2(y)) → TIMES(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • TIMES(x, d3(y)) → TIMES(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • TIMES(x, d4(y)) → TIMES(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • TIMES(x, d5(y)) → TIMES(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • TIMES(x, d6(y)) → TIMES(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • TIMES(x, d7(y)) → TIMES(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • TIMES(x, d8(y)) → TIMES(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • TIMES(x, d9(y)) → TIMES(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

(88) YES