0 QTRS
↳1 DependencyPairsProof (⇔, 392 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔, 0 ms)
↳7 QDP
↳8 QReductionProof (⇔, 0 ms)
↳9 QDP
↳10 MRRProof (⇔, 17 ms)
↳11 QDP
↳12 DependencyGraphProof (⇔, 0 ms)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 MRRProof (⇔, 15 ms)
↳20 QDP
↳21 PisEmptyProof (⇔, 0 ms)
↳22 YES
↳23 QDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 QDP
↳26 QReductionProof (⇔, 0 ms)
↳27 QDP
↳28 MRRProof (⇔, 36 ms)
↳29 QDP
↳30 PisEmptyProof (⇔, 0 ms)
↳31 YES
↳32 QDP
↳33 UsableRulesProof (⇔, 0 ms)
↳34 QDP
↳35 QReductionProof (⇔, 0 ms)
↳36 QDP
↳37 MRRProof (⇔, 18 ms)
↳38 QDP
↳39 DependencyGraphProof (⇔, 0 ms)
↳40 TRUE
↳41 QDP
↳42 UsableRulesProof (⇔, 0 ms)
↳43 QDP
↳44 QReductionProof (⇔, 0 ms)
↳45 QDP
↳46 MRRProof (⇔, 6 ms)
↳47 QDP
↳48 DependencyGraphProof (⇔, 0 ms)
↳49 TRUE
↳50 QDP
↳51 UsableRulesProof (⇔, 0 ms)
↳52 QDP
↳53 QReductionProof (⇔, 0 ms)
↳54 QDP
↳55 QDPSizeChangeProof (⇔, 0 ms)
↳56 YES
↳57 QDP
↳58 UsableRulesProof (⇔, 0 ms)
↳59 QDP
↳60 QReductionProof (⇔, 77 ms)
↳61 QDP
↳62 QDPOrderProof (⇔, 75 ms)
↳63 QDP
↳64 QDPOrderProof (⇔, 19 ms)
↳65 QDP
↳66 QDPOrderProof (⇔, 51 ms)
↳67 QDP
↳68 QDPOrderProof (⇔, 15 ms)
↳69 QDP
↳70 QDPOrderProof (⇔, 32 ms)
↳71 QDP
↳72 QDPOrderProof (⇔, 10 ms)
↳73 QDP
↳74 QDPOrderProof (⇔, 19 ms)
↳75 QDP
↳76 QDPOrderProof (⇔, 61 ms)
↳77 QDP
↳78 QDPOrderProof (⇔, 6 ms)
↳79 QDP
↳80 QDPSizeChangeProof (⇔, 0 ms)
↳81 YES
↳82 QDP
↳83 UsableRulesProof (⇔, 0 ms)
↳84 QDP
↳85 QReductionProof (⇔, 0 ms)
↳86 QDP
↳87 QDPSizeChangeProof (⇔, 0 ms)
↳88 YES
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))
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))
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)
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))
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))
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)
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))
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))
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)
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
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))
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))
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)
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
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))
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)
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
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
P(d0(x)) → D9(p(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)
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))
D5(m(x)) → D5(p(x))
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))
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))
D5(m(x)) → D5(p(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)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x
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))
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))
D5(m(x)) → D5(p(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)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x
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))
D5(m(x)) → D5(p(x))
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
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
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)))
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))
D4(m(x)) → D6(p(x))
D6(m(x)) → D4(p(x))
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))
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))
D4(m(x)) → D6(p(x))
D6(m(x)) → D4(p(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)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x
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))
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))
D4(m(x)) → D6(p(x))
D6(m(x)) → D4(p(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)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x
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))
D4(m(x)) → D6(p(x))
D6(m(x)) → D4(p(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)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x
p1 > d91 > 3 > d11 > d71 > 6 > m1 > 5 > 1 > 4 > D61 > 2 > 8 > d21 > d41 > D41 > 0 > d01 > 7 > 9 > d61 > d31 > d81 > d51
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
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))
D3(m(x)) → D7(p(x))
D7(m(x)) → D3(p(x))
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))
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))
D3(m(x)) → D7(p(x))
D7(m(x)) → D3(p(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)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x
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))
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))
D3(m(x)) → D7(p(x))
D7(m(x)) → D3(p(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)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x
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))
D7(m(x)) → D3(p(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
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
D3(m(x)) → D7(p(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)
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))
D2(m(x)) → D8(p(x))
D8(m(x)) → D2(p(x))
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))
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))
D2(m(x)) → D8(p(x))
D8(m(x)) → D2(p(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)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x
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))
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))
D2(m(x)) → D8(p(x))
D8(m(x)) → D2(p(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)))
d1(0) → 1
d1(m(x)) → m(d9(p(x)))
m(0) → 0
m(m(x)) → x
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))
D8(m(x)) → D2(p(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
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
D2(m(x)) → D8(p(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)
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))
S(d9(x)) → S(x)
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))
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))
S(d9(x)) → S(x)
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))
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))
S(d9(x)) → S(x)
d9(0)
d9(m(x0))
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)
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))
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))
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))
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))
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))
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))
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))
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))
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))
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(x, d9(y)) → PLUS(x, d0(y))
trivial
dummyConstant=1
d9_1=1
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, 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))
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(x, d8(y)) → PLUS(x, d0(y))
trivial
dummyConstant=1
d8_1=1
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, 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))
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(x, d7(y)) → PLUS(x, d0(y))
trivial
dummyConstant=1
d7_1=1
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, 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))
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(x, d6(y)) → PLUS(x, d0(y))
trivial
dummyConstant=1
d6_1=1
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, 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))
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(x, d5(y)) → PLUS(x, d0(y))
trivial
dummyConstant=1
d5_1=1
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, 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))
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(x, d4(y)) → PLUS(x, d0(y))
trivial
dummyConstant=1
d4_1=1
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, 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))
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(x, d3(y)) → PLUS(x, d0(y))
trivial
d3_1=1
dummyConstant=1
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, 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))
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(x, d2(y)) → PLUS(x, d0(y))
trivial
dummyConstant=1
d2_1=1
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, 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))
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(x, d1(y)) → PLUS(x, d0(y))
trivial
dummyConstant=1
d1_1=1
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, 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))
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))
From the DPs we obtained the following set of size-change graphs:
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)
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))
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))
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)
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))
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))
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)
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))
From the DPs we obtained the following set of size-change graphs: