R
↳Dependency Pair Analysis
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)))
R
↳DPs
→DP Problem 1
↳SizeChange Principle
→DP Problem 2
↳Neg POLO
→DP Problem 3
↳MRR
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)))


trivial
s(x_{1}) > s(x_{1})
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Negative Polynomial Order
→DP Problem 3
↳MRR
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)))
QUOT(s(x), s(y)) > QUOT(minus(x, y), s(y))
minus(x, 0) > x
minus(s(x), s(y)) > minus(x, y)
POL( QUOT(x_{1}, x_{2}) ) = x_{1}
POL( s(x_{1}) ) = x_{1} + 1
POL( minus(x_{1}, x_{2}) ) = x_{1}
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Neg POLO
→DP Problem 4
↳Dependency Graph
→DP Problem 3
↳MRR
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)))
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Neg POLO
→DP Problem 3
↳Modular Removal of Rules
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)
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)))
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
plus(0, y) > y
plus(s(x), y) > s(plus(x, y))
minus(s(x), s(y)) > minus(x, y)
minus(x, 0) > x
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)))
_{ }^{ }POL(PLUS(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(plus(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(0) = 0_{ }^{ } _{ }^{ }POL(minus(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(s(x_{1})) = x_{1}_{ }^{ }
2 non usable rules have been deleted.
minus(x, 0) > x
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Neg POLO
→DP Problem 3
↳MRR
→DP Problem 5
↳Modular Removal of Rules
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(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)
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
plus(0, y) > y
plus(s(x), y) > s(plus(x, y))
minus(s(x), s(y)) > minus(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)))
_{ }^{ }POL(PLUS(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(plus(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(0) = 0_{ }^{ } _{ }^{ }POL(minus(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(s(x_{1})) = x_{1}_{ }^{ }
plus(0, y) > y
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Neg POLO
→DP Problem 3
↳MRR
→DP Problem 5
↳MRR
...
→DP Problem 6
↳Modular Removal of Rules
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(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)
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
plus(s(x), y) > s(plus(x, y))
minus(s(x), s(y)) > minus(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)))
_{ }^{ }POL(PLUS(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(plus(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(0) = 0_{ }^{ } _{ }^{ }POL(minus(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(s(x_{1})) = 1 + x_{1}_{ }^{ }
PLUS(s(x), y) > PLUS(x, y)
minus(s(x), s(y)) > minus(x, y)
R
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Neg POLO
→DP Problem 3
↳MRR
→DP Problem 5
↳MRR
...
→DP Problem 7
↳Dependency Graph
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) > 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)))