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

0 QTRS
↳1 DependencyPairsProof (⇔, 89 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 (⇔, 35 ms)
        ↳11 QDP
        ↳12 DependencyGraphProof (⇔, 0 ms)
        ↳13 QDP
        ↳14 MRRProof (⇔, 11 ms)
        ↳15 QDP
        ↳16 TransformationProof (⇔, 0 ms)
        ↳17 QDP
        ↳18 QDPOrderProof (⇔, 6 ms)
        ↳19 QDP
        ↳20 DependencyGraphProof (⇔, 0 ms)
        ↳21 TRUE
    ↳22 QDP
        ↳23 UsableRulesProof (⇔, 0 ms)
        ↳24 QDP
        ↳25 QReductionProof (⇔, 0 ms)
        ↳26 QDP
        ↳27 QDPSizeChangeProof (⇔, 0 ms)
        ↳28 YES

(0) Obligation:

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

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

The set Q consists of the following terms:

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

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

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

BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(x, bt(y, z)) → PLUS(x, y)
PLUS(1, 1) → BT(1, 0)
PLUS(x, bt(y, z)) → BT(y, plus(x, z))
PLUS(x, bt(y, z)) → PLUS(x, z)
PLUS(bt(x, y), z) → BT(x, plus(y, z))
PLUS(bt(x, y), z) → PLUS(y, z)
MULT(x, bt(y, z)) → BT(mult(x, y), mult(x, z))
MULT(x, bt(y, z)) → MULT(x, y)
MULT(x, bt(y, z)) → MULT(x, z)
MULT(bt(x, y), z) → BT(mult(x, z), mult(y, z))
MULT(bt(x, y), z) → MULT(x, z)
MULT(bt(x, y), z) → MULT(y, z)
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(bt(x, 0), neg(1)) → BT(x, neg(1))
BT(bt(x, 1), neg(1)) → BT(bt(x, 0), 1)
BT(bt(x, 1), neg(1)) → BT(x, 0)
BT(x, neg(bt(y, z))) → NEG(bt(plus(y, neg(x)), z))
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
BT(x, neg(bt(y, z))) → PLUS(y, neg(x))
BT(x, neg(bt(y, z))) → NEG(x)
BT(neg(x), y) → NEG(bt(x, neg(y)))
BT(neg(x), y) → BT(x, neg(y))
BT(neg(x), y) → NEG(y)
PLUS(x, neg(bt(y, z))) → NEG(bt(y, plus(z, neg(x))))
PLUS(x, neg(bt(y, z))) → BT(y, plus(z, neg(x)))
PLUS(x, neg(bt(y, z))) → PLUS(z, neg(x))
PLUS(x, neg(bt(y, z))) → NEG(x)
PLUS(neg(bt(x, y)), z) → NEG(bt(x, plus(y, neg(z))))
PLUS(neg(bt(x, y)), z) → BT(x, plus(y, neg(z)))
PLUS(neg(bt(x, y)), z) → PLUS(y, neg(z))
PLUS(neg(bt(x, y)), z) → NEG(z)
MULT(x, neg(y)) → NEG(mult(x, y))
MULT(x, neg(y)) → MULT(x, y)
MULT(neg(x), y) → NEG(mult(x, y))
MULT(neg(x), y) → MULT(x, y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

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

BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(neg(x), y) → BT(x, neg(y))
BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(bt(x, 0), neg(1)) → BT(x, neg(1))
BT(x, bt(y, z)) → PLUS(x, y)
PLUS(x, bt(y, z)) → BT(y, plus(x, z))
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
BT(x, neg(bt(y, z))) → PLUS(y, neg(x))
PLUS(x, bt(y, z)) → PLUS(x, z)
PLUS(bt(x, y), z) → BT(x, plus(y, z))
PLUS(bt(x, y), z) → PLUS(y, z)
PLUS(x, neg(bt(y, z))) → BT(y, plus(z, neg(x)))
PLUS(x, neg(bt(y, z))) → PLUS(z, neg(x))
PLUS(neg(bt(x, y)), z) → BT(x, plus(y, neg(z)))
PLUS(neg(bt(x, y)), z) → PLUS(y, neg(z))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(6) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(7) Obligation:

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

BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(neg(x), y) → BT(x, neg(y))
BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(bt(x, 0), neg(1)) → BT(x, neg(1))
BT(x, bt(y, z)) → PLUS(x, y)
PLUS(x, bt(y, z)) → BT(y, plus(x, z))
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
BT(x, neg(bt(y, z))) → PLUS(y, neg(x))
PLUS(x, bt(y, z)) → PLUS(x, z)
PLUS(bt(x, y), z) → BT(x, plus(y, z))
PLUS(bt(x, y), z) → PLUS(y, z)
PLUS(x, neg(bt(y, z))) → BT(y, plus(z, neg(x)))
PLUS(x, neg(bt(y, z))) → PLUS(z, neg(x))
PLUS(neg(bt(x, y)), z) → BT(x, plus(y, neg(z)))
PLUS(neg(bt(x, y)), z) → PLUS(y, neg(z))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(8) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

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

(9) Obligation:

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

BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(neg(x), y) → BT(x, neg(y))
BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(bt(x, 0), neg(1)) → BT(x, neg(1))
BT(x, bt(y, z)) → PLUS(x, y)
PLUS(x, bt(y, z)) → BT(y, plus(x, z))
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
BT(x, neg(bt(y, z))) → PLUS(y, neg(x))
PLUS(x, bt(y, z)) → PLUS(x, z)
PLUS(bt(x, y), z) → BT(x, plus(y, z))
PLUS(bt(x, y), z) → PLUS(y, z)
PLUS(x, neg(bt(y, z))) → BT(y, plus(z, neg(x)))
PLUS(x, neg(bt(y, z))) → PLUS(z, neg(x))
PLUS(neg(bt(x, y)), z) → BT(x, plus(y, neg(z)))
PLUS(neg(bt(x, y)), z) → PLUS(y, neg(z))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(10) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

BT(bt(x, 0), neg(1)) → BT(x, neg(1))
BT(x, bt(y, z)) → PLUS(x, y)
BT(x, neg(bt(y, z))) → PLUS(y, neg(x))
PLUS(x, bt(y, z)) → PLUS(x, z)
PLUS(bt(x, y), z) → PLUS(y, z)
PLUS(x, neg(bt(y, z))) → PLUS(z, neg(x))
PLUS(neg(bt(x, y)), z) → PLUS(y, neg(z))

Strictly oriented rules of the TRS R:

plus(0, x) → x
plus(x, 0) → x
plus(1, neg(1)) → 0
plus(neg(1), 1) → 0
bt(1, neg(1)) → 1
bt(0, x) → x

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 2   
POL(1) = 2   
POL(BT(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(PLUS(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(bt(x1, x2)) = 1 + x1 + x2   
POL(neg(x1)) = x1   
POL(plus(x1, x2)) = 1 + x1 + x2   

(11) Obligation:

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

BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(neg(x), y) → BT(x, neg(y))
BT(x, bt(y, z)) → BT(plus(x, y), z)
PLUS(x, bt(y, z)) → BT(y, plus(x, z))
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
PLUS(bt(x, y), z) → BT(x, plus(y, z))
PLUS(x, neg(bt(y, z))) → BT(y, plus(z, neg(x)))
PLUS(neg(bt(x, y)), z) → BT(x, plus(y, neg(z)))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(12) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.

(13) Obligation:

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

BT(neg(x), y) → BT(x, neg(y))
BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(14) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 1   
POL(1) = 1   
POL(BT(x1, x2)) = x1 + 2·x2   
POL(bt(x1, x2)) = 1 + x1 + x2   
POL(neg(x1)) = x1   
POL(plus(x1, x2)) = 1 + x1 + x2   

(15) Obligation:

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

BT(neg(x), y) → BT(x, neg(y))
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(16) TransformationProof (EQUIVALENT transformation)

By instantiating [LPAR04] the rule BT(neg(x), y) → BT(x, neg(y)) we obtained the following new rules [LPAR04]:

BT(neg(x0), 1) → BT(x0, neg(1)) → BT(neg(x0), 1) → BT(x0, neg(1))

(17) Obligation:

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

BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(neg(x0), 1) → BT(x0, neg(1))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
BT(x1, x2)  =  x1
bt(x1, x2)  =  x2
0  =  0
neg(x1)  =  x1
1  =  1

Knuth-Bendix order [KBO] with precedence:
0 > 1

and weight map:

0=1
1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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

(19) Obligation:

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

BT(neg(x0), 1) → BT(x0, neg(1))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(20) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(21) TRUE

(22) Obligation:

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

MULT(x, bt(y, z)) → MULT(x, z)
MULT(bt(x, y), z) → MULT(x, z)
MULT(x, bt(y, z)) → MULT(x, y)
MULT(bt(x, y), z) → MULT(y, z)
MULT(x, neg(y)) → MULT(x, y)
MULT(neg(x), y) → MULT(x, y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(23) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(24) Obligation:

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

MULT(x, bt(y, z)) → MULT(x, z)
MULT(bt(x, y), z) → MULT(x, z)
MULT(x, bt(y, z)) → MULT(x, y)
MULT(bt(x, y), z) → MULT(y, z)
MULT(x, neg(y)) → MULT(x, y)
MULT(neg(x), y) → MULT(x, y)

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

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

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

(25) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

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

(26) Obligation:

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

MULT(x, bt(y, z)) → MULT(x, z)
MULT(bt(x, y), z) → MULT(x, z)
MULT(x, bt(y, z)) → MULT(x, y)
MULT(bt(x, y), z) → MULT(y, z)
MULT(x, neg(y)) → MULT(x, y)
MULT(neg(x), y) → MULT(x, y)

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

bt(0, x0)
bt(x0, bt(x1, x2))
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)

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

(27) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

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

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

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

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

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

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

(28) YES