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
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))
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))
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)
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))
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))
P1(ba0(x)) → BA1(P(x))
BA1(neg(x)) → BA1(P(x))
BA1(neg(x)) → P1(x)
P1(ba0(x)) → P1(x)
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))
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))
P1(ba0(x)) → BA1(P(x))
BA1(neg(x)) → BA1(P(x))
BA1(neg(x)) → P1(x)
P1(ba0(x)) → P1(x)
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
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))
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))
P1(ba0(x)) → BA1(P(x))
BA1(neg(x)) → BA1(P(x))
BA1(neg(x)) → P1(x)
P1(ba0(x)) → P1(x)
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
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))
P1(ba0(x)) → BA1(P(x))
BA1(neg(x)) → BA1(P(x))
BA1(neg(x)) → P1(x)
P1(ba0(x)) → P1(x)
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
P1 > BA11 > P^11 > ba11 > neg1 > ba01 > 0 > 1
1=3
0=1
P_1=0
ba0_1=2
ba1_1=2
neg_1=1
P^1_1=2
BA1_1=1
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))
S1(ba1(x)) → S1(x)
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))
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))
S1(ba1(x)) → S1(x)
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))
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))
S1(ba1(x)) → S1(x)
ba1(0)
ba1(neg(x0))
From the DPs we obtained the following set of size-change graphs:
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)
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))
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))
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)
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))
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))
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)
ba0(0)
ba1(0)
ba0(neg(x0))
ba1(neg(x0))
From the DPs we obtained the following set of size-change graphs:
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))
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))
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))
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))
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))
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))
mult(x0, 0)
mult(x0, 1)
mult(x0, ba0(x1))
mult(x0, ba1(x1))
mult(x0, neg(x1))
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))
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))
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))
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)
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)
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))
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))
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))
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))
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))
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)
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)
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))
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))
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))
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))
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))
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))
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))
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))
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))
ba0(0)
ba1(0)
neg(0)
neg(neg(x0))
ba0(neg(x0))
ba1(neg(x0))
From the DPs we obtained the following set of size-change graphs:
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))
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))
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))
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)
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)
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))
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))
PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), neg(0))
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))
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))
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)
PLUS(neg(ba0(y)), ba1(x)) → PLUS(ba1(plus(x, neg(y))), 0)
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))
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))
MULT(x, ba1(y)) → MULT(x, y)
MULT(x, ba0(y)) → MULT(x, y)
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))
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))
MULT(x, ba1(y)) → MULT(x, y)
MULT(x, ba0(y)) → MULT(x, y)
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))
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))
MULT(x, ba1(y)) → MULT(x, y)
MULT(x, ba0(y)) → MULT(x, y)
ba0(0)
ba1(0)
ba0(neg(x0))
ba1(neg(x0))
From the DPs we obtained the following set of size-change graphs: