Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 DependencyPairsProof (⇔, 169 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
    ↳5 QDP
        ↳6 UsableRulesProof (⇔, 0 ms)
        ↳7 QDP
        ↳8 QReductionProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 QDPSizeChangeProof (⇔, 0 ms)
        ↳11 YES
    ↳12 QDP
        ↳13 UsableRulesProof (⇔, 0 ms)
        ↳14 QDP
        ↳15 QReductionProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 QDPSizeChangeProof (⇔, 0 ms)
        ↳18 YES
    ↳19 QDP
        ↳20 UsableRulesProof (⇔, 0 ms)
        ↳21 QDP
        ↳22 QReductionProof (⇔, 0 ms)
        ↳23 QDP
        ↳24 QDPSizeChangeProof (⇔, 0 ms)
        ↳25 YES

(0) Obligation:

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

dt(0, x) → x
dt(x, dt(y, z)) → dt(plus(x, y), z)
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) → dt(1, 0)
S(dt(x, 0)) → dt(x, 1)
S(dt(x, 1)) → dt(x, 2)
S(dt(x, 2)) → dt(x, 3)
S(dt(x, 3)) → dt(x, 4)
S(dt(x, 4)) → dt(x, 5)
S(dt(x, 5)) → dt(x, 6)
S(dt(x, 6)) → dt(x, 7)
S(dt(x, 7)) → dt(x, 8)
S(dt(x, 8)) → dt(x, 9)
S(dt(x, 9)) → dt(S(x), 0)
plus(x, 0) → x
plus(x, 1) → plus(S(x), 0)
plus(x, 2) → plus(S(x), 1)
plus(x, 3) → plus(S(x), 2)
plus(x, 4) → plus(S(x), 3)
plus(x, 5) → plus(S(x), 4)
plus(x, 6) → plus(S(x), 5)
plus(x, 7) → plus(S(x), 6)
plus(x, 8) → plus(S(x), 7)
plus(x, 9) → plus(S(x), 8)
plus(x, dt(y, 0)) → plus(dt(y, x), 0)
plus(x, dt(y, 1)) → plus(dt(y, x), 1)
plus(x, dt(y, 2)) → plus(dt(y, x), 2)
plus(x, dt(y, 3)) → plus(dt(y, x), 3)
plus(x, dt(y, 4)) → plus(dt(y, x), 4)
plus(x, dt(y, 5)) → plus(dt(y, x), 5)
plus(x, dt(y, 6)) → plus(dt(y, x), 6)
plus(x, dt(y, 7)) → plus(dt(y, x), 7)
plus(x, dt(y, 8)) → plus(dt(y, x), 8)
plus(x, dt(y, 9)) → plus(dt(y, x), 9)
mult(x, 0) → 0
mult(x, 1) → plus(x, mult(x, 0))
mult(x, 2) → plus(x, mult(x, 1))
mult(x, 3) → plus(x, mult(x, 2))
mult(x, 4) → plus(x, mult(x, 3))
mult(x, 5) → plus(x, mult(x, 4))
mult(x, 6) → plus(x, mult(x, 5))
mult(x, 7) → plus(x, mult(x, 6))
mult(x, 8) → plus(x, mult(x, 7))
mult(x, 9) → plus(x, mult(x, 8))
mult(x, dt(y, 0)) → plus(dt(mult(x, y), 0), mult(x, 0))
mult(x, dt(y, 1)) → plus(dt(mult(x, y), 0), mult(x, 1))
mult(x, dt(y, 2)) → plus(dt(mult(x, y), 0), mult(x, 2))
mult(x, dt(y, 3)) → plus(dt(mult(x, y), 0), mult(x, 3))
mult(x, dt(y, 4)) → plus(dt(mult(x, y), 0), mult(x, 4))
mult(x, dt(y, 5)) → plus(dt(mult(x, y), 0), mult(x, 5))
mult(x, dt(y, 6)) → plus(dt(mult(x, y), 0), mult(x, 6))
mult(x, dt(y, 7)) → plus(dt(mult(x, y), 0), mult(x, 7))
mult(x, dt(y, 8)) → plus(dt(mult(x, y), 0), mult(x, 8))
mult(x, dt(y, 9)) → plus(dt(mult(x, y), 0), mult(x, 9))

