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

0 QTRS
↳1 DependencyPairsProof (⇔, 71 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 (⇔, 2 ms)
        ↳11 QDP
        ↳12 PisEmptyProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 QReductionProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 QDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 QDP
        ↳24 QReductionProof (⇔, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 QDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 QDP
        ↳31 QReductionProof (⇔, 0 ms)
        ↳32 QDP
        ↳33 TransformationProof (⇔, 0 ms)
        ↳34 QDP
        ↳35 DependencyGraphProof (⇔, 0 ms)
        ↳36 QDP
        ↳37 TransformationProof (⇔, 0 ms)
        ↳38 QDP
        ↳39 DependencyGraphProof (⇔, 0 ms)
        ↳40 AND
            ↳41 QDP
                ↳42 UsableRulesProof (⇔, 0 ms)
                ↳43 QDP
                ↳44 QReductionProof (⇔, 0 ms)
                ↳45 QDP
                ↳46 QDPSizeChangeProof (⇔, 0 ms)
                ↳47 YES
            ↳48 QDP
                ↳49 TransformationProof (⇔, 0 ms)
                ↳50 QDP
                ↳51 DependencyGraphProof (⇔, 0 ms)
                ↳52 QDP
                ↳53 TransformationProof (⇔, 0 ms)
                ↳54 QDP
                ↳55 DependencyGraphProof (⇔, 0 ms)
                ↳56 TRUE
    ↳57 QDP
        ↳58 UsableRulesProof (⇔, 0 ms)
        ↳59 QDP
        ↳60 QReductionProof (⇔, 0 ms)
        ↳61 QDP
        ↳62 QDPSizeChangeProof (⇔, 0 ms)
        ↳63 YES

(0) Obligation:

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

ba0(0) → 0
ba1(0) → 1
S(0) → 1
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(1, x) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
mult(x, 0) → 0
mult(x, 1) → x
mult(x, ba0(y)) → plus(ba0(mult(x, y)), mult(x, 0))
mult(x, ba1(y)) → plus(ba0(mult(x, y)), mult(x, 1))
neg(0) → 0
neg(neg(x)) → x
P(0) → neg(1)
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
P(neg(x)) → neg(S(x))
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))
ba0(neg(x)) → neg(ba0(x))
ba1(neg(x)) → neg(ba1(P(x)))
plus(x, neg(1)) → P(x)
plus(neg(1), x) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, neg(y)) → neg(mult(x, y))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(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:

S1(1) → BA0(1)
S1(ba0(x)) → BA1(x)
S1(ba1(x)) → BA0(S(x))
S1(ba1(x)) → S1(x)
PLUS(x, 1) → S1(x)
PLUS(1, x) → S1(x)
PLUS(ba0(x), ba0(y)) → PLUS(ba0(plus(x, y)), 0)
PLUS(ba0(x), ba0(y)) → BA0(plus(x, y))
PLUS(ba0(x), ba0(y)) → PLUS(x, y)
PLUS(ba1(x), ba0(y)) → PLUS(ba1(plus(x, y)), 0)
PLUS(ba1(x), ba0(y)) → BA1(plus(x, y))
PLUS(ba1(x), ba0(y)) → PLUS(x, y)
PLUS(ba0(x), ba1(y)) → PLUS(ba0(plus(x, y)), 1)
PLUS(ba0(x), ba1(y)) → BA0(plus(x, y))
PLUS(ba0(x), ba1(y)) → PLUS(x, y)
PLUS(ba1(x), ba1(y)) → PLUS(ba1(plus(x, y)), 1)
PLUS(ba1(x), ba1(y)) → BA1(plus(x, y))
PLUS(ba1(x), ba1(y)) → PLUS(x, y)
MULT(x, ba0(y)) → PLUS(ba0(mult(x, y)), mult(x, 0))
MULT(x, ba0(y)) → BA0(mult(x, y))
MULT(x, ba0(y)) → MULT(x, y)
MULT(x, ba0(y)) → MULT(x, 0)
MULT(x, ba1(y)) → PLUS(ba0(mult(x, y)), mult(x, 1))
MULT(x, ba1(y)) → BA0(mult(x, y))
MULT(x, ba1(y)) → MULT(x, y)
MULT(x, ba1(y)) → MULT(x, 1)
P1(0) → NEG(1)
P1(ba0(x)) → BA1(P(x))
P1(ba0(x)) → P1(x)
P1(ba1(x)) → BA0(x)
P1(neg(x)) → NEG(S(x))
P1(neg(x)) → S1(x)
S1(neg(ba0(x))) → NEG(ba1(P(x)))
S1(neg(ba0(x))) → BA1(P(x))
S1(neg(ba0(x))) → P1(x)
S1(neg(ba1(x))) → NEG(ba0(x))
S1(neg(ba1(x))) → BA0(x)
BA0(neg(x)) → NEG(ba0(x))
BA0(neg(x)) → BA0(x)
BA1(neg(x)) → NEG(ba1(P(x)))
BA1(neg(x)) → BA1(P(x))
BA1(neg(x)) → P1(x)
PLUS(x, neg(1)) → P1(x)
PLUS(neg(1), x) → P1(x)
PLUS(ba1(x), neg(ba1(y))) → PLUS(ba1(plus(x, neg(y))), neg(1))
PLUS(ba1(x), neg(ba1(y))) → BA1(plus(x, neg(y)))
PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba1(y))) → NEG(y)
PLUS(ba1(x), neg(ba1(y))) → NEG(1)
PLUS(ba0(x), neg(ba1(y))) → PLUS(ba0(plus(x, neg(y))), neg(1))
PLUS(ba0(x), neg(ba1(y))) → BA0(plus(x, neg(y)))
PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba1(y))) → NEG(y)
PLUS(ba0(x), neg(ba1(y))) → NEG(1)
PLUS(ba1(x), neg(ba0(y))) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(ba1(x), neg(ba0(y))) → BA1(plus(x, neg(y)))
PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → NEG(y)
PLUS(ba1(x), neg(ba0(y))) → NEG(0)
PLUS(ba0(x), neg(ba0(y))) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(ba0(x), neg(ba0(y))) → BA0(plus(x, neg(y)))
PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → NEG(y)
PLUS(ba0(x), neg(ba0(y))) → NEG(0)
PLUS(neg(ba1(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(1))
PLUS(neg(ba1(y)), ba1(x)) → BA1(plus(x, neg(y)))
PLUS(neg(ba1(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba1(x)) → NEG(y)
PLUS(neg(ba1(y)), ba1(x)) → NEG(1)
PLUS(neg(ba1(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), neg(1))
PLUS(neg(ba1(y)), ba0(x)) → BA0(plus(x, neg(y)))
PLUS(neg(ba1(y)), ba0(x)) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba0(x)) → NEG(y)
PLUS(neg(ba1(y)), ba0(x)) → NEG(1)
PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba1(x)) → BA1(plus(x, neg(y)))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba1(x)) → NEG(y)
PLUS(neg(ba0(y)), ba1(x)) → NEG(0)
PLUS(neg(ba0(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba0(x)) → BA0(plus(x, neg(y)))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba0(x)) → NEG(y)
PLUS(neg(ba0(y)), ba0(x)) → NEG(0)
PLUS(neg(x), neg(y)) → NEG(plus(x, y))
PLUS(neg(x), neg(y)) → PLUS(x, y)
MULT(x, neg(y)) → NEG(mult(x, y))
MULT(x, neg(y)) → MULT(x, y)

The TRS R consists of the following rules:

ba0(0) → 0
ba1(0) → 1
S(0) → 1
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(1, x) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
mult(x, 0) → 0
mult(x, 1) → x
mult(x, ba0(y)) → plus(ba0(mult(x, y)), mult(x, 0))
mult(x, ba1(y)) → plus(ba0(mult(x, y)), mult(x, 1))
neg(0) → 0
neg(neg(x)) → x
P(0) → neg(1)
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
P(neg(x)) → neg(S(x))
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))
ba0(neg(x)) → neg(ba0(x))
ba1(neg(x)) → neg(ba1(P(x)))
plus(x, neg(1)) → P(x)
plus(neg(1), x) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, neg(y)) → neg(mult(x, y))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(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 5 SCCs with 65 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

P1(ba0(x)) → BA1(P(x))
BA1(neg(x)) → BA1(P(x))
BA1(neg(x)) → P1(x)
P1(ba0(x)) → P1(x)

The TRS R consists of the following rules:

ba0(0) → 0
ba1(0) → 1
S(0) → 1
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(1, x) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
mult(x, 0) → 0
mult(x, 1) → x
mult(x, ba0(y)) → plus(ba0(mult(x, y)), mult(x, 0))
mult(x, ba1(y)) → plus(ba0(mult(x, y)), mult(x, 1))
neg(0) → 0
neg(neg(x)) → x
P(0) → neg(1)
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
P(neg(x)) → neg(S(x))
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))
ba0(neg(x)) → neg(ba0(x))
ba1(neg(x)) → neg(ba1(P(x)))
plus(x, neg(1)) → P(x)
plus(neg(1), x) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, neg(y)) → neg(mult(x, y))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(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:

P1(ba0(x)) → BA1(P(x))
BA1(neg(x)) → BA1(P(x))
BA1(neg(x)) → P1(x)
P1(ba0(x)) → P1(x)

The TRS R consists of the following rules:

P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
neg(0) → 0
neg(neg(x)) → x

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(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].

S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

(9) Obligation:

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

P1(ba0(x)) → BA1(P(x))
BA1(neg(x)) → BA1(P(x))
BA1(neg(x)) → P1(x)
P1(ba0(x)) → P1(x)

The TRS R consists of the following rules:

P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
neg(0) → 0
neg(neg(x)) → x

The set Q consists of the following terms:

ba0(0)
ba1(0)
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
ba0(neg(x0))
ba1(neg(x0))

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:

P1(ba0(x)) → BA1(P(x))
BA1(neg(x)) → BA1(P(x))
BA1(neg(x)) → P1(x)
P1(ba0(x)) → P1(x)

Strictly oriented rules of the TRS R:

P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
neg(0) → 0
neg(neg(x)) → x

Used ordering: Knuth-Bendix order [KBO] with precedence:
P1 > BA11 > P^11 > ba11 > neg1 > ba01 > 0 > 1

and weight map:

1=3
0=1
P_1=0
ba0_1=2
ba1_1=2
neg_1=1
P^1_1=2
BA1_1=1

The variable weight is 1

(11) Obligation:

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

ba0(0)
ba1(0)
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
ba0(neg(x0))
ba1(neg(x0))

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

(12) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(13) YES

(14) Obligation:

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

S1(ba1(x)) → S1(x)

The TRS R consists of the following rules:

ba0(0) → 0
ba1(0) → 1
S(0) → 1
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(1, x) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
mult(x, 0) → 0
mult(x, 1) → x
mult(x, ba0(y)) → plus(ba0(mult(x, y)), mult(x, 0))
mult(x, ba1(y)) → plus(ba0(mult(x, y)), mult(x, 1))
neg(0) → 0
neg(neg(x)) → x
P(0) → neg(1)
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
P(neg(x)) → neg(S(x))
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))
ba0(neg(x)) → neg(ba0(x))
ba1(neg(x)) → neg(ba1(P(x)))
plus(x, neg(1)) → P(x)
plus(neg(1), x) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, neg(y)) → neg(mult(x, y))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

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

(15) 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.

(16) Obligation:

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

S1(ba1(x)) → S1(x)

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

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

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

(17) 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].

ba0(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

(18) Obligation:

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

S1(ba1(x)) → S1(x)

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

ba1(0)
ba1(neg(x0))

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

(19) 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:

  • S1(ba1(x)) → S1(x)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

PLUS(ba1(x), ba0(y)) → PLUS(x, y)
PLUS(ba0(x), ba0(y)) → PLUS(x, y)
PLUS(ba0(x), ba1(y)) → PLUS(x, y)
PLUS(ba1(x), ba1(y)) → PLUS(x, y)

The TRS R consists of the following rules:

ba0(0) → 0
ba1(0) → 1
S(0) → 1
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(1, x) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
mult(x, 0) → 0
mult(x, 1) → x
mult(x, ba0(y)) → plus(ba0(mult(x, y)), mult(x, 0))
mult(x, ba1(y)) → plus(ba0(mult(x, y)), mult(x, 1))
neg(0) → 0
neg(neg(x)) → x
P(0) → neg(1)
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
P(neg(x)) → neg(S(x))
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))
ba0(neg(x)) → neg(ba0(x))
ba1(neg(x)) → neg(ba1(P(x)))
plus(x, neg(1)) → P(x)
plus(neg(1), x) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, neg(y)) → neg(mult(x, y))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

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

(22) 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.

(23) Obligation:

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

PLUS(ba1(x), ba0(y)) → PLUS(x, y)
PLUS(ba0(x), ba0(y)) → PLUS(x, y)
PLUS(ba0(x), ba1(y)) → PLUS(x, y)
PLUS(ba1(x), ba1(y)) → PLUS(x, y)

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

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

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

(24) 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].

S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

(25) Obligation:

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

PLUS(ba1(x), ba0(y)) → PLUS(x, y)
PLUS(ba0(x), ba0(y)) → PLUS(x, y)
PLUS(ba0(x), ba1(y)) → PLUS(x, y)
PLUS(ba1(x), ba1(y)) → PLUS(x, y)

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

ba0(0)
ba1(0)
ba0(neg(x0))
ba1(neg(x0))

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

(26) 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:

  • PLUS(ba1(x), ba0(y)) → PLUS(x, y)
    The graph contains the following edges 1 > 1, 2 > 2

  • PLUS(ba0(x), ba0(y)) → PLUS(x, y)
    The graph contains the following edges 1 > 1, 2 > 2

  • PLUS(ba0(x), ba1(y)) → PLUS(x, y)
    The graph contains the following edges 1 > 1, 2 > 2

  • PLUS(ba1(x), ba1(y)) → PLUS(x, y)
    The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

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

PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba0(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(x, neg(y))

The TRS R consists of the following rules:

ba0(0) → 0
ba1(0) → 1
S(0) → 1
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(1, x) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
mult(x, 0) → 0
mult(x, 1) → x
mult(x, ba0(y)) → plus(ba0(mult(x, y)), mult(x, 0))
mult(x, ba1(y)) → plus(ba0(mult(x, y)), mult(x, 1))
neg(0) → 0
neg(neg(x)) → x
P(0) → neg(1)
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
P(neg(x)) → neg(S(x))
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))
ba0(neg(x)) → neg(ba0(x))
ba1(neg(x)) → neg(ba1(P(x)))
plus(x, neg(1)) → P(x)
plus(neg(1), x) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, neg(y)) → neg(mult(x, y))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

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

(29) 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.

(30) Obligation:

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

PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba0(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(x, neg(y))

The TRS R consists of the following rules:

plus(1, x) → S(x)
plus(x, neg(1)) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
ba0(0) → 0
ba0(neg(x)) → neg(ba0(x))
neg(0) → 0
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
plus(neg(1), x) → P(x)
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(x), neg(y)) → neg(plus(x, y))
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
neg(neg(x)) → x
P(0) → neg(1)
P(neg(x)) → neg(S(x))
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
S(0) → 1
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

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

(31) 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(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
mult(x0, neg(x1))

(32) Obligation:

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

PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba0(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(x, neg(y))

The TRS R consists of the following rules:

plus(1, x) → S(x)
plus(x, neg(1)) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
ba0(0) → 0
ba0(neg(x)) → neg(ba0(x))
neg(0) → 0
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
plus(neg(1), x) → P(x)
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(x), neg(y)) → neg(plus(x, y))
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
neg(neg(x)) → x
P(0) → neg(1)
P(neg(x)) → neg(S(x))
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
S(0) → 1
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

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

(33) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PLUS(ba1(x), neg(ba0(y))) → PLUS(ba1(plus(x, neg(y))), neg(0)) at position [1] we obtained the following new rules [LPAR04]:

PLUS(ba1(x), neg(ba0(y))) → PLUS(ba1(plus(x, neg(y))), 0) → PLUS(ba1(x), neg(ba0(y))) → PLUS(ba1(plus(x, neg(y))), 0)

(34) Obligation:

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

PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba0(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → PLUS(ba1(plus(x, neg(y))), 0)

The TRS R consists of the following rules:

plus(1, x) → S(x)
plus(x, neg(1)) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
ba0(0) → 0
ba0(neg(x)) → neg(ba0(x))
neg(0) → 0
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
plus(neg(1), x) → P(x)
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(x), neg(y)) → neg(plus(x, y))
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
neg(neg(x)) → x
P(0) → neg(1)
P(neg(x)) → neg(S(x))
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
S(0) → 1
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

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

(35) DependencyGraphProof (EQUIVALENT transformation)

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

(36) Obligation:

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

PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba0(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(x, neg(y))

The TRS R consists of the following rules:

plus(1, x) → S(x)
plus(x, neg(1)) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
ba0(0) → 0
ba0(neg(x)) → neg(ba0(x))
neg(0) → 0
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
plus(neg(1), x) → P(x)
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(x), neg(y)) → neg(plus(x, y))
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
neg(neg(x)) → x
P(0) → neg(1)
P(neg(x)) → neg(S(x))
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
S(0) → 1
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

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

(37) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PLUS(ba0(x), neg(ba0(y))) → PLUS(ba0(plus(x, neg(y))), neg(0)) at position [1] we obtained the following new rules [LPAR04]:

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

(38) Obligation:

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

PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba1(y)), ba0(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(x, neg(y))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → PLUS(ba0(plus(x, neg(y))), 0)

The TRS R consists of the following rules:

plus(1, x) → S(x)
plus(x, neg(1)) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
ba0(0) → 0
ba0(neg(x)) → neg(ba0(x))
neg(0) → 0
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
plus(neg(1), x) → P(x)
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(x), neg(y)) → neg(plus(x, y))
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
neg(neg(x)) → x
P(0) → neg(1)
P(neg(x)) → neg(S(x))
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
S(0) → 1
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

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

