(0) Obligation:

da_0(0) → 0
da_1(0) → 1
da_2(0) → 2
da_3(0) → 3
da_4(0) → 4
da_5(0) → 5
da_6(0) → 6
da_7(0) → 7
da_8(0) → 8
da_9(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) → da_0(1)
S(da_0(x)) → da_1(x)
S(da_1(x)) → da_2(x)
S(da_2(x)) → da_3(x)
S(da_3(x)) → da_4(x)
S(da_4(x)) → da_5(x)
S(da_5(x)) → da_6(x)
S(da_6(x)) → da_7(x)
S(da_7(x)) → da_8(x)
S(da_8(x)) → da_9(x)
S(da_9(x)) → da_0(S(x))
plus(x, 0) → x
plus(0, x) → 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(1, x) → S(x)
plus(2, x) → S(S(x))
plus(3, x) → S(S(S(x)))
plus(4, x) → S(S(S(S(x))))
plus(5, x) → S(S(S(S(S(x)))))
plus(6, x) → S(S(S(S(S(S(x))))))
plus(7, x) → S(S(S(S(S(S(S(x)))))))
plus(8, x) → S(S(S(S(S(S(S(S(x))))))))
plus(9, x) → S(S(S(S(S(S(S(S(S(x)))))))))
plus(da_0(x), da_0(y)) → plus(da_0(plus(x, y)), 0)
plus(da_1(x), da_0(y)) → plus(da_1(plus(x, y)), 0)
plus(da_2(x), da_0(y)) → plus(da_2(plus(x, y)), 0)
plus(da_3(x), da_0(y)) → plus(da_3(plus(x, y)), 0)
plus(da_4(x), da_0(y)) → plus(da_4(plus(x, y)), 0)
plus(da_5(x), da_0(y)) → plus(da_5(plus(x, y)), 0)
plus(da_6(x), da_0(y)) → plus(da_6(plus(x, y)), 0)
plus(da_7(x), da_0(y)) → plus(da_7(plus(x, y)), 0)
plus(da_8(x), da_0(y)) → plus(da_8(plus(x, y)), 0)
plus(da_9(x), da_0(y)) → plus(da_9(plus(x, y)), 0)
plus(da_0(x), da_1(y)) → plus(da_0(plus(x, y)), 1)
plus(da_1(x), da_1(y)) → plus(da_1(plus(x, y)), 1)
plus(da_2(x), da_1(y)) → plus(da_2(plus(x, y)), 1)
plus(da_3(x), da_1(y)) → plus(da_3(plus(x, y)), 1)
plus(da_4(x), da_1(y)) → plus(da_4(plus(x, y)), 1)
plus(da_5(x), da_1(y)) → plus(da_5(plus(x, y)), 1)
plus(da_6(x), da_1(y)) → plus(da_6(plus(x, y)), 1)
plus(da_7(x), da_1(y)) → plus(da_7(plus(x, y)), 1)
plus(da_8(x), da_1(y)) → plus(da_8(plus(x, y)), 1)
plus(da_9(x), da_1(y)) → plus(da_9(plus(x, y)), 1)
plus(da_0(x), da_2(y)) → plus(da_0(plus(x, y)), 2)
plus(da_1(x), da_2(y)) → plus(da_1(plus(x, y)), 2)
plus(da_2(x), da_2(y)) → plus(da_2(plus(x, y)), 2)
plus(da_3(x), da_2(y)) → plus(da_3(plus(x, y)), 2)
plus(da_4(x), da_2(y)) → plus(da_4(plus(x, y)), 2)
plus(da_5(x), da_2(y)) → plus(da_5(plus(x, y)), 2)
plus(da_6(x), da_2(y)) → plus(da_6(plus(x, y)), 2)
plus(da_7(x), da_2(y)) → plus(da_7(plus(x, y)), 2)
plus(da_8(x), da_2(y)) → plus(da_8(plus(x, y)), 2)
plus(da_9(x), da_2(y)) → plus(da_9(plus(x, y)), 2)
plus(da_0(x), da_3(y)) → plus(da_0(plus(x, y)), 3)
plus(da_1(x), da_3(y)) → plus(da_1(plus(x, y)), 3)
plus(da_2(x), da_3(y)) → plus(da_2(plus(x, y)), 3)
plus(da_3(x), da_3(y)) → plus(da_3(plus(x, y)), 3)
plus(da_4(x), da_3(y)) → plus(da_4(plus(x, y)), 3)
plus(da_5(x), da_3(y)) → plus(da_5(plus(x, y)), 3)
plus(da_6(x), da_3(y)) → plus(da_6(plus(x, y)), 3)
plus(da_7(x), da_3(y)) → plus(da_7(plus(x, y)), 3)
plus(da_8(x), da_3(y)) → plus(da_8(plus(x, y)), 3)
plus(da_9(x), da_3(y)) → plus(da_9(plus(x, y)), 3)
plus(da_0(x), da_4(y)) → plus(da_0(plus(x, y)), 4)
plus(da_1(x), da_4(y)) → plus(da_1(plus(x, y)), 4)
plus(da_2(x), da_4(y)) → plus(da_2(plus(x, y)), 4)
plus(da_3(x), da_4(y)) → plus(da_3(plus(x, y)), 4)
plus(da_4(x), da_4(y)) → plus(da_4(plus(x, y)), 4)
plus(da_5(x), da_4(y)) → plus(da_5(plus(x, y)), 4)
plus(da_6(x), da_4(y)) → plus(da_6(plus(x, y)), 4)
plus(da_7(x), da_4(y)) → plus(da_7(plus(x, y)), 4)
plus(da_8(x), da_4(y)) → plus(da_8(plus(x, y)), 4)
plus(da_9(x), da_4(y)) → plus(da_9(plus(x, y)), 4)
plus(da_0(x), da_5(y)) → plus(da_0(plus(x, y)), 5)
plus(da_1(x), da_5(y)) → plus(da_1(plus(x, y)), 5)
plus(da_2(x), da_5(y)) → plus(da_2(plus(x, y)), 5)
plus(da_3(x), da_5(y)) → plus(da_3(plus(x, y)), 5)
plus(da_4(x), da_5(y)) → plus(da_4(plus(x, y)), 5)
plus(da_5(x), da_5(y)) → plus(da_5(plus(x, y)), 5)
plus(da_6(x), da_5(y)) → plus(da_6(plus(x, y)), 5)
plus(da_7(x), da_5(y)) → plus(da_7(plus(x, y)), 5)
plus(da_8(x), da_5(y)) → plus(da_8(plus(x, y)), 5)
plus(da_9(x), da_5(y)) → plus(da_9(plus(x, y)), 5)
plus(da_0(x), da_6(y)) → plus(da_0(plus(x, y)), 6)
plus(da_1(x), da_6(y)) → plus(da_1(plus(x, y)), 6)
plus(da_2(x), da_6(y)) → plus(da_2(plus(x, y)), 6)
plus(da_3(x), da_6(y)) → plus(da_3(plus(x, y)), 6)
plus(da_4(x), da_6(y)) → plus(da_4(plus(x, y)), 6)
plus(da_5(x), da_6(y)) → plus(da_5(plus(x, y)), 6)
plus(da_6(x), da_6(y)) → plus(da_6(plus(x, y)), 6)
plus(da_7(x), da_6(y)) → plus(da_7(plus(x, y)), 6)
plus(da_8(x), da_6(y)) → plus(da_8(plus(x, y)), 6)
plus(da_9(x), da_6(y)) → plus(da_9(plus(x, y)), 6)
plus(da_0(x), da_7(y)) → plus(da_0(plus(x, y)), 7)
plus(da_1(x), da_7(y)) → plus(da_1(plus(x, y)), 7)
plus(da_2(x), da_7(y)) → plus(da_2(plus(x, y)), 7)
plus(da_3(x), da_7(y)) → plus(da_3(plus(x, y)), 7)
plus(da_4(x), da_7(y)) → plus(da_4(plus(x, y)), 7)
plus(da_5(x), da_7(y)) → plus(da_5(plus(x, y)), 7)
plus(da_6(x), da_7(y)) → plus(da_6(plus(x, y)), 7)
plus(da_7(x), da_7(y)) → plus(da_7(plus(x, y)), 7)
plus(da_8(x), da_7(y)) → plus(da_8(plus(x, y)), 7)
plus(da_9(x), da_7(y)) → plus(da_9(plus(x, y)), 7)
plus(da_0(x), da_8(y)) → plus(da_0(plus(x, y)), 8)
plus(da_1(x), da_8(y)) → plus(da_1(plus(x, y)), 8)
plus(da_2(x), da_8(y)) → plus(da_2(plus(x, y)), 8)
plus(da_3(x), da_8(y)) → plus(da_3(plus(x, y)), 8)
plus(da_4(x), da_8(y)) → plus(da_4(plus(x, y)), 8)
plus(da_5(x), da_8(y)) → plus(da_5(plus(x, y)), 8)
plus(da_6(x), da_8(y)) → plus(da_6(plus(x, y)), 8)
plus(da_7(x), da_8(y)) → plus(da_7(plus(x, y)), 8)
plus(da_8(x), da_8(y)) → plus(da_8(plus(x, y)), 8)
plus(da_9(x), da_8(y)) → plus(da_9(plus(x, y)), 8)
plus(da_0(x), da_9(y)) → plus(da_0(plus(x, y)), 9)
plus(da_1(x), da_9(y)) → plus(da_1(plus(x, y)), 9)
plus(da_2(x), da_9(y)) → plus(da_2(plus(x, y)), 9)
plus(da_3(x), da_9(y)) → plus(da_3(plus(x, y)), 9)
plus(da_4(x), da_9(y)) → plus(da_4(plus(x, y)), 9)
plus(da_5(x), da_9(y)) → plus(da_5(plus(x, y)), 9)
plus(da_6(x), da_9(y)) → plus(da_6(plus(x, y)), 9)
plus(da_7(x), da_9(y)) → plus(da_7(plus(x, y)), 9)
plus(da_8(x), da_9(y)) → plus(da_8(plus(x, y)), 9)
plus(da_9(x), da_9(y)) → plus(da_9(plus(x, y)), 9)
mult(x, 0) → 0
mult(x, 1) → plus(mult(x, 0), x)
mult(x, 2) → plus(mult(x, 1), x)
mult(x, 3) → plus(mult(x, 2), x)
mult(x, 4) → plus(mult(x, 3), x)
mult(x, 5) → plus(mult(x, 4), x)
mult(x, 6) → plus(mult(x, 5), x)
mult(x, 7) → plus(mult(x, 6), x)
mult(x, 8) → plus(mult(x, 7), x)
mult(x, 9) → plus(mult(x, 8), x)
mult(x, da_0(y)) → plus(da_0(mult(x, y)), mult(x, 0))
mult(x, da_1(y)) → plus(da_0(mult(x, y)), mult(x, 1))
mult(x, da_2(y)) → plus(da_0(mult(x, y)), mult(x, 2))
mult(x, da_3(y)) → plus(da_0(mult(x, y)), mult(x, 3))
mult(x, da_4(y)) → plus(da_0(mult(x, y)), mult(x, 4))
mult(x, da_5(y)) → plus(da_0(mult(x, y)), mult(x, 5))
mult(x, da_6(y)) → plus(da_0(mult(x, y)), mult(x, 6))
mult(x, da_7(y)) → plus(da_0(mult(x, y)), mult(x, 7))
mult(x, da_8(y)) → plus(da_0(mult(x, y)), mult(x, 8))
mult(x, da_9(y)) → plus(da_0(mult(x, y)), mult(x, 9))
neg(0) → 0
neg(neg(x)) → x
P(0) → neg(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(da_0(x)) → da_9(P(x))
P(da_1(x)) → da_0(x)
P(da_2(x)) → da_1(x)
P(da_3(x)) → da_2(x)
P(da_4(x)) → da_3(x)
P(da_5(x)) → da_4(x)
P(da_6(x)) → da_5(x)
P(da_7(x)) → da_6(x)
P(da_8(x)) → da_7(x)
P(da_9(x)) → da_8(x)
P(neg(x)) → neg(S(x))
S(neg(1)) → neg(0)
S(neg(2)) → neg(1)
S(neg(3)) → neg(2)
S(neg(4)) → neg(3)
S(neg(5)) → neg(4)
S(neg(6)) → neg(5)
S(neg(7)) → neg(6)
S(neg(8)) → neg(7)
S(neg(9)) → neg(8)
S(neg(da_0(x))) → neg(da_9(P(x)))
S(neg(da_1(x))) → neg(da_0(x))
S(neg(da_2(x))) → neg(da_1(x))
S(neg(da_3(x))) → neg(da_2(x))
S(neg(da_4(x))) → neg(da_3(x))
S(neg(da_5(x))) → neg(da_4(x))
S(neg(da_6(x))) → neg(da_5(x))
S(neg(da_7(x))) → neg(da_6(x))
S(neg(da_8(x))) → neg(da_7(x))
S(neg(da_9(x))) → neg(da_8(x))
da_0(neg(x)) → neg(da_0(x))
da_1(neg(x)) → neg(da_9(P(x)))
da_2(neg(x)) → neg(da_8(P(x)))
da_3(neg(x)) → neg(da_7(P(x)))
da_4(neg(x)) → neg(da_6(P(x)))
da_5(neg(x)) → neg(da_5(P(x)))
da_6(neg(x)) → neg(da_4(P(x)))
da_7(neg(x)) → neg(da_3(P(x)))
da_8(neg(x)) → neg(da_2(P(x)))
da_9(neg(x)) → neg(da_1(P(x)))
plus(x, neg(1)) → P(x)
plus(x, neg(2)) → P(P(x))
plus(x, neg(3)) → P(P(P(x)))
plus(x, neg(4)) → P(P(P(P(x))))
plus(x, neg(5)) → P(P(P(P(P(x)))))
plus(x, neg(6)) → P(P(P(P(P(P(x))))))
plus(x, neg(7)) → P(P(P(P(P(P(P(x)))))))
plus(x, neg(8)) → P(P(P(P(P(P(P(P(x))))))))
plus(x, neg(9)) → P(P(P(P(P(P(P(P(P(x)))))))))
plus(neg(1), x) → P(x)
plus(neg(2), x) → P(P(x))
plus(neg(3), x) → P(P(P(x)))
plus(neg(4), x) → P(P(P(P(x))))
plus(neg(5), x) → P(P(P(P(P(x)))))
plus(neg(6), x) → P(P(P(P(P(P(x))))))
plus(neg(7), x) → P(P(P(P(P(P(P(x)))))))
plus(neg(8), x) → P(P(P(P(P(P(P(P(x))))))))
plus(neg(9), x) → P(P(P(P(P(P(P(P(P(x)))))))))
plus(da_0(x), neg(da_0(y))) → plus(da_0(plus(x, neg(y))), neg(0))
plus(da_1(x), neg(da_0(y))) → plus(da_1(plus(x, neg(y))), neg(0))
plus(da_2(x), neg(da_0(y))) → plus(da_2(plus(x, neg(y))), neg(0))
plus(da_3(x), neg(da_0(y))) → plus(da_3(plus(x, neg(y))), neg(0))
plus(da_4(x), neg(da_0(y))) → plus(da_4(plus(x, neg(y))), neg(0))
plus(da_5(x), neg(da_0(y))) → plus(da_5(plus(x, neg(y))), neg(0))
plus(da_6(x), neg(da_0(y))) → plus(da_6(plus(x, neg(y))), neg(0))
plus(da_7(x), neg(da_0(y))) → plus(da_7(plus(x, neg(y))), neg(0))
plus(da_8(x), neg(da_0(y))) → plus(da_8(plus(x, neg(y))), neg(0))
plus(da_9(x), neg(da_0(y))) → plus(da_9(plus(x, neg(y))), neg(0))
plus(da_0(x), neg(da_1(y))) → plus(da_0(plus(x, neg(y))), neg(1))
plus(da_1(x), neg(da_1(y))) → plus(da_1(plus(x, neg(y))), neg(1))
plus(da_2(x), neg(da_1(y))) → plus(da_2(plus(x, neg(y))), neg(1))
plus(da_3(x), neg(da_1(y))) → plus(da_3(plus(x, neg(y))), neg(1))
plus(da_4(x), neg(da_1(y))) → plus(da_4(plus(x, neg(y))), neg(1))
plus(da_5(x), neg(da_1(y))) → plus(da_5(plus(x, neg(y))), neg(1))
plus(da_6(x), neg(da_1(y))) → plus(da_6(plus(x, neg(y))), neg(1))
plus(da_7(x), neg(da_1(y))) → plus(da_7(plus(x, neg(y))), neg(1))
plus(da_8(x), neg(da_1(y))) → plus(da_8(plus(x, neg(y))), neg(1))
plus(da_9(x), neg(da_1(y))) → plus(da_9(plus(x, neg(y))), neg(1))
plus(da_0(x), neg(da_2(y))) → plus(da_0(plus(x, neg(y))), neg(2))
plus(da_1(x), neg(da_2(y))) → plus(da_1(plus(x, neg(y))), neg(2))
plus(da_2(x), neg(da_2(y))) → plus(da_2(plus(x, neg(y))), neg(2))
plus(da_3(x), neg(da_2(y))) → plus(da_3(plus(x, neg(y))), neg(2))
plus(da_4(x), neg(da_2(y))) → plus(da_4(plus(x, neg(y))), neg(2))
plus(da_5(x), neg(da_2(y))) → plus(da_5(plus(x, neg(y))), neg(2))
plus(da_6(x), neg(da_2(y))) → plus(da_6(plus(x, neg(y))), neg(2))
plus(da_7(x), neg(da_2(y))) → plus(da_7(plus(x, neg(y))), neg(2))
plus(da_8(x), neg(da_2(y))) → plus(da_8(plus(x, neg(y))), neg(2))
plus(da_9(x), neg(da_2(y))) → plus(da_9(plus(x, neg(y))), neg(2))
plus(da_0(x), neg(da_3(y))) → plus(da_0(plus(x, neg(y))), neg(3))
plus(da_1(x), neg(da_3(y))) → plus(da_1(plus(x, neg(y))), neg(3))
plus(da_2(x), neg(da_3(y))) → plus(da_2(plus(x, neg(y))), neg(3))
plus(da_3(x), neg(da_3(y))) → plus(da_3(plus(x, neg(y))), neg(3))
plus(da_4(x), neg(da_3(y))) → plus(da_4(plus(x, neg(y))), neg(3))
plus(da_5(x), neg(da_3(y))) → plus(da_5(plus(x, neg(y))), neg(3))
plus(da_6(x), neg(da_3(y))) → plus(da_6(plus(x, neg(y))), neg(3))
plus(da_7(x), neg(da_3(y))) → plus(da_7(plus(x, neg(y))), neg(3))
plus(da_8(x), neg(da_3(y))) → plus(da_8(plus(x, neg(y))), neg(3))
plus(da_9(x), neg(da_3(y))) → plus(da_9(plus(x, neg(y))), neg(3))
plus(da_0(x), neg(da_4(y))) → plus(da_0(plus(x, neg(y))), neg(4))
plus(da_1(x), neg(da_4(y))) → plus(da_1(plus(x, neg(y))), neg(4))
plus(da_2(x), neg(da_4(y))) → plus(da_2(plus(x, neg(y))), neg(4))
plus(da_3(x), neg(da_4(y))) → plus(da_3(plus(x, neg(y))), neg(4))
plus(da_4(x), neg(da_4(y))) → plus(da_4(plus(x, neg(y))), neg(4))
plus(da_5(x), neg(da_4(y))) → plus(da_5(plus(x, neg(y))), neg(4))
plus(da_6(x), neg(da_4(y))) → plus(da_6(plus(x, neg(y))), neg(4))
plus(da_7(x), neg(da_4(y))) → plus(da_7(plus(x, neg(y))), neg(4))
plus(da_8(x), neg(da_4(y))) → plus(da_8(plus(x, neg(y))), neg(4))
plus(da_9(x), neg(da_4(y))) → plus(da_9(plus(x, neg(y))), neg(4))
plus(da_0(x), neg(da_5(y))) → plus(da_0(plus(x, neg(y))), neg(5))
plus(da_1(x), neg(da_5(y))) → plus(da_1(plus(x, neg(y))), neg(5))
plus(da_2(x), neg(da_5(y))) → plus(da_2(plus(x, neg(y))), neg(5))
plus(da_3(x), neg(da_5(y))) → plus(da_3(plus(x, neg(y))), neg(5))
plus(da_4(x), neg(da_5(y))) → plus(da_4(plus(x, neg(y))), neg(5))
plus(da_5(x), neg(da_5(y))) → plus(da_5(plus(x, neg(y))), neg(5))
plus(da_6(x), neg(da_5(y))) → plus(da_6(plus(x, neg(y))), neg(5))
plus(da_7(x), neg(da_5(y))) → plus(da_7(plus(x, neg(y))), neg(5))
plus(da_8(x), neg(da_5(y))) → plus(da_8(plus(x, neg(y))), neg(5))
plus(da_9(x), neg(da_5(y))) → plus(da_9(plus(x, neg(y))), neg(5))
plus(da_0(x), neg(da_6(y))) → plus(da_0(plus(x, neg(y))), neg(6))
plus(da_1(x), neg(da_6(y))) → plus(da_1(plus(x, neg(y))), neg(6))
plus(da_2(x), neg(da_6(y))) → plus(da_2(plus(x, neg(y))), neg(6))
plus(da_3(x), neg(da_6(y))) → plus(da_3(plus(x, neg(y))), neg(6))
plus(da_4(x), neg(da_6(y))) → plus(da_4(plus(x, neg(y))), neg(6))
plus(da_5(x), neg(da_6(y))) → plus(da_5(plus(x, neg(y))), neg(6))
plus(da_6(x), neg(da_6(y))) → plus(da_6(plus(x, neg(y))), neg(6))
plus(da_7(x), neg(da_6(y))) → plus(da_7(plus(x, neg(y))), neg(6))
plus(da_8(x), neg(da_6(y))) → plus(da_8(plus(x, neg(y))), neg(6))
plus(da_9(x), neg(da_6(y))) → plus(da_9(plus(x, neg(y))), neg(6))
plus(da_0(x), neg(da_7(y))) → plus(da_0(plus(x, neg(y))), neg(7))
plus(da_1(x), neg(da_7(y))) → plus(da_1(plus(x, neg(y))), neg(7))
plus(da_2(x), neg(da_7(y))) → plus(da_2(plus(x, neg(y))), neg(7))
plus(da_3(x), neg(da_7(y))) → plus(da_3(plus(x, neg(y))), neg(7))
plus(da_4(x), neg(da_7(y))) → plus(da_4(plus(x, neg(y))), neg(7))
plus(da_5(x), neg(da_7(y))) → plus(da_5(plus(x, neg(y))), neg(7))
plus(da_6(x), neg(da_7(y))) → plus(da_6(plus(x, neg(y))), neg(7))
plus(da_7(x), neg(da_7(y))) → plus(da_7(plus(x, neg(y))), neg(7))
plus(da_8(x), neg(da_7(y))) → plus(da_8(plus(x, neg(y))), neg(7))
plus(da_9(x), neg(da_7(y))) → plus(da_9(plus(x, neg(y))), neg(7))
plus(da_0(x), neg(da_8(y))) → plus(da_0(plus(x, neg(y))), neg(8))
plus(da_1(x), neg(da_8(y))) → plus(da_1(plus(x, neg(y))), neg(8))
plus(da_2(x), neg(da_8(y))) → plus(da_2(plus(x, neg(y))), neg(8))
plus(da_3(x), neg(da_8(y))) → plus(da_3(plus(x, neg(y))), neg(8))
plus(da_4(x), neg(da_8(y))) → plus(da_4(plus(x, neg(y))), neg(8))
plus(da_5(x), neg(da_8(y))) → plus(da_5(plus(x, neg(y))), neg(8))
plus(da_6(x), neg(da_8(y))) → plus(da_6(plus(x, neg(y))), neg(8))
plus(da_7(x), neg(da_8(y))) → plus(da_7(plus(x, neg(y))), neg(8))
plus(da_8(x), neg(da_8(y))) → plus(da_8(plus(x, neg(y))), neg(8))
plus(da_9(x), neg(da_8(y))) → plus(da_9(plus(x, neg(y))), neg(8))
plus(da_0(x), neg(da_9(y))) → plus(da_0(plus(x, neg(y))), neg(9))
plus(da_1(x), neg(da_9(y))) → plus(da_1(plus(x, neg(y))), neg(9))
plus(da_2(x), neg(da_9(y))) → plus(da_2(plus(x, neg(y))), neg(9))
plus(da_3(x), neg(da_9(y))) → plus(da_3(plus(x, neg(y))), neg(9))
plus(da_4(x), neg(da_9(y))) → plus(da_4(plus(x, neg(y))), neg(9))
plus(da_5(x), neg(da_9(y))) → plus(da_5(plus(x, neg(y))), neg(9))
plus(da_6(x), neg(da_9(y))) → plus(da_6(plus(x, neg(y))), neg(9))
plus(da_7(x), neg(da_9(y))) → plus(da_7(plus(x, neg(y))), neg(9))
plus(da_8(x), neg(da_9(y))) → plus(da_8(plus(x, neg(y))), neg(9))
plus(da_9(x), neg(da_9(y))) → plus(da_9(plus(x, neg(y))), neg(9))
plus(neg(da_0(y)), da_0(x)) → plus(da_0(plus(x, neg(y))), neg(0))
plus(neg(da_0(y)), da_1(x)) → plus(da_1(plus(x, neg(y))), neg(0))
plus(neg(da_0(y)), da_2(x)) → plus(da_2(plus(x, neg(y))), neg(0))
plus(neg(da_0(y)), da_3(x)) → plus(da_3(plus(x, neg(y))), neg(0))
plus(neg(da_0(y)), da_4(x)) → plus(da_4(plus(x, neg(y))), neg(0))
plus(neg(da_0(y)), da_5(x)) → plus(da_5(plus(x, neg(y))), neg(0))
plus(neg(da_0(y)), da_6(x)) → plus(da_6(plus(x, neg(y))), neg(0))
plus(neg(da_0(y)), da_7(x)) → plus(da_7(plus(x, neg(y))), neg(0))
plus(neg(da_0(y)), da_8(x)) → plus(da_8(plus(x, neg(y))), neg(0))
plus(neg(da_0(y)), da_9(x)) → plus(da_9(plus(x, neg(y))), neg(0))
plus(neg(da_1(y)), da_0(x)) → plus(da_0(plus(x, neg(y))), neg(1))
plus(neg(da_1(y)), da_1(x)) → plus(da_1(plus(x, neg(y))), neg(1))
plus(neg(da_1(y)), da_2(x)) → plus(da_2(plus(x, neg(y))), neg(1))
plus(neg(da_1(y)), da_3(x)) → plus(da_3(plus(x, neg(y))), neg(1))
plus(neg(da_1(y)), da_4(x)) → plus(da_4(plus(x, neg(y))), neg(1))
plus(neg(da_1(y)), da_5(x)) → plus(da_5(plus(x, neg(y))), neg(1))
plus(neg(da_1(y)), da_6(x)) → plus(da_6(plus(x, neg(y))), neg(1))
plus(neg(da_1(y)), da_7(x)) → plus(da_7(plus(x, neg(y))), neg(1))
plus(neg(da_1(y)), da_8(x)) → plus(da_8(plus(x, neg(y))), neg(1))
plus(neg(da_1(y)), da_9(x)) → plus(da_9(plus(x, neg(y))), neg(1))
plus(neg(da_2(y)), da_0(x)) → plus(da_0(plus(x, neg(y))), neg(2))
plus(neg(da_2(y)), da_1(x)) → plus(da_1(plus(x, neg(y))), neg(2))
plus(neg(da_2(y)), da_2(x)) → plus(da_2(plus(x, neg(y))), neg(2))
plus(neg(da_2(y)), da_3(x)) → plus(da_3(plus(x, neg(y))), neg(2))
plus(neg(da_2(y)), da_4(x)) → plus(da_4(plus(x, neg(y))), neg(2))
plus(neg(da_2(y)), da_5(x)) → plus(da_5(plus(x, neg(y))), neg(2))
plus(neg(da_2(y)), da_6(x)) → plus(da_6(plus(x, neg(y))), neg(2))
plus(neg(da_2(y)), da_7(x)) → plus(da_7(plus(x, neg(y))), neg(2))
plus(neg(da_2(y)), da_8(x)) → plus(da_8(plus(x, neg(y))), neg(2))
plus(neg(da_2(y)), da_9(x)) → plus(da_9(plus(x, neg(y))), neg(2))
plus(neg(da_3(y)), da_0(x)) → plus(da_0(plus(x, neg(y))), neg(3))
plus(neg(da_3(y)), da_1(x)) → plus(da_1(plus(x, neg(y))), neg(3))
plus(neg(da_3(y)), da_2(x)) → plus(da_2(plus(x, neg(y))), neg(3))
plus(neg(da_3(y)), da_3(x)) → plus(da_3(plus(x, neg(y))), neg(3))
plus(neg(da_3(y)), da_4(x)) → plus(da_4(plus(x, neg(y))), neg(3))
plus(neg(da_3(y)), da_5(x)) → plus(da_5(plus(x, neg(y))), neg(3))
plus(neg(da_3(y)), da_6(x)) → plus(da_6(plus(x, neg(y))), neg(3))
plus(neg(da_3(y)), da_7(x)) → plus(da_7(plus(x, neg(y))), neg(3))
plus(neg(da_3(y)), da_8(x)) → plus(da_8(plus(x, neg(y))), neg(3))
plus(neg(da_3(y)), da_9(x)) → plus(da_9(plus(x, neg(y))), neg(3))
plus(neg(da_4(y)), da_0(x)) → plus(da_0(plus(x, neg(y))), neg(4))
plus(neg(da_4(y)), da_1(x)) → plus(da_1(plus(x, neg(y))), neg(4))
plus(neg(da_4(y)), da_2(x)) → plus(da_2(plus(x, neg(y))), neg(4))
plus(neg(da_4(y)), da_3(x)) → plus(da_3(plus(x, neg(y))), neg(4))
plus(neg(da_4(y)), da_4(x)) → plus(da_4(plus(x, neg(y))), neg(4))
plus(neg(da_4(y)), da_5(x)) → plus(da_5(plus(x, neg(y))), neg(4))
plus(neg(da_4(y)), da_6(x)) → plus(da_6(plus(x, neg(y))), neg(4))
plus(neg(da_4(y)), da_7(x)) → plus(da_7(plus(x, neg(y))), neg(4))
plus(neg(da_4(y)), da_8(x)) → plus(da_8(plus(x, neg(y))), neg(4))
plus(neg(da_4(y)), da_9(x)) → plus(da_9(plus(x, neg(y))), neg(4))
plus(neg(da_5(y)), da_0(x)) → plus(da_0(plus(x, neg(y))), neg(5))
plus(neg(da_5(y)), da_1(x)) → plus(da_1(plus(x, neg(y))), neg(5))
plus(neg(da_5(y)), da_2(x)) → plus(da_2(plus(x, neg(y))), neg(5))
plus(neg(da_5(y)), da_3(x)) → plus(da_3(plus(x, neg(y))), neg(5))
plus(neg(da_5(y)), da_4(x)) → plus(da_4(plus(x, neg(y))), neg(5))
plus(neg(da_5(y)), da_5(x)) → plus(da_5(plus(x, neg(y))), neg(5))
plus(neg(da_5(y)), da_6(x)) → plus(da_6(plus(x, neg(y))), neg(5))
plus(neg(da_5(y)), da_7(x)) → plus(da_7(plus(x, neg(y))), neg(5))
plus(neg(da_5(y)), da_8(x)) → plus(da_8(plus(x, neg(y))), neg(5))
plus(neg(da_5(y)), da_9(x)) → plus(da_9(plus(x, neg(y))), neg(5))
plus(neg(da_6(y)), da_0(x)) → plus(da_0(plus(x, neg(y))), neg(6))
plus(neg(da_6(y)), da_1(x)) → plus(da_1(plus(x, neg(y))), neg(6))
plus(neg(da_6(y)), da_2(x)) → plus(da_2(plus(x, neg(y))), neg(6))
plus(neg(da_6(y)), da_3(x)) → plus(da_3(plus(x, neg(y))), neg(6))
plus(neg(da_6(y)), da_4(x)) → plus(da_4(plus(x, neg(y))), neg(6))
plus(neg(da_6(y)), da_5(x)) → plus(da_5(plus(x, neg(y))), neg(6))
plus(neg(da_6(y)), da_6(x)) → plus(da_6(plus(x, neg(y))), neg(6))
plus(neg(da_6(y)), da_7(x)) → plus(da_7(plus(x, neg(y))), neg(6))
plus(neg(da_6(y)), da_8(x)) → plus(da_8(plus(x, neg(y))), neg(6))
plus(neg(da_6(y)), da_9(x)) → plus(da_9(plus(x, neg(y))), neg(6))
plus(neg(da_7(y)), da_0(x)) → plus(da_0(plus(x, neg(y))), neg(7))
plus(neg(da_7(y)), da_1(x)) → plus(da_1(plus(x, neg(y))), neg(7))
plus(neg(da_7(y)), da_2(x)) → plus(da_2(plus(x, neg(y))), neg(7))
plus(neg(da_7(y)), da_3(x)) → plus(da_3(plus(x, neg(y))), neg(7))
plus(neg(da_7(y)), da_4(x)) → plus(da_4(plus(x, neg(y))), neg(7))
plus(neg(da_7(y)), da_5(x)) → plus(da_5(plus(x, neg(y))), neg(7))
plus(neg(da_7(y)), da_6(x)) → plus(da_6(plus(x, neg(y))), neg(7))
plus(neg(da_7(y)), da_7(x)) → plus(da_7(plus(x, neg(y))), neg(7))
plus(neg(da_7(y)), da_8(x)) → plus(da_8(plus(x, neg(y))), neg(7))
plus(neg(da_7(y)), da_9(x)) → plus(da_9(plus(x, neg(y))), neg(7))
plus(neg(da_8(y)), da_0(x)) → plus(da_0(plus(x, neg(y))), neg(8))
plus(neg(da_8(y)), da_1(x)) → plus(da_1(plus(x, neg(y))), neg(8))
plus(neg(da_8(y)), da_2(x)) → plus(da_2(plus(x, neg(y))), neg(8))
plus(neg(da_8(y)), da_3(x)) → plus(da_3(plus(x, neg(y))), neg(8))
plus(neg(da_8(y)), da_4(x)) → plus(da_4(plus(x, neg(y))), neg(8))
plus(neg(da_8(y)), da_5(x)) → plus(da_5(plus(x, neg(y))), neg(8))
plus(neg(da_8(y)), da_6(x)) → plus(da_6(plus(x, neg(y))), neg(8))
plus(neg(da_8(y)), da_7(x)) → plus(da_7(plus(x, neg(y))), neg(8))
plus(neg(da_8(y)), da_8(x)) → plus(da_8(plus(x, neg(y))), neg(8))
plus(neg(da_8(y)), da_9(x)) → plus(da_9(plus(x, neg(y))), neg(8))
plus(neg(da_9(y)), da_0(x)) → plus(da_0(plus(x, neg(y))), neg(9))
plus(neg(da_9(y)), da_1(x)) → plus(da_1(plus(x, neg(y))), neg(9))
plus(neg(da_9(y)), da_2(x)) → plus(da_2(plus(x, neg(y))), neg(9))
plus(neg(da_9(y)), da_3(x)) → plus(da_3(plus(x, neg(y))), neg(9))
plus(neg(da_9(y)), da_4(x)) → plus(da_4(plus(x, neg(y))), neg(9))
plus(neg(da_9(y)), da_5(x)) → plus(da_5(plus(x, neg(y))), neg(9))
plus(neg(da_9(y)), da_6(x)) → plus(da_6(plus(x, neg(y))), neg(9))
plus(neg(da_9(y)), da_7(x)) → plus(da_7(plus(x, neg(y))), neg(9))
plus(neg(da_9(y)), da_8(x)) → plus(da_8(plus(x, neg(y))), neg(9))
plus(neg(da_9(y)), da_9(x)) → plus(da_9(plus(x, neg(y))), neg(9))
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, neg(y)) → neg(mult(x, y))

