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

0 QTRS
↳1 QTRSRRRProof (⇔, 107 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 0 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 0 ms)
↳6 QTRS
↳7 RisEmptyProof (⇔, 0 ms)
↳8 YES

(0) Obligation:

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

neg(0) → 0
neg(neg(x)) → x
plus(x, plus(y, z)) → plus(plus(x, y), z)
plus(x, 0) → x
plus(1, neg(1)) → 0
plus(plus(x, 1), neg(1)) → x
plus(x, neg(plus(y, 1))) → plus(plus(x, neg(y)), neg(1))
plus(0, x) → x
plus(neg(1), 1) → 0
plus(neg(plus(x, 1)), 1) → neg(x)
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, 0) → 0
mult(x, 1) → x
mult(x, neg(y)) → mult(neg(x), y)
mult(x, plus(y, z)) → plus(mult(x, y), mult(x, z))

The set Q consists of the following terms:

neg(0)
neg(neg(x0))
plus(x0, plus(x1, x2))
plus(x0, 0)
plus(1, neg(1))
plus(plus(x0, 1), neg(1))
plus(x0, neg(plus(x1, 1)))
plus(0, x0)
plus(neg(1), 1)
plus(neg(plus(x0, 1)), 1)
plus(neg(x0), neg(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, neg(x1))
mult(x0, plus(x1, x2))

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
neg(x1)  =  x1
0  =  0
plus(x1, x2)  =  plus(x1, x2)
1  =  1
mult(x1, x2)  =  mult(x1, x2)

Recursive path order with status [RPO].
Quasi-Precedence:
mult2 > [0, plus2, 1]

Status:
0: multiset
plus2: [2,1]
1: multiset
mult2: [2,1]

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

plus(x, plus(y, z)) → plus(plus(x, y), z)
plus(x, 0) → x
plus(1, neg(1)) → 0
plus(plus(x, 1), neg(1)) → x
plus(x, neg(plus(y, 1))) → plus(plus(x, neg(y)), neg(1))
plus(0, x) → x
plus(neg(1), 1) → 0
plus(neg(plus(x, 1)), 1) → neg(x)
mult(x, 0) → 0
mult(x, 1) → x
mult(x, plus(y, z)) → plus(mult(x, y), mult(x, z))


(2) Obligation:

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

neg(0) → 0
neg(neg(x)) → x
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, neg(y)) → mult(neg(x), y)

The set Q consists of the following terms:

neg(0)
neg(neg(x0))
plus(x0, plus(x1, x2))
plus(x0, 0)
plus(1, neg(1))
plus(plus(x0, 1), neg(1))
plus(x0, neg(plus(x1, 1)))
plus(0, x0)
plus(neg(1), 1)
plus(neg(plus(x0, 1)), 1)
plus(neg(x0), neg(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, neg(x1))
mult(x0, plus(x1, x2))

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 1   
POL(mult(x1, x2)) = 2·x1 + 2·x2   
POL(neg(x1)) = 1 + x1   
POL(plus(x1, x2)) = x1 + x2   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

neg(0) → 0
neg(neg(x)) → x
plus(neg(x), neg(y)) → neg(plus(x, y))


(4) Obligation:

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

mult(x, neg(y)) → mult(neg(x), y)

The set Q consists of the following terms:

neg(0)
neg(neg(x0))
plus(x0, plus(x1, x2))
plus(x0, 0)
plus(1, neg(1))
plus(plus(x0, 1), neg(1))
plus(x0, neg(plus(x1, 1)))
plus(0, x0)
plus(neg(1), 1)
plus(neg(plus(x0, 1)), 1)
plus(neg(x0), neg(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, neg(x1))
mult(x0, plus(x1, x2))

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(mult(x1, x2)) = x1 + 2·x2   
POL(neg(x1)) = 1 + x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

mult(x, neg(y)) → mult(neg(x), y)


(6) Obligation:

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

neg(0)
neg(neg(x0))
plus(x0, plus(x1, x2))
plus(x0, 0)
plus(1, neg(1))
plus(plus(x0, 1), neg(1))
plus(x0, neg(plus(x1, 1)))
plus(0, x0)
plus(neg(1), 1)
plus(neg(plus(x0, 1)), 1)
plus(neg(x0), neg(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, neg(x1))
mult(x0, plus(x1, x2))

(7) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(8) YES