The set Q consists of the following terms:

dt(0, x0)
dt(x0, dt(x1, x2))
S(0)
S(1)
S(2)
S(3)
S(4)
S(5)
S(6)
S(7)
S(8)
S(9)
S(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

(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:

DT(x, dt(y, z)) → DT(plus(x, y), z)
DT(x, dt(y, z)) → PLUS(x, y)
S1(9) → DT(1, 0)
S1(dt(x, 0)) → DT(x, 1)
S1(dt(x, 1)) → DT(x, 2)
S1(dt(x, 2)) → DT(x, 3)
S1(dt(x, 3)) → DT(x, 4)
S1(dt(x, 4)) → DT(x, 5)
S1(dt(x, 5)) → DT(x, 6)
S1(dt(x, 6)) → DT(x, 7)
S1(dt(x, 7)) → DT(x, 8)
S1(dt(x, 8)) → DT(x, 9)
S1(dt(x, 9)) → DT(S(x), 0)
S1(dt(x, 9)) → S1(x)
PLUS(x, 1) → PLUS(S(x), 0)
PLUS(x, 1) → S1(x)
PLUS(x, 2) → PLUS(S(x), 1)
PLUS(x, 2) → S1(x)
PLUS(x, 3) → PLUS(S(x), 2)
PLUS(x, 3) → S1(x)
PLUS(x, 4) → PLUS(S(x), 3)
PLUS(x, 4) → S1(x)
PLUS(x, 5) → PLUS(S(x), 4)
PLUS(x, 5) → S1(x)
PLUS(x, 6) → PLUS(S(x), 5)
PLUS(x, 6) → S1(x)
PLUS(x, 7) → PLUS(S(x), 6)
PLUS(x, 7) → S1(x)
PLUS(x, 8) → PLUS(S(x), 7)
PLUS(x, 8) → S1(x)
PLUS(x, 9) → PLUS(S(x), 8)
PLUS(x, 9) → S1(x)
PLUS(x, dt(y, 0)) → PLUS(dt(y, x), 0)
PLUS(x, dt(y, 0)) → DT(y, x)
PLUS(x, dt(y, 1)) → PLUS(dt(y, x), 1)
PLUS(x, dt(y, 1)) → DT(y, x)
PLUS(x, dt(y, 2)) → PLUS(dt(y, x), 2)
PLUS(x, dt(y, 2)) → DT(y, x)
PLUS(x, dt(y, 3)) → PLUS(dt(y, x), 3)
PLUS(x, dt(y, 3)) → DT(y, x)
PLUS(x, dt(y, 4)) → PLUS(dt(y, x), 4)
PLUS(x, dt(y, 4)) → DT(y, x)
PLUS(x, dt(y, 5)) → PLUS(dt(y, x), 5)
PLUS(x, dt(y, 5)) → DT(y, x)
PLUS(x, dt(y, 6)) → PLUS(dt(y, x), 6)
PLUS(x, dt(y, 6)) → DT(y, x)
PLUS(x, dt(y, 7)) → PLUS(dt(y, x), 7)
PLUS(x, dt(y, 7)) → DT(y, x)
PLUS(x, dt(y, 8)) → PLUS(dt(y, x), 8)
PLUS(x, dt(y, 8)) → DT(y, x)
PLUS(x, dt(y, 9)) → PLUS(dt(y, x), 9)
PLUS(x, dt(y, 9)) → DT(y, x)
MULT(x, 1) → PLUS(x, mult(x, 0))
MULT(x, 1) → MULT(x, 0)
MULT(x, 2) → PLUS(x, mult(x, 1))
MULT(x, 2) → MULT(x, 1)
MULT(x, 3) → PLUS(x, mult(x, 2))
MULT(x, 3) → MULT(x, 2)
MULT(x, 4) → PLUS(x, mult(x, 3))
MULT(x, 4) → MULT(x, 3)
MULT(x, 5) → PLUS(x, mult(x, 4))
MULT(x, 5) → MULT(x, 4)
MULT(x, 6) → PLUS(x, mult(x, 5))
MULT(x, 6) → MULT(x, 5)
MULT(x, 7) → PLUS(x, mult(x, 6))
MULT(x, 7) → MULT(x, 6)
MULT(x, 8) → PLUS(x, mult(x, 7))
MULT(x, 8) → MULT(x, 7)
MULT(x, 9) → PLUS(x, mult(x, 8))
MULT(x, 9) → MULT(x, 8)
MULT(x, dt(y, 0)) → PLUS(dt(mult(x, y), 0), mult(x, 0))
MULT(x, dt(y, 0)) → DT(mult(x, y), 0)
MULT(x, dt(y, 0)) → MULT(x, y)
MULT(x, dt(y, 0)) → MULT(x, 0)
MULT(x, dt(y, 1)) → PLUS(dt(mult(x, y), 0), mult(x, 1))
MULT(x, dt(y, 1)) → DT(mult(x, y), 0)
MULT(x, dt(y, 1)) → MULT(x, y)
MULT(x, dt(y, 1)) → MULT(x, 1)
MULT(x, dt(y, 2)) → PLUS(dt(mult(x, y), 0), mult(x, 2))
MULT(x, dt(y, 2)) → DT(mult(x, y), 0)
MULT(x, dt(y, 2)) → MULT(x, y)
MULT(x, dt(y, 2)) → MULT(x, 2)
MULT(x, dt(y, 3)) → PLUS(dt(mult(x, y), 0), mult(x, 3))
MULT(x, dt(y, 3)) → DT(mult(x, y), 0)
MULT(x, dt(y, 3)) → MULT(x, y)
MULT(x, dt(y, 3)) → MULT(x, 3)
MULT(x, dt(y, 4)) → PLUS(dt(mult(x, y), 0), mult(x, 4))
MULT(x, dt(y, 4)) → DT(mult(x, y), 0)
MULT(x, dt(y, 4)) → MULT(x, y)
MULT(x, dt(y, 4)) → MULT(x, 4)
MULT(x, dt(y, 5)) → PLUS(dt(mult(x, y), 0), mult(x, 5))
MULT(x, dt(y, 5)) → DT(mult(x, y), 0)
MULT(x, dt(y, 5)) → MULT(x, y)
MULT(x, dt(y, 5)) → MULT(x, 5)
MULT(x, dt(y, 6)) → PLUS(dt(mult(x, y), 0), mult(x, 6))
MULT(x, dt(y, 6)) → DT(mult(x, y), 0)
MULT(x, dt(y, 6)) → MULT(x, y)
MULT(x, dt(y, 6)) → MULT(x, 6)
MULT(x, dt(y, 7)) → PLUS(dt(mult(x, y), 0), mult(x, 7))
MULT(x, dt(y, 7)) → DT(mult(x, y), 0)
MULT(x, dt(y, 7)) → MULT(x, y)
MULT(x, dt(y, 7)) → MULT(x, 7)
MULT(x, dt(y, 8)) → PLUS(dt(mult(x, y), 0), mult(x, 8))
MULT(x, dt(y, 8)) → DT(mult(x, y), 0)
MULT(x, dt(y, 8)) → MULT(x, y)
MULT(x, dt(y, 8)) → MULT(x, 8)
MULT(x, dt(y, 9)) → PLUS(dt(mult(x, y), 0), mult(x, 9))
MULT(x, dt(y, 9)) → DT(mult(x, y), 0)
MULT(x, dt(y, 9)) → MULT(x, y)
MULT(x, dt(y, 9)) → MULT(x, 9)

The TRS R consists of the following rules:

dt(0, x) → x
dt(x, dt(y, z)) → dt(plus(x, y), z)
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) → dt(1, 0)
S(dt(x, 0)) → dt(x, 1)
S(dt(x, 1)) → dt(x, 2)
S(dt(x, 2)) → dt(x, 3)
S(dt(x, 3)) → dt(x, 4)
S(dt(x, 4)) → dt(x, 5)
S(dt(x, 5)) → dt(x, 6)
S(dt(x, 6)) → dt(x, 7)
S(dt(x, 7)) → dt(x, 8)
S(dt(x, 8)) → dt(x, 9)
S(dt(x, 9)) → dt(S(x), 0)
plus(x, 0) → x
plus(x, 1) → plus(S(x), 0)
plus(x, 2) → plus(S(x), 1)
plus(x, 3) → plus(S(x), 2)
plus(x, 4) → plus(S(x), 3)
plus(x, 5) → plus(S(x), 4)
plus(x, 6) → plus(S(x), 5)
plus(x, 7) → plus(S(x), 6)
plus(x, 8) → plus(S(x), 7)
plus(x, 9) → plus(S(x), 8)
plus(x, dt(y, 0)) → plus(dt(y, x), 0)
plus(x, dt(y, 1)) → plus(dt(y, x), 1)
plus(x, dt(y, 2)) → plus(dt(y, x), 2)
plus(x, dt(y, 3)) → plus(dt(y, x), 3)
plus(x, dt(y, 4)) → plus(dt(y, x), 4)
plus(x, dt(y, 5)) → plus(dt(y, x), 5)
plus(x, dt(y, 6)) → plus(dt(y, x), 6)
plus(x, dt(y, 7)) → plus(dt(y, x), 7)
plus(x, dt(y, 8)) → plus(dt(y, x), 8)
plus(x, dt(y, 9)) → plus(dt(y, x), 9)
mult(x, 0) → 0
mult(x, 1) → plus(x, mult(x, 0))
mult(x, 2) → plus(x, mult(x, 1))
mult(x, 3) → plus(x, mult(x, 2))
mult(x, 4) → plus(x, mult(x, 3))
mult(x, 5) → plus(x, mult(x, 4))
mult(x, 6) → plus(x, mult(x, 5))
mult(x, 7) → plus(x, mult(x, 6))
mult(x, 8) → plus(x, mult(x, 7))
mult(x, 9) → plus(x, mult(x, 8))
mult(x, dt(y, 0)) → plus(dt(mult(x, y), 0), mult(x, 0))
mult(x, dt(y, 1)) → plus(dt(mult(x, y), 0), mult(x, 1))
mult(x, dt(y, 2)) → plus(dt(mult(x, y), 0), mult(x, 2))
mult(x, dt(y, 3)) → plus(dt(mult(x, y), 0), mult(x, 3))
mult(x, dt(y, 4)) → plus(dt(mult(x, y), 0), mult(x, 4))
mult(x, dt(y, 5)) → plus(dt(mult(x, y), 0), mult(x, 5))
mult(x, dt(y, 6)) → plus(dt(mult(x, y), 0), mult(x, 6))
mult(x, dt(y, 7)) → plus(dt(mult(x, y), 0), mult(x, 7))
mult(x, dt(y, 8)) → plus(dt(mult(x, y), 0), mult(x, 8))
mult(x, dt(y, 9)) → plus(dt(mult(x, y), 0), mult(x, 9))

The set Q consists of the following terms:

dt(0, x0)
dt(x0, dt(x1, x2))
S(0)
S(1)
S(2)
S(3)
S(4)
S(5)
S(6)
S(7)
S(8)
S(9)
S(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

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

S1(dt(x, 9)) → S1(x)

The TRS R consists of the following rules:

dt(0, x) → x
dt(x, dt(y, z)) → dt(plus(x, y), z)
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) → dt(1, 0)
S(dt(x, 0)) → dt(x, 1)
S(dt(x, 1)) → dt(x, 2)
S(dt(x, 2)) → dt(x, 3)
S(dt(x, 3)) → dt(x, 4)
S(dt(x, 4)) → dt(x, 5)
S(dt(x, 5)) → dt(x, 6)
S(dt(x, 6)) → dt(x, 7)
S(dt(x, 7)) → dt(x, 8)
S(dt(x, 8)) → dt(x, 9)
S(dt(x, 9)) → dt(S(x), 0)
plus(x, 0) → x
plus(x, 1) → plus(S(x), 0)
plus(x, 2) → plus(S(x), 1)
plus(x, 3) → plus(S(x), 2)
plus(x, 4) → plus(S(x), 3)
plus(x, 5) → plus(S(x), 4)
plus(x, 6) → plus(S(x), 5)
plus(x, 7) → plus(S(x), 6)
plus(x, 8) → plus(S(x), 7)
plus(x, 9) → plus(S(x), 8)
plus(x, dt(y, 0)) → plus(dt(y, x), 0)
plus(x, dt(y, 1)) → plus(dt(y, x), 1)
plus(x, dt(y, 2)) → plus(dt(y, x), 2)
plus(x, dt(y, 3)) → plus(dt(y, x), 3)
plus(x, dt(y, 4)) → plus(dt(y, x), 4)
plus(x, dt(y, 5)) → plus(dt(y, x), 5)
plus(x, dt(y, 6)) → plus(dt(y, x), 6)
plus(x, dt(y, 7)) → plus(dt(y, x), 7)
plus(x, dt(y, 8)) → plus(dt(y, x), 8)
plus(x, dt(y, 9)) → plus(dt(y, x), 9)
mult(x, 0) → 0
mult(x, 1) → plus(x, mult(x, 0))
mult(x, 2) → plus(x, mult(x, 1))
mult(x, 3) → plus(x, mult(x, 2))
mult(x, 4) → plus(x, mult(x, 3))
mult(x, 5) → plus(x, mult(x, 4))
mult(x, 6) → plus(x, mult(x, 5))
mult(x, 7) → plus(x, mult(x, 6))
mult(x, 8) → plus(x, mult(x, 7))
mult(x, 9) → plus(x, mult(x, 8))
mult(x, dt(y, 0)) → plus(dt(mult(x, y), 0), mult(x, 0))
mult(x, dt(y, 1)) → plus(dt(mult(x, y), 0), mult(x, 1))
mult(x, dt(y, 2)) → plus(dt(mult(x, y), 0), mult(x, 2))
mult(x, dt(y, 3)) → plus(dt(mult(x, y), 0), mult(x, 3))
mult(x, dt(y, 4)) → plus(dt(mult(x, y), 0), mult(x, 4))
mult(x, dt(y, 5)) → plus(dt(mult(x, y), 0), mult(x, 5))
mult(x, dt(y, 6)) → plus(dt(mult(x, y), 0), mult(x, 6))
mult(x, dt(y, 7)) → plus(dt(mult(x, y), 0), mult(x, 7))
mult(x, dt(y, 8)) → plus(dt(mult(x, y), 0), mult(x, 8))
mult(x, dt(y, 9)) → plus(dt(mult(x, y), 0), mult(x, 9))

The set Q consists of the following terms:

dt(0, x0)
dt(x0, dt(x1, x2))
S(0)
S(1)
S(2)
S(3)
S(4)
S(5)
S(6)
S(7)
S(8)
S(9)
S(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

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:

S1(dt(x, 9)) → S1(x)

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

dt(0, x0)
dt(x0, dt(x1, x2))
S(0)
S(1)
S(2)
S(3)
S(4)
S(5)
S(6)
S(7)
S(8)
S(9)
S(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

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(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

(9) Obligation:

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

S1(dt(x, 9)) → S1(x)

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

dt(0, x0)
dt(x0, dt(x1, x2))

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

(10) 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:

  • S1(dt(x, 9)) → S1(x)
    The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

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

DT(x, dt(y, z)) → PLUS(x, y)
PLUS(x, dt(y, 0)) → DT(y, x)
PLUS(x, dt(y, 1)) → DT(y, x)
PLUS(x, dt(y, 2)) → DT(y, x)
PLUS(x, dt(y, 3)) → DT(y, x)
PLUS(x, dt(y, 4)) → DT(y, x)
PLUS(x, dt(y, 5)) → DT(y, x)
PLUS(x, dt(y, 6)) → DT(y, x)
PLUS(x, dt(y, 7)) → DT(y, x)
PLUS(x, dt(y, 8)) → DT(y, x)
PLUS(x, dt(y, 9)) → DT(y, x)

The TRS R consists of the following rules:

dt(0, x) → x
dt(x, dt(y, z)) → dt(plus(x, y), z)
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) → dt(1, 0)
S(dt(x, 0)) → dt(x, 1)
S(dt(x, 1)) → dt(x, 2)
S(dt(x, 2)) → dt(x, 3)
S(dt(x, 3)) → dt(x, 4)
S(dt(x, 4)) → dt(x, 5)
S(dt(x, 5)) → dt(x, 6)
S(dt(x, 6)) → dt(x, 7)
S(dt(x, 7)) → dt(x, 8)
S(dt(x, 8)) → dt(x, 9)
S(dt(x, 9)) → dt(S(x), 0)
plus(x, 0) → x
plus(x, 1) → plus(S(x), 0)
plus(x, 2) → plus(S(x), 1)
plus(x, 3) → plus(S(x), 2)
plus(x, 4) → plus(S(x), 3)
plus(x, 5) → plus(S(x), 4)
plus(x, 6) → plus(S(x), 5)
plus(x, 7) → plus(S(x), 6)
plus(x, 8) → plus(S(x), 7)
plus(x, 9) → plus(S(x), 8)
plus(x, dt(y, 0)) → plus(dt(y, x), 0)
plus(x, dt(y, 1)) → plus(dt(y, x), 1)
plus(x, dt(y, 2)) → plus(dt(y, x), 2)
plus(x, dt(y, 3)) → plus(dt(y, x), 3)
plus(x, dt(y, 4)) → plus(dt(y, x), 4)
plus(x, dt(y, 5)) → plus(dt(y, x), 5)
plus(x, dt(y, 6)) → plus(dt(y, x), 6)
plus(x, dt(y, 7)) → plus(dt(y, x), 7)
plus(x, dt(y, 8)) → plus(dt(y, x), 8)
plus(x, dt(y, 9)) → plus(dt(y, x), 9)
mult(x, 0) → 0
mult(x, 1) → plus(x, mult(x, 0))
mult(x, 2) → plus(x, mult(x, 1))
mult(x, 3) → plus(x, mult(x, 2))
mult(x, 4) → plus(x, mult(x, 3))
mult(x, 5) → plus(x, mult(x, 4))
mult(x, 6) → plus(x, mult(x, 5))
mult(x, 7) → plus(x, mult(x, 6))
mult(x, 8) → plus(x, mult(x, 7))
mult(x, 9) → plus(x, mult(x, 8))
mult(x, dt(y, 0)) → plus(dt(mult(x, y), 0), mult(x, 0))
mult(x, dt(y, 1)) → plus(dt(mult(x, y), 0), mult(x, 1))
mult(x, dt(y, 2)) → plus(dt(mult(x, y), 0), mult(x, 2))
mult(x, dt(y, 3)) → plus(dt(mult(x, y), 0), mult(x, 3))
mult(x, dt(y, 4)) → plus(dt(mult(x, y), 0), mult(x, 4))
mult(x, dt(y, 5)) → plus(dt(mult(x, y), 0), mult(x, 5))
mult(x, dt(y, 6)) → plus(dt(mult(x, y), 0), mult(x, 6))
mult(x, dt(y, 7)) → plus(dt(mult(x, y), 0), mult(x, 7))
mult(x, dt(y, 8)) → plus(dt(mult(x, y), 0), mult(x, 8))
mult(x, dt(y, 9)) → plus(dt(mult(x, y), 0), mult(x, 9))

The set Q consists of the following terms:

dt(0, x0)
dt(x0, dt(x1, x2))
S(0)
S(1)
S(2)
S(3)
S(4)
S(5)
S(6)
S(7)
S(8)
S(9)
S(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

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

(13) 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.

(14) Obligation:

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

DT(x, dt(y, z)) → PLUS(x, y)
PLUS(x, dt(y, 0)) → DT(y, x)
PLUS(x, dt(y, 1)) → DT(y, x)
PLUS(x, dt(y, 2)) → DT(y, x)
PLUS(x, dt(y, 3)) → DT(y, x)
PLUS(x, dt(y, 4)) → DT(y, x)
PLUS(x, dt(y, 5)) → DT(y, x)
PLUS(x, dt(y, 6)) → DT(y, x)
PLUS(x, dt(y, 7)) → DT(y, x)
PLUS(x, dt(y, 8)) → DT(y, x)
PLUS(x, dt(y, 9)) → DT(y, x)

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

dt(0, x0)
dt(x0, dt(x1, x2))
S(0)
S(1)
S(2)
S(3)
S(4)
S(5)
S(6)
S(7)
S(8)
S(9)
S(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

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

(15) 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(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

(16) Obligation:

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

DT(x, dt(y, z)) → PLUS(x, y)
PLUS(x, dt(y, 0)) → DT(y, x)
PLUS(x, dt(y, 1)) → DT(y, x)
PLUS(x, dt(y, 2)) → DT(y, x)
PLUS(x, dt(y, 3)) → DT(y, x)
PLUS(x, dt(y, 4)) → DT(y, x)
PLUS(x, dt(y, 5)) → DT(y, x)
PLUS(x, dt(y, 6)) → DT(y, x)
PLUS(x, dt(y, 7)) → DT(y, x)
PLUS(x, dt(y, 8)) → DT(y, x)
PLUS(x, dt(y, 9)) → DT(y, x)

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

dt(0, x0)
dt(x0, dt(x1, x2))

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

(17) 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:

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

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

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

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

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

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

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

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

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

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

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

(18) YES

(19) Obligation:

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

MULT(x, dt(y, 1)) → MULT(x, y)
MULT(x, dt(y, 0)) → MULT(x, y)
MULT(x, dt(y, 2)) → MULT(x, y)
MULT(x, dt(y, 3)) → MULT(x, y)
MULT(x, dt(y, 4)) → MULT(x, y)
MULT(x, dt(y, 5)) → MULT(x, y)
MULT(x, dt(y, 6)) → MULT(x, y)
MULT(x, dt(y, 7)) → MULT(x, y)
MULT(x, dt(y, 8)) → MULT(x, y)
MULT(x, dt(y, 9)) → MULT(x, y)

The TRS R consists of the following rules:

dt(0, x) → x
dt(x, dt(y, z)) → dt(plus(x, y), z)
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) → dt(1, 0)
S(dt(x, 0)) → dt(x, 1)
S(dt(x, 1)) → dt(x, 2)
S(dt(x, 2)) → dt(x, 3)
S(dt(x, 3)) → dt(x, 4)
S(dt(x, 4)) → dt(x, 5)
S(dt(x, 5)) → dt(x, 6)
S(dt(x, 6)) → dt(x, 7)
S(dt(x, 7)) → dt(x, 8)
S(dt(x, 8)) → dt(x, 9)
S(dt(x, 9)) → dt(S(x), 0)
plus(x, 0) → x
plus(x, 1) → plus(S(x), 0)
plus(x, 2) → plus(S(x), 1)
plus(x, 3) → plus(S(x), 2)
plus(x, 4) → plus(S(x), 3)
plus(x, 5) → plus(S(x), 4)
plus(x, 6) → plus(S(x), 5)
plus(x, 7) → plus(S(x), 6)
plus(x, 8) → plus(S(x), 7)
plus(x, 9) → plus(S(x), 8)
plus(x, dt(y, 0)) → plus(dt(y, x), 0)
plus(x, dt(y, 1)) → plus(dt(y, x), 1)
plus(x, dt(y, 2)) → plus(dt(y, x), 2)
plus(x, dt(y, 3)) → plus(dt(y, x), 3)
plus(x, dt(y, 4)) → plus(dt(y, x), 4)
plus(x, dt(y, 5)) → plus(dt(y, x), 5)
plus(x, dt(y, 6)) → plus(dt(y, x), 6)
plus(x, dt(y, 7)) → plus(dt(y, x), 7)
plus(x, dt(y, 8)) → plus(dt(y, x), 8)
plus(x, dt(y, 9)) → plus(dt(y, x), 9)
mult(x, 0) → 0
mult(x, 1) → plus(x, mult(x, 0))
mult(x, 2) → plus(x, mult(x, 1))
mult(x, 3) → plus(x, mult(x, 2))
mult(x, 4) → plus(x, mult(x, 3))
mult(x, 5) → plus(x, mult(x, 4))
mult(x, 6) → plus(x, mult(x, 5))
mult(x, 7) → plus(x, mult(x, 6))
mult(x, 8) → plus(x, mult(x, 7))
mult(x, 9) → plus(x, mult(x, 8))
mult(x, dt(y, 0)) → plus(dt(mult(x, y), 0), mult(x, 0))
mult(x, dt(y, 1)) → plus(dt(mult(x, y), 0), mult(x, 1))
mult(x, dt(y, 2)) → plus(dt(mult(x, y), 0), mult(x, 2))
mult(x, dt(y, 3)) → plus(dt(mult(x, y), 0), mult(x, 3))
mult(x, dt(y, 4)) → plus(dt(mult(x, y), 0), mult(x, 4))
mult(x, dt(y, 5)) → plus(dt(mult(x, y), 0), mult(x, 5))
mult(x, dt(y, 6)) → plus(dt(mult(x, y), 0), mult(x, 6))
mult(x, dt(y, 7)) → plus(dt(mult(x, y), 0), mult(x, 7))
mult(x, dt(y, 8)) → plus(dt(mult(x, y), 0), mult(x, 8))
mult(x, dt(y, 9)) → plus(dt(mult(x, y), 0), mult(x, 9))

The set Q consists of the following terms:

dt(0, x0)
dt(x0, dt(x1, x2))
S(0)
S(1)
S(2)
S(3)
S(4)
S(5)
S(6)
S(7)
S(8)
S(9)
S(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

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

(20) 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.

(21) Obligation:

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

MULT(x, dt(y, 1)) → MULT(x, y)
MULT(x, dt(y, 0)) → MULT(x, y)
MULT(x, dt(y, 2)) → MULT(x, y)
MULT(x, dt(y, 3)) → MULT(x, y)
MULT(x, dt(y, 4)) → MULT(x, y)
MULT(x, dt(y, 5)) → MULT(x, y)
MULT(x, dt(y, 6)) → MULT(x, y)
MULT(x, dt(y, 7)) → MULT(x, y)
MULT(x, dt(y, 8)) → MULT(x, y)
MULT(x, dt(y, 9)) → MULT(x, y)

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

dt(0, x0)
dt(x0, dt(x1, x2))
S(0)
S(1)
S(2)
S(3)
S(4)
S(5)
S(6)
S(7)
S(8)
S(9)
S(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

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

(22) 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(dt(x0, 0))
S(dt(x0, 1))
S(dt(x0, 2))
S(dt(x0, 3))
S(dt(x0, 4))
S(dt(x0, 5))
S(dt(x0, 6))
S(dt(x0, 7))
S(dt(x0, 8))
S(dt(x0, 9))
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, dt(x1, 0))
plus(x0, dt(x1, 1))
plus(x0, dt(x1, 2))
plus(x0, dt(x1, 3))
plus(x0, dt(x1, 4))
plus(x0, dt(x1, 5))
plus(x0, dt(x1, 6))
plus(x0, dt(x1, 7))
plus(x0, dt(x1, 8))
plus(x0, dt(x1, 9))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, dt(x1, 0))
mult(x0, dt(x1, 1))
mult(x0, dt(x1, 2))
mult(x0, dt(x1, 3))
mult(x0, dt(x1, 4))
mult(x0, dt(x1, 5))
mult(x0, dt(x1, 6))
mult(x0, dt(x1, 7))
mult(x0, dt(x1, 8))
mult(x0, dt(x1, 9))

(23) Obligation:

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

MULT(x, dt(y, 1)) → MULT(x, y)
MULT(x, dt(y, 0)) → MULT(x, y)
MULT(x, dt(y, 2)) → MULT(x, y)
MULT(x, dt(y, 3)) → MULT(x, y)
MULT(x, dt(y, 4)) → MULT(x, y)
MULT(x, dt(y, 5)) → MULT(x, y)
MULT(x, dt(y, 6)) → MULT(x, y)
MULT(x, dt(y, 7)) → MULT(x, y)
MULT(x, dt(y, 8)) → MULT(x, y)
MULT(x, dt(y, 9)) → MULT(x, y)

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

dt(0, x0)
dt(x0, dt(x1, x2))

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

(24) 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:

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

  • MULT(x, dt(y, 0)) → MULT(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

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

  • MULT(x, dt(y, 3)) → MULT(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • MULT(x, dt(y, 4)) → MULT(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • MULT(x, dt(y, 5)) → MULT(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • MULT(x, dt(y, 6)) → MULT(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • MULT(x, dt(y, 7)) → MULT(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • MULT(x, dt(y, 8)) → MULT(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

  • MULT(x, dt(y, 9)) → MULT(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

(25) YES