(39) DependencyGraphProof (EQUIVALENT transformation)

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

(40) Complex Obligation (AND)

(41) Obligation:

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

PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))

The TRS R consists of the following rules:

plus(1, x) → S(x)
plus(x, neg(1)) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
ba0(0) → 0
ba0(neg(x)) → neg(ba0(x))
neg(0) → 0
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
plus(neg(1), x) → P(x)
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(x), neg(y)) → neg(plus(x, y))
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
neg(neg(x)) → x
P(0) → neg(1)
P(neg(x)) → neg(S(x))
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
S(0) → 1
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

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

(42) 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.

(43) Obligation:

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

PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))

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

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

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

(44) 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].

S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

(45) Obligation:

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

PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))

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

ba0(0)
ba1(0)
neg(0)
neg(neg(x0))
ba0(neg(x0))
ba1(neg(x0))

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

(46) 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:

  • PLUS(ba1(x), neg(ba1(y))) → PLUS(x, neg(y))
    The graph contains the following edges 1 > 1

  • PLUS(ba0(x), neg(ba1(y))) → PLUS(x, neg(y))
    The graph contains the following edges 1 > 1

  • PLUS(ba1(x), neg(ba0(y))) → PLUS(x, neg(y))
    The graph contains the following edges 1 > 1

  • PLUS(ba0(x), neg(ba0(y))) → PLUS(x, neg(y))
    The graph contains the following edges 1 > 1

(47) YES

(48) Obligation:

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

PLUS(neg(ba0(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))

The TRS R consists of the following rules:

plus(1, x) → S(x)
plus(x, neg(1)) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
ba0(0) → 0
ba0(neg(x)) → neg(ba0(x))
neg(0) → 0
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
plus(neg(1), x) → P(x)
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(x), neg(y)) → neg(plus(x, y))
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
neg(neg(x)) → x
P(0) → neg(1)
P(neg(x)) → neg(S(x))
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
S(0) → 1
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

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

(49) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PLUS(neg(ba0(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), neg(0)) at position [1] we obtained the following new rules [LPAR04]:

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

(50) Obligation:

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

PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))
PLUS(neg(ba0(y)), ba0(x)) → PLUS(ba0(plus(x, neg(y))), 0)

The TRS R consists of the following rules:

plus(1, x) → S(x)
plus(x, neg(1)) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
ba0(0) → 0
ba0(neg(x)) → neg(ba0(x))
neg(0) → 0
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
plus(neg(1), x) → P(x)
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(x), neg(y)) → neg(plus(x, y))
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
neg(neg(x)) → x
P(0) → neg(1)
P(neg(x)) → neg(S(x))
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
S(0) → 1
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

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

(51) DependencyGraphProof (EQUIVALENT transformation)

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

(52) Obligation:

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

PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))

The TRS R consists of the following rules:

plus(1, x) → S(x)
plus(x, neg(1)) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
ba0(0) → 0
ba0(neg(x)) → neg(ba0(x))
neg(0) → 0
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
plus(neg(1), x) → P(x)
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(x), neg(y)) → neg(plus(x, y))
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
neg(neg(x)) → x
P(0) → neg(1)
P(neg(x)) → neg(S(x))
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
S(0) → 1
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

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

(53) TransformationProof (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0)) at position [1] we obtained the following new rules [LPAR04]:

PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), 0) → PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), 0)

(54) Obligation:

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

PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), 0)

The TRS R consists of the following rules:

plus(1, x) → S(x)
plus(x, neg(1)) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
ba0(0) → 0
ba0(neg(x)) → neg(ba0(x))
neg(0) → 0
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
plus(neg(1), x) → P(x)
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(x), neg(y)) → neg(plus(x, y))
ba1(0) → 1
ba1(neg(x)) → neg(ba1(P(x)))
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
neg(neg(x)) → x
P(0) → neg(1)
P(neg(x)) → neg(S(x))
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
S(0) → 1
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))

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