da_0(0)
da_1(0)
da_2(0)
da_3(0)
da_4(0)
da_5(0)
da_6(0)
da_7(0)
da_8(0)
da_9(0)
S(0)
S(1)
S(2)
S(3)
S(4)
S(5)
S(6)
S(7)
S(8)
S(9)
S(da_0(x0))
S(da_1(x0))
S(da_2(x0))
S(da_3(x0))
S(da_4(x0))
S(da_5(x0))
S(da_6(x0))
S(da_7(x0))
S(da_8(x0))
S(da_9(x0))
plus(x0, 0)
plus(0, x0)
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(1, x0)
plus(2, x0)
plus(3, x0)
plus(4, x0)
plus(5, x0)
plus(6, x0)
plus(7, x0)
plus(8, x0)
plus(9, x0)
plus(da_0(x0), da_0(x1))
plus(da_1(x0), da_0(x1))
plus(da_2(x0), da_0(x1))
plus(da_3(x0), da_0(x1))
plus(da_4(x0), da_0(x1))
plus(da_5(x0), da_0(x1))
plus(da_6(x0), da_0(x1))
plus(da_7(x0), da_0(x1))
plus(da_8(x0), da_0(x1))
plus(da_9(x0), da_0(x1))
plus(da_0(x0), da_1(x1))
plus(da_1(x0), da_1(x1))
plus(da_2(x0), da_1(x1))
plus(da_3(x0), da_1(x1))
plus(da_4(x0), da_1(x1))
plus(da_5(x0), da_1(x1))
plus(da_6(x0), da_1(x1))
plus(da_7(x0), da_1(x1))
plus(da_8(x0), da_1(x1))
plus(da_9(x0), da_1(x1))
plus(da_0(x0), da_2(x1))
plus(da_1(x0), da_2(x1))
plus(da_2(x0), da_2(x1))
plus(da_3(x0), da_2(x1))
plus(da_4(x0), da_2(x1))
plus(da_5(x0), da_2(x1))
plus(da_6(x0), da_2(x1))
plus(da_7(x0), da_2(x1))
plus(da_8(x0), da_2(x1))
plus(da_9(x0), da_2(x1))
plus(da_0(x0), da_3(x1))
plus(da_1(x0), da_3(x1))
plus(da_2(x0), da_3(x1))
plus(da_3(x0), da_3(x1))
plus(da_4(x0), da_3(x1))
plus(da_5(x0), da_3(x1))
plus(da_6(x0), da_3(x1))
plus(da_7(x0), da_3(x1))
plus(da_8(x0), da_3(x1))
plus(da_9(x0), da_3(x1))
plus(da_0(x0), da_4(x1))
plus(da_1(x0), da_4(x1))
plus(da_2(x0), da_4(x1))
plus(da_3(x0), da_4(x1))
plus(da_4(x0), da_4(x1))
plus(da_5(x0), da_4(x1))
plus(da_6(x0), da_4(x1))
plus(da_7(x0), da_4(x1))
plus(da_8(x0), da_4(x1))
plus(da_9(x0), da_4(x1))
plus(da_0(x0), da_5(x1))
plus(da_1(x0), da_5(x1))
plus(da_2(x0), da_5(x1))
plus(da_3(x0), da_5(x1))
plus(da_4(x0), da_5(x1))
plus(da_5(x0), da_5(x1))
plus(da_6(x0), da_5(x1))
plus(da_7(x0), da_5(x1))
plus(da_8(x0), da_5(x1))
plus(da_9(x0), da_5(x1))
plus(da_0(x0), da_6(x1))
plus(da_1(x0), da_6(x1))
plus(da_2(x0), da_6(x1))
plus(da_3(x0), da_6(x1))
plus(da_4(x0), da_6(x1))
plus(da_5(x0), da_6(x1))
plus(da_6(x0), da_6(x1))
plus(da_7(x0), da_6(x1))
plus(da_8(x0), da_6(x1))
plus(da_9(x0), da_6(x1))
plus(da_0(x0), da_7(x1))
plus(da_1(x0), da_7(x1))
plus(da_2(x0), da_7(x1))
plus(da_3(x0), da_7(x1))
plus(da_4(x0), da_7(x1))
plus(da_5(x0), da_7(x1))
plus(da_6(x0), da_7(x1))
plus(da_7(x0), da_7(x1))
plus(da_8(x0), da_7(x1))
plus(da_9(x0), da_7(x1))
plus(da_0(x0), da_8(x1))
plus(da_1(x0), da_8(x1))
plus(da_2(x0), da_8(x1))
plus(da_3(x0), da_8(x1))
plus(da_4(x0), da_8(x1))
plus(da_5(x0), da_8(x1))
plus(da_6(x0), da_8(x1))
plus(da_7(x0), da_8(x1))
plus(da_8(x0), da_8(x1))
plus(da_9(x0), da_8(x1))
plus(da_0(x0), da_9(x1))
plus(da_1(x0), da_9(x1))
plus(da_2(x0), da_9(x1))
plus(da_3(x0), da_9(x1))
plus(da_4(x0), da_9(x1))
plus(da_5(x0), da_9(x1))
plus(da_6(x0), da_9(x1))
plus(da_7(x0), da_9(x1))
plus(da_8(x0), da_9(x1))
plus(da_9(x0), da_9(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, 2)
mult(x0, 3)
mult(x0, 4)
mult(x0, 5)
mult(x0, 6)
mult(x0, 7)
mult(x0, 8)
mult(x0, 9)
mult(x0, da_0(x1))
mult(x0, da_1(x1))
mult(x0, da_2(x1))
mult(x0, da_3(x1))
mult(x0, da_4(x1))
mult(x0, da_5(x1))
mult(x0, da_6(x1))
mult(x0, da_7(x1))
mult(x0, da_8(x1))
mult(x0, da_9(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(2)
P(3)
P(4)
P(5)
P(6)
P(7)
P(8)
P(9)
P(da_0(x0))
P(da_1(x0))
P(da_2(x0))
P(da_3(x0))
P(da_4(x0))
P(da_5(x0))
P(da_6(x0))
P(da_7(x0))
P(da_8(x0))
P(da_9(x0))
P(neg(x0))
S(neg(1))
S(neg(2))
S(neg(3))
S(neg(4))
S(neg(5))
S(neg(6))
S(neg(7))
S(neg(8))
S(neg(9))
S(neg(da_0(x0)))
S(neg(da_1(x0)))
S(neg(da_2(x0)))
S(neg(da_3(x0)))
S(neg(da_4(x0)))
S(neg(da_5(x0)))
S(neg(da_6(x0)))
S(neg(da_7(x0)))
S(neg(da_8(x0)))
S(neg(da_9(x0)))
da_0(neg(x0))
da_1(neg(x0))
da_2(neg(x0))
da_3(neg(x0))
da_4(neg(x0))
da_5(neg(x0))
da_6(neg(x0))
da_7(neg(x0))
da_8(neg(x0))
da_9(neg(x0))
plus(x0, neg(1))
plus(x0, neg(2))
plus(x0, neg(3))
plus(x0, neg(4))
plus(x0, neg(5))
plus(x0, neg(6))
plus(x0, neg(7))
plus(x0, neg(8))
plus(x0, neg(9))
plus(neg(1), x0)
plus(neg(2), x0)
plus(neg(3), x0)
plus(neg(4), x0)
plus(neg(5), x0)
plus(neg(6), x0)
plus(neg(7), x0)
plus(neg(8), x0)
plus(neg(9), x0)
plus(da_0(x0), neg(da_0(x1)))
plus(da_1(x0), neg(da_0(x1)))
plus(da_2(x0), neg(da_0(x1)))
plus(da_3(x0), neg(da_0(x1)))
plus(da_4(x0), neg(da_0(x1)))
plus(da_5(x0), neg(da_0(x1)))
plus(da_6(x0), neg(da_0(x1)))
plus(da_7(x0), neg(da_0(x1)))
plus(da_8(x0), neg(da_0(x1)))
plus(da_9(x0), neg(da_0(x1)))
plus(da_0(x0), neg(da_1(x1)))
plus(da_1(x0), neg(da_1(x1)))
plus(da_2(x0), neg(da_1(x1)))
plus(da_3(x0), neg(da_1(x1)))
plus(da_4(x0), neg(da_1(x1)))
plus(da_5(x0), neg(da_1(x1)))
plus(da_6(x0), neg(da_1(x1)))
plus(da_7(x0), neg(da_1(x1)))
plus(da_8(x0), neg(da_1(x1)))
plus(da_9(x0), neg(da_1(x1)))
plus(da_0(x0), neg(da_2(x1)))
plus(da_1(x0), neg(da_2(x1)))
plus(da_2(x0), neg(da_2(x1)))
plus(da_3(x0), neg(da_2(x1)))
plus(da_4(x0), neg(da_2(x1)))
plus(da_5(x0), neg(da_2(x1)))
plus(da_6(x0), neg(da_2(x1)))
plus(da_7(x0), neg(da_2(x1)))
plus(da_8(x0), neg(da_2(x1)))
plus(da_9(x0), neg(da_2(x1)))
plus(da_0(x0), neg(da_3(x1)))
plus(da_1(x0), neg(da_3(x1)))
plus(da_2(x0), neg(da_3(x1)))
plus(da_3(x0), neg(da_3(x1)))
plus(da_4(x0), neg(da_3(x1)))
plus(da_5(x0), neg(da_3(x1)))
plus(da_6(x0), neg(da_3(x1)))
plus(da_7(x0), neg(da_3(x1)))
plus(da_8(x0), neg(da_3(x1)))
plus(da_9(x0), neg(da_3(x1)))
plus(da_0(x0), neg(da_4(x1)))
plus(da_1(x0), neg(da_4(x1)))
plus(da_2(x0), neg(da_4(x1)))
plus(da_3(x0), neg(da_4(x1)))
plus(da_4(x0), neg(da_4(x1)))
plus(da_5(x0), neg(da_4(x1)))
plus(da_6(x0), neg(da_4(x1)))
plus(da_7(x0), neg(da_4(x1)))
plus(da_8(x0), neg(da_4(x1)))
plus(da_9(x0), neg(da_4(x1)))
plus(da_0(x0), neg(da_5(x1)))
plus(da_1(x0), neg(da_5(x1)))
plus(da_2(x0), neg(da_5(x1)))
plus(da_3(x0), neg(da_5(x1)))
plus(da_4(x0), neg(da_5(x1)))
plus(da_5(x0), neg(da_5(x1)))
plus(da_6(x0), neg(da_5(x1)))
plus(da_7(x0), neg(da_5(x1)))
plus(da_8(x0), neg(da_5(x1)))
plus(da_9(x0), neg(da_5(x1)))
plus(da_0(x0), neg(da_6(x1)))
plus(da_1(x0), neg(da_6(x1)))
plus(da_2(x0), neg(da_6(x1)))
plus(da_3(x0), neg(da_6(x1)))
plus(da_4(x0), neg(da_6(x1)))
plus(da_5(x0), neg(da_6(x1)))
plus(da_6(x0), neg(da_6(x1)))
plus(da_7(x0), neg(da_6(x1)))
plus(da_8(x0), neg(da_6(x1)))
plus(da_9(x0), neg(da_6(x1)))
plus(da_0(x0), neg(da_7(x1)))
plus(da_1(x0), neg(da_7(x1)))
plus(da_2(x0), neg(da_7(x1)))
plus(da_3(x0), neg(da_7(x1)))
plus(da_4(x0), neg(da_7(x1)))
plus(da_5(x0), neg(da_7(x1)))
plus(da_6(x0), neg(da_7(x1)))
plus(da_7(x0), neg(da_7(x1)))
plus(da_8(x0), neg(da_7(x1)))
plus(da_9(x0), neg(da_7(x1)))
plus(da_0(x0), neg(da_8(x1)))
plus(da_1(x0), neg(da_8(x1)))
plus(da_2(x0), neg(da_8(x1)))
plus(da_3(x0), neg(da_8(x1)))
plus(da_4(x0), neg(da_8(x1)))
plus(da_5(x0), neg(da_8(x1)))
plus(da_6(x0), neg(da_8(x1)))
plus(da_7(x0), neg(da_8(x1)))
plus(da_8(x0), neg(da_8(x1)))
plus(da_9(x0), neg(da_8(x1)))
plus(da_0(x0), neg(da_9(x1)))
plus(da_1(x0), neg(da_9(x1)))
plus(da_2(x0), neg(da_9(x1)))
plus(da_3(x0), neg(da_9(x1)))
plus(da_4(x0), neg(da_9(x1)))
plus(da_5(x0), neg(da_9(x1)))
plus(da_6(x0), neg(da_9(x1)))
plus(da_7(x0), neg(da_9(x1)))
plus(da_8(x0), neg(da_9(x1)))
plus(da_9(x0), neg(da_9(x1)))
plus(neg(da_0(x0)), da_0(x1))
plus(neg(da_0(x0)), da_1(x1))
plus(neg(da_0(x0)), da_2(x1))
plus(neg(da_0(x0)), da_3(x1))
plus(neg(da_0(x0)), da_4(x1))
plus(neg(da_0(x0)), da_5(x1))
plus(neg(da_0(x0)), da_6(x1))
plus(neg(da_0(x0)), da_7(x1))
plus(neg(da_0(x0)), da_8(x1))
plus(neg(da_0(x0)), da_9(x1))
plus(neg(da_1(x0)), da_0(x1))
plus(neg(da_1(x0)), da_1(x1))
plus(neg(da_1(x0)), da_2(x1))
plus(neg(da_1(x0)), da_3(x1))
plus(neg(da_1(x0)), da_4(x1))
plus(neg(da_1(x0)), da_5(x1))
plus(neg(da_1(x0)), da_6(x1))
plus(neg(da_1(x0)), da_7(x1))
plus(neg(da_1(x0)), da_8(x1))
plus(neg(da_1(x0)), da_9(x1))
plus(neg(da_2(x0)), da_0(x1))
plus(neg(da_2(x0)), da_1(x1))
plus(neg(da_2(x0)), da_2(x1))
plus(neg(da_2(x0)), da_3(x1))
plus(neg(da_2(x0)), da_4(x1))
plus(neg(da_2(x0)), da_5(x1))
plus(neg(da_2(x0)), da_6(x1))
plus(neg(da_2(x0)), da_7(x1))
plus(neg(da_2(x0)), da_8(x1))
plus(neg(da_2(x0)), da_9(x1))
plus(neg(da_3(x0)), da_0(x1))
plus(neg(da_3(x0)), da_1(x1))
plus(neg(da_3(x0)), da_2(x1))
plus(neg(da_3(x0)), da_3(x1))
plus(neg(da_3(x0)), da_4(x1))
plus(neg(da_3(x0)), da_5(x1))
plus(neg(da_3(x0)), da_6(x1))
plus(neg(da_3(x0)), da_7(x1))
plus(neg(da_3(x0)), da_8(x1))
plus(neg(da_3(x0)), da_9(x1))
plus(neg(da_4(x0)), da_0(x1))
plus(neg(da_4(x0)), da_1(x1))
plus(neg(da_4(x0)), da_2(x1))
plus(neg(da_4(x0)), da_3(x1))
plus(neg(da_4(x0)), da_4(x1))
plus(neg(da_4(x0)), da_5(x1))
plus(neg(da_4(x0)), da_6(x1))
plus(neg(da_4(x0)), da_7(x1))
plus(neg(da_4(x0)), da_8(x1))
plus(neg(da_4(x0)), da_9(x1))
plus(neg(da_5(x0)), da_0(x1))
plus(neg(da_5(x0)), da_1(x1))
plus(neg(da_5(x0)), da_2(x1))
plus(neg(da_5(x0)), da_3(x1))
plus(neg(da_5(x0)), da_4(x1))
plus(neg(da_5(x0)), da_5(x1))
plus(neg(da_5(x0)), da_6(x1))
plus(neg(da_5(x0)), da_7(x1))
plus(neg(da_5(x0)), da_8(x1))
plus(neg(da_5(x0)), da_9(x1))
plus(neg(da_6(x0)), da_0(x1))
plus(neg(da_6(x0)), da_1(x1))
plus(neg(da_6(x0)), da_2(x1))
plus(neg(da_6(x0)), da_3(x1))
plus(neg(da_6(x0)), da_4(x1))
plus(neg(da_6(x0)), da_5(x1))
plus(neg(da_6(x0)), da_6(x1))
plus(neg(da_6(x0)), da_7(x1))
plus(neg(da_6(x0)), da_8(x1))
plus(neg(da_6(x0)), da_9(x1))
plus(neg(da_7(x0)), da_0(x1))
plus(neg(da_7(x0)), da_1(x1))
plus(neg(da_7(x0)), da_2(x1))
plus(neg(da_7(x0)), da_3(x1))
plus(neg(da_7(x0)), da_4(x1))
plus(neg(da_7(x0)), da_5(x1))
plus(neg(da_7(x0)), da_6(x1))
plus(neg(da_7(x0)), da_7(x1))
plus(neg(da_7(x0)), da_8(x1))
plus(neg(da_7(x0)), da_9(x1))
plus(neg(da_8(x0)), da_0(x1))
plus(neg(da_8(x0)), da_1(x1))
plus(neg(da_8(x0)), da_2(x1))
plus(neg(da_8(x0)), da_3(x1))
plus(neg(da_8(x0)), da_4(x1))
plus(neg(da_8(x0)), da_5(x1))
plus(neg(da_8(x0)), da_6(x1))
plus(neg(da_8(x0)), da_7(x1))
plus(neg(da_8(x0)), da_8(x1))
plus(neg(da_8(x0)), da_9(x1))
plus(neg(da_9(x0)), da_0(x1))
plus(neg(da_9(x0)), da_1(x1))
plus(neg(da_9(x0)), da_2(x1))
plus(neg(da_9(x0)), da_3(x1))
plus(neg(da_9(x0)), da_4(x1))
plus(neg(da_9(x0)), da_5(x1))
plus(neg(da_9(x0)), da_6(x1))
plus(neg(da_9(x0)), da_7(x1))
plus(neg(da_9(x0)), da_8(x1))
plus(neg(da_9(x0)), da_9(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))