0 QTRS
↳1 DependencyPairsProof (⇔, 89 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔, 0 ms)
↳7 QDP
↳8 QReductionProof (⇔, 0 ms)
↳9 QDP
↳10 MRRProof (⇔, 35 ms)
↳11 QDP
↳12 DependencyGraphProof (⇔, 0 ms)
↳13 QDP
↳14 MRRProof (⇔, 11 ms)
↳15 QDP
↳16 TransformationProof (⇔, 0 ms)
↳17 QDP
↳18 QDPOrderProof (⇔, 6 ms)
↳19 QDP
↳20 DependencyGraphProof (⇔, 0 ms)
↳21 TRUE
↳22 QDP
↳23 UsableRulesProof (⇔, 0 ms)
↳24 QDP
↳25 QReductionProof (⇔, 0 ms)
↳26 QDP
↳27 QDPSizeChangeProof (⇔, 0 ms)
↳28 YES
bt(0, x) → x
bt(x, bt(y, z)) → bt(plus(x, y), z)
plus(0, x) → x
plus(x, 0) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(bt(x, y), z) → bt(x, plus(y, z))
mult(x, 0) → 0
mult(0, x) → 0
mult(1, 1) → 1
mult(x, bt(y, z)) → bt(mult(x, y), mult(x, z))
mult(bt(x, y), z) → bt(mult(x, z), mult(y, z))
neg(0) → 0
neg(neg(x)) → x
bt(1, neg(1)) → 1
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(1, neg(1)) → 0
plus(neg(1), 1) → 0
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
mult(x, neg(y)) → neg(mult(x, y))
mult(neg(x), y) → neg(mult(x, y))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
mult(x0, 0)
mult(0, x0)
mult(1, 1)
mult(x0, bt(x1, x2))
mult(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
mult(x0, neg(x1))
mult(neg(x0), x1)
BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(x, bt(y, z)) → PLUS(x, y)
PLUS(1, 1) → BT(1, 0)
PLUS(x, bt(y, z)) → BT(y, plus(x, z))
PLUS(x, bt(y, z)) → PLUS(x, z)
PLUS(bt(x, y), z) → BT(x, plus(y, z))
PLUS(bt(x, y), z) → PLUS(y, z)
MULT(x, bt(y, z)) → BT(mult(x, y), mult(x, z))
MULT(x, bt(y, z)) → MULT(x, y)
MULT(x, bt(y, z)) → MULT(x, z)
MULT(bt(x, y), z) → BT(mult(x, z), mult(y, z))
MULT(bt(x, y), z) → MULT(x, z)
MULT(bt(x, y), z) → MULT(y, z)
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(bt(x, 0), neg(1)) → BT(x, neg(1))
BT(bt(x, 1), neg(1)) → BT(bt(x, 0), 1)
BT(bt(x, 1), neg(1)) → BT(x, 0)
BT(x, neg(bt(y, z))) → NEG(bt(plus(y, neg(x)), z))
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
BT(x, neg(bt(y, z))) → PLUS(y, neg(x))
BT(x, neg(bt(y, z))) → NEG(x)
BT(neg(x), y) → NEG(bt(x, neg(y)))
BT(neg(x), y) → BT(x, neg(y))
BT(neg(x), y) → NEG(y)
PLUS(x, neg(bt(y, z))) → NEG(bt(y, plus(z, neg(x))))
PLUS(x, neg(bt(y, z))) → BT(y, plus(z, neg(x)))
PLUS(x, neg(bt(y, z))) → PLUS(z, neg(x))
PLUS(x, neg(bt(y, z))) → NEG(x)
PLUS(neg(bt(x, y)), z) → NEG(bt(x, plus(y, neg(z))))
PLUS(neg(bt(x, y)), z) → BT(x, plus(y, neg(z)))
PLUS(neg(bt(x, y)), z) → PLUS(y, neg(z))
PLUS(neg(bt(x, y)), z) → NEG(z)
MULT(x, neg(y)) → NEG(mult(x, y))
MULT(x, neg(y)) → MULT(x, y)
MULT(neg(x), y) → NEG(mult(x, y))
MULT(neg(x), y) → MULT(x, y)
bt(0, x) → x
bt(x, bt(y, z)) → bt(plus(x, y), z)
plus(0, x) → x
plus(x, 0) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(bt(x, y), z) → bt(x, plus(y, z))
mult(x, 0) → 0
mult(0, x) → 0
mult(1, 1) → 1
mult(x, bt(y, z)) → bt(mult(x, y), mult(x, z))
mult(bt(x, y), z) → bt(mult(x, z), mult(y, z))
neg(0) → 0
neg(neg(x)) → x
bt(1, neg(1)) → 1
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(1, neg(1)) → 0
plus(neg(1), 1) → 0
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
mult(x, neg(y)) → neg(mult(x, y))
mult(neg(x), y) → neg(mult(x, y))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
mult(x0, 0)
mult(0, x0)
mult(1, 1)
mult(x0, bt(x1, x2))
mult(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
mult(x0, neg(x1))
mult(neg(x0), x1)
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(neg(x), y) → BT(x, neg(y))
BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(bt(x, 0), neg(1)) → BT(x, neg(1))
BT(x, bt(y, z)) → PLUS(x, y)
PLUS(x, bt(y, z)) → BT(y, plus(x, z))
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
BT(x, neg(bt(y, z))) → PLUS(y, neg(x))
PLUS(x, bt(y, z)) → PLUS(x, z)
PLUS(bt(x, y), z) → BT(x, plus(y, z))
PLUS(bt(x, y), z) → PLUS(y, z)
PLUS(x, neg(bt(y, z))) → BT(y, plus(z, neg(x)))
PLUS(x, neg(bt(y, z))) → PLUS(z, neg(x))
PLUS(neg(bt(x, y)), z) → BT(x, plus(y, neg(z)))
PLUS(neg(bt(x, y)), z) → PLUS(y, neg(z))
bt(0, x) → x
bt(x, bt(y, z)) → bt(plus(x, y), z)
plus(0, x) → x
plus(x, 0) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(bt(x, y), z) → bt(x, plus(y, z))
mult(x, 0) → 0
mult(0, x) → 0
mult(1, 1) → 1
mult(x, bt(y, z)) → bt(mult(x, y), mult(x, z))
mult(bt(x, y), z) → bt(mult(x, z), mult(y, z))
neg(0) → 0
neg(neg(x)) → x
bt(1, neg(1)) → 1
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(1, neg(1)) → 0
plus(neg(1), 1) → 0
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
mult(x, neg(y)) → neg(mult(x, y))
mult(neg(x), y) → neg(mult(x, y))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
mult(x0, 0)
mult(0, x0)
mult(1, 1)
mult(x0, bt(x1, x2))
mult(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
mult(x0, neg(x1))
mult(neg(x0), x1)
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(neg(x), y) → BT(x, neg(y))
BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(bt(x, 0), neg(1)) → BT(x, neg(1))
BT(x, bt(y, z)) → PLUS(x, y)
PLUS(x, bt(y, z)) → BT(y, plus(x, z))
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
BT(x, neg(bt(y, z))) → PLUS(y, neg(x))
PLUS(x, bt(y, z)) → PLUS(x, z)
PLUS(bt(x, y), z) → BT(x, plus(y, z))
PLUS(bt(x, y), z) → PLUS(y, z)
PLUS(x, neg(bt(y, z))) → BT(y, plus(z, neg(x)))
PLUS(x, neg(bt(y, z))) → PLUS(z, neg(x))
PLUS(neg(bt(x, y)), z) → BT(x, plus(y, neg(z)))
PLUS(neg(bt(x, y)), z) → PLUS(y, neg(z))
neg(0) → 0
neg(neg(x)) → x
plus(0, x) → x
plus(x, 0) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(1, neg(1)) → 0
plus(neg(1), 1) → 0
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
bt(x, bt(y, z)) → bt(plus(x, y), z)
bt(1, neg(1)) → 1
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
plus(bt(x, y), z) → bt(x, plus(y, z))
bt(0, x) → x
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
mult(x0, 0)
mult(0, x0)
mult(1, 1)
mult(x0, bt(x1, x2))
mult(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
mult(x0, neg(x1))
mult(neg(x0), x1)
mult(x0, 0)
mult(0, x0)
mult(1, 1)
mult(x0, bt(x1, x2))
mult(bt(x0, x1), x2)
mult(x0, neg(x1))
mult(neg(x0), x1)
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(neg(x), y) → BT(x, neg(y))
BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(bt(x, 0), neg(1)) → BT(x, neg(1))
BT(x, bt(y, z)) → PLUS(x, y)
PLUS(x, bt(y, z)) → BT(y, plus(x, z))
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
BT(x, neg(bt(y, z))) → PLUS(y, neg(x))
PLUS(x, bt(y, z)) → PLUS(x, z)
PLUS(bt(x, y), z) → BT(x, plus(y, z))
PLUS(bt(x, y), z) → PLUS(y, z)
PLUS(x, neg(bt(y, z))) → BT(y, plus(z, neg(x)))
PLUS(x, neg(bt(y, z))) → PLUS(z, neg(x))
PLUS(neg(bt(x, y)), z) → BT(x, plus(y, neg(z)))
PLUS(neg(bt(x, y)), z) → PLUS(y, neg(z))
neg(0) → 0
neg(neg(x)) → x
plus(0, x) → x
plus(x, 0) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(1, neg(1)) → 0
plus(neg(1), 1) → 0
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
bt(x, bt(y, z)) → bt(plus(x, y), z)
bt(1, neg(1)) → 1
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
plus(bt(x, y), z) → bt(x, plus(y, z))
bt(0, x) → x
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
BT(bt(x, 0), neg(1)) → BT(x, neg(1))
BT(x, bt(y, z)) → PLUS(x, y)
BT(x, neg(bt(y, z))) → PLUS(y, neg(x))
PLUS(x, bt(y, z)) → PLUS(x, z)
PLUS(bt(x, y), z) → PLUS(y, z)
PLUS(x, neg(bt(y, z))) → PLUS(z, neg(x))
PLUS(neg(bt(x, y)), z) → PLUS(y, neg(z))
plus(0, x) → x
plus(x, 0) → x
plus(1, neg(1)) → 0
plus(neg(1), 1) → 0
bt(1, neg(1)) → 1
bt(0, x) → x
POL(0) = 2
POL(1) = 2
POL(BT(x1, x2)) = 1 + 2·x1 + 2·x2
POL(PLUS(x1, x2)) = 1 + 2·x1 + 2·x2
POL(bt(x1, x2)) = 1 + x1 + x2
POL(neg(x1)) = x1
POL(plus(x1, x2)) = 1 + x1 + x2
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(neg(x), y) → BT(x, neg(y))
BT(x, bt(y, z)) → BT(plus(x, y), z)
PLUS(x, bt(y, z)) → BT(y, plus(x, z))
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
PLUS(bt(x, y), z) → BT(x, plus(y, z))
PLUS(x, neg(bt(y, z))) → BT(y, plus(z, neg(x)))
PLUS(neg(bt(x, y)), z) → BT(x, plus(y, neg(z)))
neg(0) → 0
neg(neg(x)) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
bt(x, bt(y, z)) → bt(plus(x, y), z)
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
plus(bt(x, y), z) → bt(x, plus(y, z))
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
BT(neg(x), y) → BT(x, neg(y))
BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
neg(0) → 0
neg(neg(x)) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
bt(x, bt(y, z)) → bt(plus(x, y), z)
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
plus(bt(x, y), z) → bt(x, plus(y, z))
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
BT(x, bt(y, z)) → BT(plus(x, y), z)
BT(x, neg(bt(y, z))) → BT(plus(y, neg(x)), z)
POL(0) = 1
POL(1) = 1
POL(BT(x1, x2)) = x1 + 2·x2
POL(bt(x1, x2)) = 1 + x1 + x2
POL(neg(x1)) = x1
POL(plus(x1, x2)) = 1 + x1 + x2
BT(neg(x), y) → BT(x, neg(y))
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
neg(0) → 0
neg(neg(x)) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
bt(x, bt(y, z)) → bt(plus(x, y), z)
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
plus(bt(x, y), z) → bt(x, plus(y, z))
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
BT(neg(x0), 1) → BT(x0, neg(1)) → BT(neg(x0), 1) → BT(x0, neg(1))
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
BT(neg(x0), 1) → BT(x0, neg(1))
neg(0) → 0
neg(neg(x)) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
bt(x, bt(y, z)) → bt(plus(x, y), z)
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
plus(bt(x, y), z) → bt(x, plus(y, z))
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
BT(bt(x, 0), neg(1)) → BT(bt(x, neg(1)), 1)
0 > 1
0=1
1=1
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(neg(x), y) → neg(bt(x, neg(y)))
bt(x, bt(y, z)) → bt(plus(x, y), z)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
neg(0) → 0
neg(neg(x)) → x
BT(neg(x0), 1) → BT(x0, neg(1))
neg(0) → 0
neg(neg(x)) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
bt(x, bt(y, z)) → bt(plus(x, y), z)
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
plus(bt(x, y), z) → bt(x, plus(y, z))
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
MULT(x, bt(y, z)) → MULT(x, z)
MULT(bt(x, y), z) → MULT(x, z)
MULT(x, bt(y, z)) → MULT(x, y)
MULT(bt(x, y), z) → MULT(y, z)
MULT(x, neg(y)) → MULT(x, y)
MULT(neg(x), y) → MULT(x, y)
bt(0, x) → x
bt(x, bt(y, z)) → bt(plus(x, y), z)
plus(0, x) → x
plus(x, 0) → x
plus(1, 1) → bt(1, 0)
plus(x, bt(y, z)) → bt(y, plus(x, z))
plus(bt(x, y), z) → bt(x, plus(y, z))
mult(x, 0) → 0
mult(0, x) → 0
mult(1, 1) → 1
mult(x, bt(y, z)) → bt(mult(x, y), mult(x, z))
mult(bt(x, y), z) → bt(mult(x, z), mult(y, z))
neg(0) → 0
neg(neg(x)) → x
bt(1, neg(1)) → 1
bt(bt(x, 0), neg(1)) → bt(bt(x, neg(1)), 1)
bt(bt(x, 1), neg(1)) → bt(bt(x, 0), 1)
bt(x, neg(bt(y, z))) → neg(bt(plus(y, neg(x)), z))
bt(neg(x), y) → neg(bt(x, neg(y)))
plus(1, neg(1)) → 0
plus(neg(1), 1) → 0
plus(x, neg(bt(y, z))) → neg(bt(y, plus(z, neg(x))))
plus(neg(bt(x, y)), z) → neg(bt(x, plus(y, neg(z))))
mult(x, neg(y)) → neg(mult(x, y))
mult(neg(x), y) → neg(mult(x, y))
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
mult(x0, 0)
mult(0, x0)
mult(1, 1)
mult(x0, bt(x1, x2))
mult(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
mult(x0, neg(x1))
mult(neg(x0), x1)
MULT(x, bt(y, z)) → MULT(x, z)
MULT(bt(x, y), z) → MULT(x, z)
MULT(x, bt(y, z)) → MULT(x, y)
MULT(bt(x, y), z) → MULT(y, z)
MULT(x, neg(y)) → MULT(x, y)
MULT(neg(x), y) → MULT(x, y)
bt(0, x0)
bt(x0, bt(x1, x2))
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
mult(x0, 0)
mult(0, x0)
mult(1, 1)
mult(x0, bt(x1, x2))
mult(bt(x0, x1), x2)
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
mult(x0, neg(x1))
mult(neg(x0), x1)
plus(0, x0)
plus(x0, 0)
plus(1, 1)
plus(x0, bt(x1, x2))
plus(bt(x0, x1), x2)
mult(x0, 0)
mult(0, x0)
mult(1, 1)
mult(x0, bt(x1, x2))
mult(bt(x0, x1), x2)
plus(1, neg(1))
plus(neg(1), 1)
plus(x0, neg(bt(x1, x2)))
plus(neg(bt(x0, x1)), x2)
mult(x0, neg(x1))
mult(neg(x0), x1)
MULT(x, bt(y, z)) → MULT(x, z)
MULT(bt(x, y), z) → MULT(x, z)
MULT(x, bt(y, z)) → MULT(x, y)
MULT(bt(x, y), z) → MULT(y, z)
MULT(x, neg(y)) → MULT(x, y)
MULT(neg(x), y) → MULT(x, y)
bt(0, x0)
bt(x0, bt(x1, x2))
neg(0)
neg(neg(x0))
bt(1, neg(1))
bt(bt(x0, 0), neg(1))
bt(bt(x0, 1), neg(1))
bt(x0, neg(bt(x1, x2)))
bt(neg(x0), x1)
From the DPs we obtained the following set of size-change graphs: