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
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))
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))
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)
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))
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))
S1(dt(x, 9)) → S1(x)
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))
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))
S1(dt(x, 9)) → S1(x)
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))
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))
S1(dt(x, 9)) → S1(x)
dt(0, x0)
dt(x0, dt(x1, x2))
From the DPs we obtained the following set of size-change graphs:
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)
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))
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))
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)
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))
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))
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)
dt(0, x0)
dt(x0, dt(x1, x2))
From the DPs we obtained the following set of size-change graphs:
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)
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))
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))
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)
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))
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))
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)
dt(0, x0)
dt(x0, dt(x1, x2))
From the DPs we obtained the following set of size-change graphs: