0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔)
↳7 QDP
↳8 MRRProof (⇔)
↳9 QDP
↳10 MRRProof (⇔)
↳11 QDP
↳12 DependencyGraphProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QDPSizeChangeProof (⇔)
↳18 TRUE
↳19 QDP
↳20 QDPOrderProof (⇔)
↳21 QDP
↳22 PisEmptyProof (⇔)
↳23 TRUE
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) → plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) → plus(plus(y, s(s(z))), plus(x, s(0)))
MINUS(s(x), s(y)) → MINUS(x, y)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) → MINUS(x, y)
PLUS(s(x), y) → PLUS(x, y)
PLUS(minus(x, s(0)), minus(y, s(s(z)))) → PLUS(minus(y, s(s(z))), minus(x, s(0)))
PLUS(plus(x, s(0)), plus(y, s(s(z)))) → PLUS(plus(y, s(s(z))), plus(x, s(0)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) → plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) → plus(plus(y, s(s(z))), plus(x, s(0)))
PLUS(minus(x, s(0)), minus(y, s(s(z)))) → PLUS(minus(y, s(s(z))), minus(x, s(0)))
PLUS(s(x), y) → PLUS(x, y)
PLUS(plus(x, s(0)), plus(y, s(s(z)))) → PLUS(plus(y, s(s(z))), plus(x, s(0)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) → plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) → plus(plus(y, s(s(z))), plus(x, s(0)))
PLUS(minus(x, s(0)), minus(y, s(s(z)))) → PLUS(minus(y, s(s(z))), minus(x, s(0)))
PLUS(s(x), y) → PLUS(x, y)
PLUS(plus(x, s(0)), plus(y, s(s(z)))) → PLUS(plus(y, s(s(z))), plus(x, s(0)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(plus(x, s(0)), plus(y, s(s(z)))) → plus(plus(y, s(s(z))), plus(x, s(0)))
plus(minus(x, s(0)), minus(y, s(s(z)))) → plus(minus(y, s(s(z))), minus(x, s(0)))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
plus(0, y) → y
minus(x, 0) → x
POL(0) = 0
POL(PLUS(x1, x2)) = x1 + x2
POL(minus(x1, x2)) = 1 + x1 + x2
POL(plus(x1, x2)) = 1 + x1 + x2
POL(s(x1)) = x1
PLUS(minus(x, s(0)), minus(y, s(s(z)))) → PLUS(minus(y, s(s(z))), minus(x, s(0)))
PLUS(s(x), y) → PLUS(x, y)
PLUS(plus(x, s(0)), plus(y, s(s(z)))) → PLUS(plus(y, s(s(z))), plus(x, s(0)))
plus(s(x), y) → s(plus(x, y))
plus(plus(x, s(0)), plus(y, s(s(z)))) → plus(plus(y, s(s(z))), plus(x, s(0)))
plus(minus(x, s(0)), minus(y, s(s(z)))) → plus(minus(y, s(s(z))), minus(x, s(0)))
minus(s(x), s(y)) → minus(x, y)
PLUS(s(x), y) → PLUS(x, y)
minus(s(x), s(y)) → minus(x, y)
POL(0) = 0
POL(PLUS(x1, x2)) = x1 + x2
POL(minus(x1, x2)) = x1 + x2
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + x1
PLUS(minus(x, s(0)), minus(y, s(s(z)))) → PLUS(minus(y, s(s(z))), minus(x, s(0)))
PLUS(plus(x, s(0)), plus(y, s(s(z)))) → PLUS(plus(y, s(s(z))), plus(x, s(0)))
plus(s(x), y) → s(plus(x, y))
plus(plus(x, s(0)), plus(y, s(s(z)))) → plus(plus(y, s(s(z))), plus(x, s(0)))
plus(minus(x, s(0)), minus(y, s(s(z)))) → plus(minus(y, s(s(z))), minus(x, s(0)))
MINUS(s(x), s(y)) → MINUS(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) → plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) → plus(plus(y, s(s(z))), plus(x, s(0)))
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) → plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) → plus(plus(y, s(s(z))), plus(x, s(0)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
POL(0) = 0
POL(QUOT(x1, x2)) = x1
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) → plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) → plus(plus(y, s(s(z))), plus(x, s(0)))