(55) DependencyGraphProof (EQUIVALENT transformation)

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

(56) TRUE

(57) Obligation:

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

MULT(x, ba1(y)) → MULT(x, y)
MULT(x, ba0(y)) → MULT(x, y)

The TRS R consists of the following rules:

ba0(0) → 0
ba1(0) → 1
S(0) → 1
S(1) → ba0(1)
S(ba0(x)) → ba1(x)
S(ba1(x)) → ba0(S(x))
plus(x, 0) → x
plus(0, x) → x
plus(x, 1) → S(x)
plus(1, x) → S(x)
plus(ba0(x), ba0(y)) → plus(ba0(plus(x, y)), 0)
plus(ba1(x), ba0(y)) → plus(ba1(plus(x, y)), 0)
plus(ba0(x), ba1(y)) → plus(ba0(plus(x, y)), 1)
plus(ba1(x), ba1(y)) → plus(ba1(plus(x, y)), 1)
mult(x, 0) → 0
mult(x, 1) → x
mult(x, ba0(y)) → plus(ba0(mult(x, y)), mult(x, 0))
mult(x, ba1(y)) → plus(ba0(mult(x, y)), mult(x, 1))
neg(0) → 0
neg(neg(x)) → x
P(0) → neg(1)
P(1) → 0
P(ba0(x)) → ba1(P(x))
P(ba1(x)) → ba0(x)
P(neg(x)) → neg(S(x))
S(neg(1)) → 0
S(neg(ba0(x))) → neg(ba1(P(x)))
S(neg(ba1(x))) → neg(ba0(x))
ba0(neg(x)) → neg(ba0(x))
ba1(neg(x)) → neg(ba1(P(x)))
plus(x, neg(1)) → P(x)
plus(neg(1), x) → P(x)
plus(ba1(x), neg(ba1(y))) → plus(ba1(plus(x, neg(y))), neg(1))
plus(ba0(x), neg(ba1(y))) → plus(ba0(plus(x, neg(y))), neg(1))
plus(ba1(x), neg(ba0(y))) → plus(ba1(plus(x, neg(y))), neg(0))
plus(ba0(x), neg(ba0(y))) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(ba1(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(1))
plus(neg(ba1(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(1))
plus(neg(ba0(y)), ba1(x)) → plus(ba1(plus(x, neg(y))), neg(0))
plus(neg(ba0(y)), ba0(x)) → plus(ba0(plus(x, neg(y))), neg(0))
plus(neg(x), neg(y)) → neg(plus(x, y))
mult(x, neg(y)) → neg(mult(x, y))

The set Q consists of the following terms:

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

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

(58) 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.

(59) Obligation:

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

MULT(x, ba1(y)) → MULT(x, y)
MULT(x, ba0(y)) → MULT(x, y)

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

ba0(0)
ba1(0)
S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
ba0(neg(x0))
ba1(neg(x0))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

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

(60) 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].

S(0)
S(1)
S(ba0(x0))
S(ba1(x0))
plus(x0, 0)
plus(0, x0)
plus(x0, 1)
plus(1, x0)
plus(ba0(x0), ba0(x1))
plus(ba1(x0), ba0(x1))
plus(ba0(x0), ba1(x1))
plus(ba1(x0), ba1(x1))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
neg(0)
neg(neg(x0))
P(0)
P(1)
P(ba0(x0))
P(ba1(x0))
P(neg(x0))
S(neg(1))
S(neg(ba0(x0)))
S(neg(ba1(x0)))
plus(x0, neg(1))
plus(neg(1), x0)
plus(ba1(x0), neg(ba1(x1)))
plus(ba0(x0), neg(ba1(x1)))
plus(ba1(x0), neg(ba0(x1)))
plus(ba0(x0), neg(ba0(x1)))
plus(neg(ba1(x0)), ba1(x1))
plus(neg(ba1(x0)), ba0(x1))
plus(neg(ba0(x0)), ba1(x1))
plus(neg(ba0(x0)), ba0(x1))
plus(neg(x0), neg(x1))
mult(x0, neg(x1))

(61) Obligation:

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

MULT(x, ba1(y)) → MULT(x, y)
MULT(x, ba0(y)) → MULT(x, y)

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

ba0(0)
ba1(0)
ba0(neg(x0))
ba1(neg(x0))

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

(62) 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, ba1(y)) → MULT(x, y)
    The graph contains the following edges 1 >= 1, 2 > 2

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

(63) YES